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 Complex.inv_natCast_pow_ofReal_pos {n : ℕ} (hn : n ≠ 0) (x : ℝ) : 0 < (↑n ^ ↑x)⁻¹

theorem ArithmeticFunction.iteratedDeriv_LSeries_alternating (a : ArithmeticFunction ℂ) (hn : ∀ (n : ℕ), 0 ≤ a n) {x : ℝ} (h : (LSeries.abscissaOfAbsConv fun (x : ℕ) => a x) < ↑x) (n : ℕ) : 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries fun (x : ℕ) => a x) ↑x

If all values of a ℂ-valued arithmetic function are nonnegative reals and x is a real number in the domain of absolute convergence, then the nth iterated derivative of the associated L-series is nonnegative real when n is even and nonpositive real when n is odd.

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 iteratedDeriv_comp_const_add {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun (z : 𝕜) => f (s + z)) = fun (t : 𝕜) => iteratedDeriv n f (s + t)

theorem iteratedDeriv_comp_add_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun (z : 𝕜) => f (z + s)) = fun (t : 𝕜) => iteratedDeriv n f (t + s)

theorem iteratedDeriv_eq_on_open {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) {f : 𝕜 → F} {g : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) (x : ↑s) (hfg : Set.EqOn f g s) : iteratedDeriv n f ↑x = iteratedDeriv n g ↑x

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 closed ball of radius r around c, where c is real, and all whose iterated derivatives at c are real can be give 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 Complex.nonneg_of_iteratedDeriv_nonneg {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0) ⦃z : ℂ⦄ (hz : 0 ≤ z) : 0 ≤ f z

An entire function whose iterated derivatives at zero are all nonnegative real has nonnegative real values for nonnegative real arguments.

theorem Complex.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.

theorem Complex.at_zero_le_of_iteratedDeriv_nonneg {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0) {z : ℂ} (hz : 0 ≤ z) : f 0 ≤ f z

An entire function whose iterated derivatives at zero are all nonnegative real (except possibly the value itself) has values of the form f 0 + nonneg. real along the nonnegative real axis.

theorem Complex.apply_le_of_iteratedDeriv_nonneg {f : ℂ → ℂ} {s : ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f s) {z : ℂ} (hz : s ≤ z) : f s ≤ f z

An entire function whose iterated derivatives at s`` are all nonnegative real (except possibly the value itself) has values of the form f s + nonneg. realalong the sets + ℝ≥0`.

theorem Complex.at_zero_le_of_iteratedDeriv_alternating {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0) {z : ℂ} (hz : z ≤ 0) : f 0 ≤ f z

An entire function whose iterated derivatives at zero are all real with alternating signs (except possibly the value itself) has values of the form f 0 + nonneg. real along the nonpositive real axis.

theorem Complex.apply_le_of_iteratedDeriv_alternating {f : ℂ → ℂ} {s : ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f s) {z : ℂ} (hz : z ≤ s) : f s ≤ f z

An entire function whose iterated derivatives at s are all real with alternating signs (except possibly the value itself) has values of the form f s + nonneg. real along the set s - ℝ≥0.