Theorem: ContinuousAt.isBigO (EulerProducts/PNT.lean)

State before:
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ (fun w => f (w + z)) =O[𝓝 0] fun x => 1
Tactic:
rw [isBigO_iff']
State after:
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖

State before:
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt (fun w => f (w + z)) 0
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖
Tactic:
simp_rw [Metric.continuousAt_iff', dist_eq_norm_sub, zero_add] at hf
State after:
f : ℂ → ℂ
z : ℂ
hf : ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < ε
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖

State before:
f : ℂ → ℂ
z : ℂ
hf : ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < ε
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖
Tactic:
specialize hf 1 zero_lt_one
State after:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖

State before:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖
Tactic:
refine ⟨‖f z‖ + 1, by positivity, ?_⟩
State after:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ (‖f z‖ + 1) * ‖1‖

State before:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ (‖f z‖ + 1) * ‖1‖
Tactic:
refine Eventually.mp hf <| eventually_of_forall fun w hw ↦ le_of_lt ?_
State after:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
w : ℂ
hw : ‖f (w + z) - f z‖ < 1
⊢ ‖f (w + z)‖ < (‖f z‖ + 1) * ‖1‖

State before:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
w : ℂ
hw : ‖f (w + z) - f z‖ < 1
⊢ ‖f (w + z)‖ < (‖f z‖ + 1) * ‖1‖
Tactic:
calc ‖f (w + z)‖
  _ ≤ ‖f z‖ + ‖f (w + z) - f z‖ := norm_le_insert' ..
  _ < ‖f z‖ + 1 := add_lt_add_left hw _
  _ = _ := by simp only [norm_one, mul_one]
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ ContinuousAt (fun w => f (w + z)) 0
Tactic:
convert (Homeomorph.comp_continuousAt_iff' (Homeomorph.addLeft (-z)) _ z).mp ?_
State after:
case h.e'_1
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ 0 = (Homeomorph.addLeft (-z)) z

case convert_4
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ ContinuousAt ((fun w => f (w + z)) ∘ ⇑(Homeomorph.addLeft (-z))) z

State before:
case h.e'_1
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ 0 = (Homeomorph.addLeft (-z)) z
Tactic:
simp
State after:
no goals

State before:
case convert_4
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ ContinuousAt ((fun w => f (w + z)) ∘ ⇑(Homeomorph.addLeft (-z))) z
Tactic:
simp [Function.comp_def, hf]
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ‖f z‖ + 1 > 0
Tactic:
positivity
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
w : ℂ
hw : ‖f (w + z) - f z‖ < 1
⊢ ‖f z‖ + 1 = (‖f z‖ + 1) * ‖1‖
Tactic:
simp only [norm_one, mul_one]
State after:
no goals