Theorem: WI_tendsto_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ Tendsto (fun c => c / A - (b - a)) (𝓝[>] (A * (b - a))) (𝓝[>] 0)
Tactic:
rw [Metric.tendsto_nhdsWithin_nhdsWithin]
State after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ},
        x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε

State before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ},
        x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
intro ε hε
State after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ {x : ℝ}, x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε

State before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ {x : ℝ}, x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
refine ⟨A * ε, by positivity, ?_⟩
State after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∀ {x : ℝ},
    x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < A * ε → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε

State before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∀ {x : ℝ},
    x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < A * ε → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
intro x hx1 hx2
State after:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε

State before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
constructor
State after:
case left
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0

case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (x / A - (b - a)) 0 < ε

State before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ A * ε > 0
Tactic:
positivity
State after:
no goals

State before:
case left
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0
Tactic:
simpa [lt_div_iff' hA]
State after:
no goals

State before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (x / A - (b - a)) 0 < ε
Tactic:
simp only [Real.dist_eq, dist_zero_right, Real.norm_eq_abs] at hx2 ⊢
State after:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| < ε

State before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| < ε
Tactic:
have : |x / A - (b - a)| = |x - A * (b - a)| / A := by
  rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le] ; congr ; field_simp
State after:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |x / A - (b - a)| = |x - A * (b - a)| / A
⊢ |x / A - (b - a)| < ε

State before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |x / A - (b - a)| = |x - A * (b - a)| / A
⊢ |x / A - (b - a)| < ε
Tactic:
rwa [this, div_lt_iff' hA]
State after:
no goals

State before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| = |x - A * (b - a)| / A
Tactic:
rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le]
State after:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| = |(x - A * (b - a)) / A|

State before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| = |(x - A * (b - a)) / A|
Tactic:
congr
State after:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ x / A - (b - a) = (x - A * (b - a)) / A

State before:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ x / A - (b - a) = (x - A * (b - a)) / A
Tactic:
field_simp
State after:
no goals