internlm/Lean-Github huggingface dataset:
Theorem: Summable.neg_clog_one_sub
Proof state before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
⊢ Summable fun n => -(1 - f n).log
Tactic:
have : g =O[𝓝 0] id := by
  simpa only [g, sub_zero, log_one, neg_zero] using DifferentiableAt.isBigO_sub hg
Proof state after:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
this : g =O[𝓝 0] id
⊢ Summable fun n => -(1 - f n).log
Theorem: Summable.neg_clog_one_sub
Proof state before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
this : g =O[𝓝 0] id
⊢ Summable fun n => -(1 - f n).log
Tactic:
exact Asymptotics.IsBigO.comp_summable this hsum
Proof state after:
no goals
Theorem: Summable.neg_clog_one_sub
Proof state before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
⊢ 1 - 0 ∈ slitPlane
Tactic:
simp only [sub_zero, one_mem_slitPlane]
Proof state after:
no goals
Theorem: Summable.neg_clog_one_sub
Proof state before:
α : Type u_1
f : α → ℂ
hsum : Summable f
g : ℂ → ℂ := fun z => -(1 - z).log
hg : DifferentiableAt ℂ g 0
⊢ g =O[𝓝 0] id
Tactic:
simpa only [g, sub_zero, log_one, neg_zero] using DifferentiableAt.isBigO_sub hg
Proof state after:
no goals
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
have H := Complex.exp_tsum_primes hsum.of_norm.neg_clog_one_sub
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
have help (n : ℕ) : n.primesBelow.prod (fun p ↦ cexp (-log (1 - f p))) =
    n.primesBelow.prod fun p ↦ (1 - f p)⁻¹ := by
  refine Finset.prod_congr rfl (fun p hp ↦ ?_)
  rw [exp_neg, exp_log ?_]
  rw [ne_eq, sub_eq_zero, ← ne_eq]
  exact fun h ↦ (norm_one (α := ℂ) ▸ h.symm ▸ hs (Nat.prime_of_mem_primesBelow hp).one_lt).false
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
simp_rw [help] at H
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
H : Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
help : ∀ (n : ℕ), ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
H : Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
⊢ cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log) = ∑' (n : ℕ), f n
Tactic:
exact tendsto_nhds_unique H <| eulerProduct_completely_multiplicative hsum
Proof state after:
no goals
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n : ℕ
⊢ ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log) = ∏ p ∈ n.primesBelow, (1 - f p)⁻¹
Tactic:
refine Finset.prod_congr rfl (fun p hp ↦ ?_)
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ cexp (-(1 - f p).log) = (1 - f p)⁻¹
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ cexp (-(1 - f p).log) = (1 - f p)⁻¹
Tactic:
rw [exp_neg, exp_log ?_]
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 - f p ≠ 0
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 - f p ≠ 0
Tactic:
rw [ne_eq, sub_eq_zero, ← ne_eq]
Proof state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 ≠ f p
Theorem: EulerProduct.exp_sum_primes_log_eq_tsum
Proof state before:
f : ℕ →*₀ ℂ
hsum : Summable fun x => ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
H :
  Tendsto (fun n => ∏ p ∈ n.primesBelow, cexp (-(1 - f p).log)) atTop (𝓝 (cexp (∑' (p : Nat.Primes), -(1 - f ↑p).log)))
n p : ℕ
hp : p ∈ n.primesBelow
⊢ 1 ≠ f p
Tactic:
exact fun h ↦ (norm_one (α := ℂ) ▸ h.symm ▸ hs (Nat.prime_of_mem_primesBelow hp).one_lt).false
Proof state after:
no goals
Theorem: Asymptotics.isBigO_mul_iff_isBigO_div
Proof state before:
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x => f x * g x) =O[l] h ↔ g =O[l] fun x => h x / f x
Tactic:
rw [isBigO_iff', isBigO_iff']
Proof state after:
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Theorem: Asymptotics.isBigO_mul_iff_isBigO_div
Proof state before:
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Tactic:
refine ⟨fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩⟩ <;>
{ refine H.congr <| Eventually.mp hf <| eventually_of_forall fun x hx ↦ ?_
  rw [norm_mul, norm_div, ← mul_div_assoc, mul_comm]
  have hx' : ‖f x‖ > 0 := norm_pos_iff.mpr hx
  rw [le_div_iff hx', mul_comm] }
Proof state after:
no goals
Theorem: Asymptotics.isBigO_mul_iff_isBigO_div
Proof state before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖
Tactic:
refine H.congr <| Eventually.mp hf <| eventually_of_forall fun x hx ↦ ?_
Proof state after:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h x‖
Theorem: Asymptotics.isBigO_mul_iff_isBigO_div
Proof state before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h x‖
Tactic:
rw [norm_mul, norm_div, ← mul_div_assoc, mul_comm]
Proof state after:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c
Theorem: Asymptotics.isBigO_mul_iff_isBigO_div
Proof state before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c
Tactic:
have hx' : ‖f x‖ > 0 := norm_pos_iff.mpr hx
Proof state after:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
hx' : ‖f x‖ > 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c
Theorem: Asymptotics.isBigO_mul_iff_isBigO_div
Proof state before:
case refine_2
α : Type u_1
F : Type u_2
inst✝ : NormedField F
l : Filter α
f g h : α → F
hf : ∀ᶠ (x : α) in l, f x ≠ 0
x✝ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
c : ℝ
hc : c > 0
H : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
x : α
hx : f x ≠ 0
hx' : ‖f x‖ > 0
⊢ ‖g x‖ ≤ ‖h x‖ * c / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ ‖h x‖ * c
Tactic:
rw [le_div_iff hx', mul_comm]
Proof state after:
no goals
Theorem: DifferentiableAt.isBigO_of_eq_zero
Proof state before:
f : ℂ → ℂ
z : ℂ
hf : DifferentiableAt ℂ f z
hz : f z = 0
⊢ (fun w => f (w + z)) =O[𝓝 0] id
Tactic:
rw [← zero_add z] at hf
Proof state after:
f : ℂ → ℂ
z : ℂ
hf : DifferentiableAt ℂ f (0 + z)
hz : f z = 0
⊢ (fun w => f (w + z)) =O[𝓝 0] id
Theorem: DifferentiableAt.isBigO_of_eq_zero
Proof state before:
f : ℂ → ℂ
z : ℂ
hf : DifferentiableAt ℂ f (0 + z)
hz : f z = 0
⊢ (fun w => f (w + z)) =O[𝓝 0] id
Tactic:
simpa only [zero_add, hz, sub_zero]
  using (hf.hasDerivAt.comp_add_const 0 z).differentiableAt.isBigO_sub
Proof state after:
no goals
Theorem: ContinuousAt.isBigO
Proof state before:
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ (fun w => f (w + z)) =O[𝓝 0] fun x => 1
Tactic:
rw [isBigO_iff']
Proof state after:
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖
Theorem: ContinuousAt.isBigO
Proof 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
Proof state after:
f : ℂ → ℂ
z : ℂ
hf : ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < ε
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖
Theorem: ContinuousAt.isBigO
Proof 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
Proof state after:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ∃ c > 0, ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ c * ‖1‖
Theorem: ContinuousAt.isBigO
Proof 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, ?_⟩
Proof state after:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z)‖ ≤ (‖f z‖ + 1) * ‖1‖
Theorem: ContinuousAt.isBigO
Proof 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 ?_
Proof 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‖
Theorem: ContinuousAt.isBigO
Proof 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]
Proof state after:
no goals
Theorem: ContinuousAt.isBigO
Proof 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 ?_
Proof 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
Theorem: ContinuousAt.isBigO
Proof state before:
case h.e'_1
f : ℂ → ℂ
z : ℂ
hf : ContinuousAt f z
⊢ 0 = (Homeomorph.addLeft (-z)) z
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousAt.isBigO
Proof 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]
Proof state after:
no goals
Theorem: ContinuousAt.isBigO
Proof state before:
f : ℂ → ℂ
z : ℂ
hf : ∀ᶠ (x : ℂ) in 𝓝 0, ‖f (x + z) - f z‖ < 1
⊢ ‖f z‖ + 1 > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: ContinuousAt.isBigO
Proof 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]
Proof state after:
no goals
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ ∃ u', u = ↑u' ∧ HasDerivAt f u' z
Tactic:
lift u to ℝ
Proof state after:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ u.im = 0

case intro
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ ∃ u', ↑u = ↑u' ∧ HasDerivAt f u' z
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
case intro
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ ∃ u', ↑u = ↑u' ∧ HasDerivAt f u' z
Tactic:
refine ⟨u, rfl, ?_⟩
Proof state after:
case intro
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ HasDerivAt f u z
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
case intro
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ HasDerivAt f u z
Tactic:
convert (reCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt
Proof state after:
case h.e'_7
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
case h.e'_7
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1
Tactic:
rw [comp_apply, smulRight_apply, one_apply, one_smul, reCLM_apply, ofReal_re]
Proof state after:
no goals
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ u.im = 0
Tactic:
have H := (imCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt.deriv
Proof state after:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : _root_.deriv (⇑imCLM ∘ fun y => ↑(f y)) z = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : _root_.deriv (⇑imCLM ∘ fun y => ↑(f y)) z = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Tactic:
simp only [Function.comp_def, imCLM_apply, ofReal_im, deriv_const] at H
Proof state after:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp
Proof state before:
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Tactic:
rwa [eq_comm, comp_apply, imCLM_apply, smulRight_apply, one_apply, one_smul] at H
Proof state after:
no goals
Theorem: DifferentiableAt.ofReal_comp_iff
Proof state before:
z : ℝ
f : ℝ → ℝ
⊢ DifferentiableAt ℝ (fun y => ↑(f y)) z ↔ DifferentiableAt ℝ f z
Tactic:
refine ⟨fun H ↦ ?_, ofReal_comp⟩
Proof state after:
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ DifferentiableAt ℝ f z
Theorem: DifferentiableAt.ofReal_comp_iff
Proof state before:
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ DifferentiableAt ℝ f z
Tactic:
obtain ⟨u, _, hu₂⟩ := H.hasDerivAt.of_hasDerivAt_ofReal_comp
Proof state after:
case intro.intro
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
u : ℝ
left✝ : deriv (fun y => ↑(f y)) z = ↑u
hu₂ : HasDerivAt (fun y => f y) u z
⊢ DifferentiableAt ℝ f z
Theorem: DifferentiableAt.ofReal_comp_iff
Proof state before:
case intro.intro
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
u : ℝ
left✝ : deriv (fun y => ↑(f y)) z = ↑u
hu₂ : HasDerivAt (fun y => f y) u z
⊢ DifferentiableAt ℝ f z
Tactic:
exact HasDerivAt.differentiableAt hu₂
Proof state after:
no goals
Theorem: deriv.ofReal_comp
Proof state before:
z : ℝ
f : ℝ → ℝ
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
by_cases hf : DifferentiableAt ℝ f z
Proof state after:
case pos
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)

case neg
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Theorem: deriv.ofReal_comp
Proof state before:
case pos
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
exact hf.hasDerivAt.ofReal_comp.deriv
Proof state after:
no goals
Theorem: deriv.ofReal_comp
Proof state before:
case neg
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
have hf' := mt DifferentiableAt.ofReal_comp_iff.mp hf
Proof state after:
case neg
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Theorem: deriv.ofReal_comp
Proof state before:
case neg
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
rw [deriv_zero_of_not_differentiableAt hf, deriv_zero_of_not_differentiableAt hf',
  Complex.ofReal_zero]
Proof state after:
no goals
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Tactic:
have Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), (x : ℂ) ∈ Metric.ball (c : ℂ) r := by
  intro x hx
  refine Metric.mem_ball.mpr ?_
  rw [dist_eq, ← ofReal_sub, abs_ofReal, abs_sub_lt_iff, sub_lt_iff_lt_add', sub_lt_comm]
  exact and_comm.mpr hx
Proof state after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Tactic:
have H ⦃z : ℂ⦄ (hz : z ∈ Metric.ball (c : ℂ) r) := taylorSeries_eq_on_ball' hz hf
Proof state after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Tactic:
refine ⟨fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ * (D n) * (x - c) ^ n, fun x hx ↦ ?_, fun x hx ↦ ?_⟩
Proof state after:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x

case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
⊢ ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
Tactic:
intro x hx
Proof state after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ↑x ∈ Metric.ball (↑c) r
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ↑x ∈ Metric.ball (↑c) r
Tactic:
refine Metric.mem_ball.mpr ?_
Proof state after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ dist ↑x ↑c < r
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ dist ↑x ↑c < r
Tactic:
rw [dist_eq, ← ofReal_sub, abs_ofReal, abs_sub_lt_iff, sub_lt_iff_lt_add', sub_lt_comm]
Proof state after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ x < c + r ∧ c - r < x