Auxiliary lemmas

theorem Complex.summable_re {α : Type u_1} {f : α → ℂ} (h : Summable f) : Summable fun (x : α) => (f x).re

theorem Complex.summable_im {α : Type u_1} {f : α → ℂ} (h : Summable f) : Summable fun (x : α) => (f x).im

theorem DifferentiableAt.isBigO_of_eq_zero {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℂ f z) (hz : f z = 0) : (fun (w : ℂ) => f (w + z)) =O[nhds 0] id

theorem ContinuousAt.isBigO {f : ℂ → ℂ} {z : ℂ} (hf : ContinuousAt f z) : (fun (w : ℂ) => f (w + z)) =O[nhds 0] fun (x : ℂ) => 1

theorem Complex.isBigO_comp_ofReal {f : ℂ → ℂ} {g : ℂ → ℂ} {x : ℝ} (h : f =O[nhds ↑x] g) : (fun (y : ℝ) => f ↑y) =O[nhds x] fun (y : ℝ) => g ↑y

theorem Complex.isBigO_comp_ofReal_nhds_ne {f : ℂ → ℂ} {g : ℂ → ℂ} {x : ℝ} (h : f =O[nhdsWithin ↑x {↑x}ᶜ] g) : (fun (y : ℝ) => f ↑y) =O[nhdsWithin x {x}ᶜ] fun (y : ℝ) => g ↑y

theorem Complex.hasDerivAt_ofReal (x : ℝ) : HasDerivAt Complex.ofReal 1 x

theorem Complex.deriv_ofReal (x : ℝ) : deriv Complex.ofReal x = 1

theorem Complex.differentiableAt_ofReal (x : ℝ) : DifferentiableAt ℝ Complex.ofReal x

theorem Complex.differentiable_ofReal : Differentiable ℝ Complex.ofReal

theorem DifferentiableAt.comp_ofReal {e : ℂ → ℂ} {z : ℝ} (hf : DifferentiableAt ℂ e ↑z) : DifferentiableAt ℝ (fun (x : ℝ) => e ↑x) z

theorem deriv.comp_ofReal {e : ℂ → ℂ} {z : ℝ} (hf : DifferentiableAt ℂ e ↑z) : deriv (fun (x : ℝ) => e ↑x) z = deriv e ↑z

theorem Differentiable.comp_ofReal {e : ℂ → ℂ} (h : Differentiable ℂ e) : Differentiable ℝ fun (x : ℝ) => e ↑x

theorem DifferentiableAt.ofReal_comp {z : ℝ} {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f z) : DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y)) z

theorem Differentiable.ofReal_comp {f : ℝ → ℝ} (hf : Differentiable ℝ f) : Differentiable ℝ fun (y : ℝ) => ↑(f y)

theorem HasDerivAt.of_hasDerivAt_ofReal_comp {z : ℝ} {f : ℝ → ℝ} {u : ℂ} (hf : HasDerivAt (fun (y : ℝ) => ↑(f y)) u z) : ∃ (u' : ℝ), u = ↑u' ∧ HasDerivAt f u' z

theorem DifferentiableAt.ofReal_comp_iff {z : ℝ} {f : ℝ → ℝ} : DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y)) z ↔ DifferentiableAt ℝ f z

theorem Differentiable.ofReal_comp_iff {f : ℝ → ℝ} : (Differentiable ℝ fun (y : ℝ) => ↑(f y)) ↔ Differentiable ℝ f

theorem deriv.ofReal_comp {z : ℝ} {f : ℝ → ℝ} : deriv (fun (y : ℝ) => ↑(f y)) z = ↑(deriv f z)

theorem Complex.realValued_of_iteratedDeriv_real_on_ball {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 ∘ Complex.ofReal) (Complex.ofReal ∘ F) (Set.Ioo (c - r) (c + r))

A function that is complex differentiable on the open ball of radius r around c, where c is real, and all whose iterated derivatives at c are real can be given by a real differentiable function on the real open interval from c-r to c+r.

theorem Complex.realValued_of_iteratedDeriv_real {f : ℂ → ℂ} (hf : Differentiable ℂ f) {c : ℝ} {D : ℕ → ℝ} (hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)) : ∃ (F : ℝ → ℝ), Differentiable ℝ F ∧ f ∘ Complex.ofReal = Complex.ofReal ∘ F

A function that is complex differentiable on the complex plane and all whose iterated derivatives at a real point c are real can be given by a real differentiable function on the real line.

theorem monotoneOn_of_iteratedDeriv_nonneg {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0) : MonotoneOn (f ∘ Complex.ofReal) (Set.Ici 0)

An entire function whose iterated derivatives at zero are all nonnegative real is monotonic on the nonnegative real axis.