internlm/Lean-Github huggingface dataset:
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 < c + r ∧ c - r < x
Tactic:
exact and_comm.mpr hx
Proof state after:
no goals
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
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
Tactic:
have Hx := Hz _ 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)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
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)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x
Tactic:
refine DifferentiableAt.differentiableWithinAt ?_
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)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
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)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
replace hf := ((hf x Hx).congr (fun _ hz ↦ H hz) (H Hx)).differentiableAt
  (Metric.isOpen_ball.mem_nhds Hx) |>.comp_ofReal
Proof state after:
case refine_1
f : ℂ → ℂ
r c : ℝ
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)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (↑x - ↑c) ^ n) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
case refine_1
f : ℂ → ℂ
r c : ℝ
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)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (↑x - ↑c) ^ n) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
simp_rw [hd, ← ofReal_sub, ← ofReal_natCast, ← ofReal_inv, ← ofReal_pow, ← ofReal_mul,
  ← ofReal_tsum] at hf
Proof state after:
case refine_1
f : ℂ → ℂ
r c : ℝ
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)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
case refine_1
f : ℂ → ℂ
r c : ℝ
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)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
exact DifferentiableAt.ofReal_comp_iff.mp hf
Proof state after:
no goals
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
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
Tactic:
simp only [Function.comp_apply, ← H (Hz _ hx), hd, ofReal_tsum]
Proof state after:
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)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
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)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)
Tactic:
push_cast
Proof state after:
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)
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a
Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball
Proof state before:
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)
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a
Tactic:
rfl
Proof state after:
no goals
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Tactic:
have H (z : ℂ) := taylorSeries_eq_of_entire' c z hf
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Tactic:
simp_rw [hd] at H
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Tactic:
refine ⟨fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ * (D n) * (x - c) ^ n, ?_, ?_⟩
Proof state after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n

case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ f ∘ ofReal' = ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
have := hf.comp_ofReal
Proof state after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => f ↑x
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => f ↑x
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
simp_rw [← H, ← ofReal_sub, ← ofReal_natCast, ← ofReal_inv, ← ofReal_pow, ← ofReal_mul,
  ← ofReal_tsum] at this
Proof state after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
exact Differentiable.ofReal_comp_iff.mp this
Proof state after:
no goals
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ f ∘ ofReal' = ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
ext x
Proof state after:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
simp only [Function.comp_apply, ofReal_eq_coe, ← H, ofReal_tsum]
Proof state after:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)
Tactic:
push_cast
Proof state after:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a
Theorem: Complex.realValued_of_iteratedDeriv_real
Proof state before:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a
Tactic:
rfl
Proof state after:
no goals
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
⊢ 0 ≤ f z
Tactic:
have H := taylorSeries_eq_of_entire' 0 z hf
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
⊢ 0 ≤ f z
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
⊢ 0 ≤ f z
Tactic:
have hz' := eq_re_of_ofReal_le hz
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
hz' : z = ↑z.re
⊢ 0 ≤ f z
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
hz' : z = ↑z.re
⊢ 0 ≤ f z
Tactic:
rw [hz'] at hz H ⊢
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ 0 ≤ f ↑z.re
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ 0 ≤ f ↑z.re
Tactic:
obtain ⟨D, hD⟩ : ∃ D : ℕ → ℝ, ∀ n, 0 ≤ D n ∧ iteratedDeriv n f 0 = D n
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ ∃ D, ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)

case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ f ↑z.re
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ f ↑z.re
Tactic:
simp_rw [← H, hD, ← ofReal_natCast, sub_zero, ← ofReal_pow, ← ofReal_inv, ← ofReal_mul,
  ← ofReal_tsum]
Proof state after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a)
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a)
Tactic:
norm_cast
Proof state after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a
Tactic:
refine tsum_nonneg fun n ↦ ?_
Proof state after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Tactic:
norm_cast at hz
Proof state after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Tactic:
have := (hD n).1
Proof state after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
this : 0 ≤ D n
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
this : 0 ≤ D n
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Tactic:
positivity
Proof state after:
no goals
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ ∃ D, ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
Tactic:
refine ⟨fun n ↦ (iteratedDeriv n f 0).re, fun n ↦ ⟨?_, ?_⟩⟩
Proof state after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n

case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ iteratedDeriv n f 0 = ↑((fun n => (iteratedDeriv n f 0).re) n)
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n
Tactic:
have := eq_re_of_ofReal_le (h n) ▸ h n
Proof state after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
this : 0 ≤ ↑(iteratedDeriv n f 0).re
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
this : 0 ≤ ↑(iteratedDeriv n f 0).re
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n
Tactic:
norm_cast at this
Proof state after:
no goals
Theorem: Complex.nonneg_of_iteratedDeriv_nonneg
Proof state before:
case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ iteratedDeriv n f 0 = ↑((fun n => (iteratedDeriv n f 0).re) n)
Tactic:
rw [eq_re_of_ofReal_le (h n)]
Proof state after:
no goals
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
let D : ℕ → ℝ := fun n ↦ (iteratedDeriv n f 0).re
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Theorem: Complex.monotoneOn_of_iteratedDeriv_nonneg
Proof state before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)
Tactic:
have hD (n : ℕ) : iteratedDeriv n f 0 = D n := by
  refine Complex.ext rfl ?_
  simp only [ofReal_im]
  exact (le_def.mp (h n)).2.symm
Proof state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
D : ℕ → ℝ := fun n => (iteratedDeriv n f 0).re
hD : ∀ (n : ℕ), iteratedDeriv n f 0 = ↑(D n)
⊢ MonotoneOn (f ∘ ofReal') (Set.Ici 0)