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 => b - a - c / 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 ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < A * ε → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < A * ε → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0
Tactic:
simpa [div_lt_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 ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (b - a - x / A) 0 < ε
Tactic:
simp [Real.dist_eq] 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| < ε
Tactic:
have : |(b - a) - x / A| = |A * (b - a) - x| / A := by
  rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le] ; congr ; field_simp ; ring
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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |b - a - x / A| = |A * (b - a) - x| / A
⊢ |b - a - x / 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |b - a - x / A| = |A * (b - a) - x| / A
⊢ |b - a - x / A| < ε
Tactic:
rwa [this, div_lt_iff' hA, ← neg_sub, abs_neg]
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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| = |A * (b - a) - x| / 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| = |(A * (b - a) - x) / 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| = |(A * (b - a) - x) / 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ b - a - x / A = (A * (b - a) - x) / 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ b - a - x / A = (A * (b - a) - x) / A
Tactic:
field_simp
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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ (b - a) * A = A * (b - 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 ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ (b - a) * A = A * (b - a)
Tactic:
ring
State after:
no goals