Loogle!

Result

Found 169 declarations mentioning iteratedDeriv.

• iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (x : 𝕜) : F
• iteratedDeriv_zero 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : iteratedDeriv 0 f = f
• iteratedDerivWithin_univ 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDerivWithin n f Set.univ = iteratedDeriv n f
• iteratedDerivWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s
• iteratedDeriv_one 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : iteratedDeriv 1 f = deriv f
• iteratedDeriv_eq_iterate 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv n f = deriv^[n] f
• iteratedDeriv_fun_const_zero 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} : iteratedDeriv n (fun x => 0) x = 0
• iteratedDeriv_const 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {c : F} {x : 𝕜} : iteratedDeriv n (fun x => c) x = if n = 0 then c else 0
• iteratedDeriv_const_zero 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} : iteratedDeriv n 0 x = 0
• iteratedDeriv_succ 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)
• iteratedDeriv_succ' 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
• ContDiff.continuous_iteratedDeriv' 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (m : ℕ) (h : ContDiff 𝕜 (↑m) f) : Continuous (iteratedDeriv m f)
• ContDiff.continuous_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : WithTop ℕ∞} (m : ℕ) (h : ContDiff 𝕜 n f) (hmn : ↑m ≤ n) : Continuous (iteratedDeriv m f)
• contDiff_of_differentiable_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ∞} (h : ∀ (m : ℕ), ↑m ≤ n → Differentiable 𝕜 (iteratedDeriv m f)) : ContDiff 𝕜 (↑n) f
• contDiff_nat_succ_iff_contDiff_one_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ} : ContDiff 𝕜 (↑(n + 1)) f ↔ ContDiff 𝕜 (↑n) f ∧ ContDiff 𝕜 1 (iteratedDeriv n f)
• iteratedDerivWithin_eq_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 (↑n) f x) (hx : x ∈ s) : iteratedDerivWithin n f s x = iteratedDeriv n f x
• ContDiff.differentiable_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : WithTop ℕ∞} (m : ℕ) (h : ContDiff 𝕜 n f) (hmn : ↑m < n) : Differentiable 𝕜 (iteratedDeriv m f)
• ContDiff.differentiable_iteratedDeriv' 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (m : ℕ) (h : ContDiff 𝕜 (↑m + 1) f) : Differentiable 𝕜 (iteratedDeriv m f)
• contDiff_nat_iff_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ} : ContDiff 𝕜 (↑n) f ↔ (∀ m ≤ n, Continuous (iteratedDeriv m f)) ∧ ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)
• contDiff_iff_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ∞} : ContDiff 𝕜 (↑n) f ↔ (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)
• norm_iteratedFDeriv_eq_norm_iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} : ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖
• AnalyticAt.hasFPowerSeriesAt 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (h : AnalyticAt 𝕜 f x) : HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x
• iteratedDeriv_eq_iteratedFDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} : iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun x => 1
• iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {x : 𝕜} {m : Fin n → 𝕜} : (iteratedFDeriv 𝕜 n f x) m = (∏ i, m i) • iteratedDeriv n f x
• iteratedFDeriv_eq_equiv_comp 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f
• iteratedDeriv_eq_equiv_comp 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} : iteratedDeriv n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f
• Filter.EventuallyEq.iteratedDeriv_eq 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) {f g : 𝕜 → F} {x : 𝕜} (hfg : f =ᶠ[nhds x] g) : iteratedDeriv n f x = iteratedDeriv n g x
• Set.EqOn.iteratedDeriv_of_isOpen 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set 𝕜} {f g : 𝕜 → F} (hfg : Set.EqOn f g s) (hs : IsOpen s) (n : ℕ) : Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s
• iteratedDeriv_const_add 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x
• iteratedDeriv_fun_neg 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (fun x => -f x) a = -iteratedDeriv n f a
• iteratedDeriv_neg 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (-f) a = -iteratedDeriv n f a
• Filter.EventuallyEq.iteratedDeriv 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ f₂ : 𝕜 → F} {x : 𝕜} (h : f₁ =ᶠ[nhds x] f₂) (n : ℕ) : iteratedDeriv n f₁ =ᶠ[nhds x] iteratedDeriv n f₂
• iteratedDeriv_comp_add_const 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun z => f (z + s)) = fun t => iteratedDeriv n f (t + s)
• iteratedDeriv_comp_const_add 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun z => f (s + z)) = fun t => iteratedDeriv n f (s + t)
• iteratedDeriv_const_sub 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x
• iteratedDeriv_comp_sub_const 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun z => f (z - s)) = fun t => iteratedDeriv n f (t - s)
• iteratedDeriv_div_const 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : ℕ} (f : 𝕜 → 𝕜') (c : 𝕜') : iteratedDeriv n (fun x => f x / c) x = iteratedDeriv n f x / c
• iteratedDeriv_fun_id 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} : iteratedDeriv n (fun x => x) x = if n = 0 then x else if n = 1 then 1 else 0
• iteratedDeriv_fun_id_zero 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} : iteratedDeriv n (fun a => a) 0 = if n = 1 then 1 else 0
• iteratedDeriv_id 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} : iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0
• iteratedDeriv_fun_pow_zero 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n m : ℕ} : iteratedDeriv n (fun x => x ^ m) 0 = ↑(if n = m then m.factorial else 0)
• iteratedDeriv_fun_sum 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} (hf : ∀ i ∈ I, ContDiffAt 𝕜 (↑n) (f i) x) : iteratedDeriv n (fun z => ∑ i ∈ I, f i z) x = ∑ i ∈ I, iteratedDeriv n (f i) x
• iteratedDeriv_const_mul_field 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : ℕ} (c : 𝕜') (f : 𝕜 → 𝕜') : iteratedDeriv n (fun x => c * f x) x = c * iteratedDeriv n f x
• iteratedDeriv_mul_const_field 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : ℕ} (f : 𝕜 → 𝕜') (c : 𝕜') : iteratedDeriv n (fun x => f x * c) x = iteratedDeriv n f x * c
• iteratedDeriv_sum 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} (hf : ∀ i ∈ I, ContDiffAt 𝕜 (↑n) (f i) x) : iteratedDeriv n (∑ i ∈ I, f i) x = ∑ i ∈ I, iteratedDeriv n (f i) x
• iteratedDeriv_pow 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} (m k : ℕ) : iteratedDeriv k (fun x => x ^ m) x = ↑(m.descFactorial k) * x ^ (m - k)
• iteratedDeriv_const_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {n : ℕ} {f : 𝕜 → 𝔸} (c : 𝔸) (hf : ContDiffAt 𝕜 (↑n) f x) : iteratedDeriv n (fun x => c * f x) x = c * iteratedDeriv n f x
• iteratedDeriv_fun_sub 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (fun i => f i - g i) x = iteratedDeriv n f x - iteratedDeriv n g x
• iteratedDeriv_fun_add 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (fun i => f i + g i) x = iteratedDeriv n f x + iteratedDeriv n g x
• iteratedDeriv_sub 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x
• iteratedDeriv_add 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x
• iteratedDeriv_comp_const_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiff 𝕜 (↑n) f) (c : 𝕜) : (iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x)
• iteratedDeriv_comp_const_smul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} (h : ContDiff 𝕜 (↑n) f) (c : 𝕜) : (iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x)
• iteratedDeriv_comp_neg 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (fun x => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)
• iteratedDeriv_comp_const_sub 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun z => f (s - z)) = fun t => (-1) ^ n • iteratedDeriv n f (s - t)
• iteratedDeriv_fun_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (fun i => f i * g i) x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x
• iteratedDeriv_mul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (f * g) x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x
• iteratedDeriv_fun_const_smul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 (↑n) f x) (c : R) : iteratedDeriv n (fun i => c • f i) x = c • iteratedDeriv n f x
• iteratedDeriv_const_smul 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 (↑n) f x) (c : R) : iteratedDeriv n (c • f) x = c • iteratedDeriv n f x
• iteratedDeriv_fun_const_smul_field 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_4} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] {n : ℕ} (c : 𝕝) (f : 𝕜 → F) : iteratedDeriv n (fun x => c • f x) x = c • iteratedDeriv n f x
• iteratedDeriv_const_smul_field 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_4} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] {n : ℕ} (c : 𝕝) (f : 𝕜 → F) : iteratedDeriv n (c • f) x = c • iteratedDeriv n f x
• iteratedDeriv_smul_const 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Module 𝔸 F] [IsBoundedSMul 𝔸 F] [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (v : F) : iteratedDeriv n (fun y => f y • v) x = iteratedDeriv n f x • v
• iteratedDeriv_exp_const_mul 📋 Mathlib.Analysis.SpecialFunctions.ExpDeriv
  (n : ℕ) (c : ℝ) : (iteratedDeriv n fun s => Real.exp (c * s)) = fun s => c ^ n * Real.exp (c * s)
• iteratedDeriv_cexp_const_mul 📋 Mathlib.Analysis.SpecialFunctions.ExpDeriv
  (n : ℕ) (c : ℂ) : (iteratedDeriv n fun s => Complex.exp (c * s)) = fun s => c ^ n * Complex.exp (c * s)
• DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ} (h0 : 0 < R) (n : ℕ) (hc : DiffContOnCl ℂ f (Metric.ball c R)) : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
• DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ} (h0 : 0 < R) (n : ℕ) (hc : DifferentiableOn ℂ f (Metric.closedBall c R)) : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
• Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable 📋 Mathlib.Analysis.Complex.CauchyIntegral
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {f : ℂ → E} {c : ℂ} {s : Set ℂ} (h0 : 0 < R) (n : ℕ) (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : ∀ z ∈ Metric.ball c R \ s, DifferentiableAt ℂ f z) : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑Real.pi * Complex.I / ↑n.factorial) • iteratedDeriv n f c
• Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le 📋 Mathlib.Analysis.Complex.Liouville
  {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (n : ℕ) (hR : 0 < R) (hf : DiffContOnCl ℂ f (Metric.ball c R)) (hC : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖iteratedDeriv n f c‖ ≤ ↑n.factorial * C / R ^ n
• AnalyticOn.hasFPowerSeriesOnSubball 📋 Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
  {𝕜 : Type u_1} [RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} {r : ENNReal} (hr_pos : 0 < r) (h : AnalyticOn 𝕜 f (Metric.eball x r)) : r ≤ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius → HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x r
• AnalyticOn.hasFPowerSeriesOnBall 📋 Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
  {𝕜 : Type u_1} [RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} : 0 < (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius → AnalyticOn 𝕜 f (Metric.eball x (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius) → HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius
• iteratedDeriv_succ_log 📋 Mathlib.Analysis.SpecialFunctions.Complex.Analytic
  {n : ℕ} {x : ℂ} (hx : x ∈ Complex.slitPlane) : iteratedDeriv (n + 1) Complex.log x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)
• Real.abs_iteratedDeriv_cos_le_one 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) (x : ℝ) : |iteratedDeriv n Real.cos x| ≤ 1
• Real.abs_iteratedDeriv_sin_le_one 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) (x : ℝ) : |iteratedDeriv n Real.sin x| ≤ 1
• Complex.iteratedDeriv_add_one_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (n + 1) Complex.sin = iteratedDeriv n Complex.cos
• Real.iteratedDeriv_add_one_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (n + 1) Real.sin = iteratedDeriv n Real.cos
• Complex.iteratedDeriv_add_one_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (n + 1) Complex.cos = -iteratedDeriv n Complex.sin
• Real.iteratedDerivWithin_cos_Ioo 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n Real.cos (Set.Ioo a b) x = iteratedDeriv n Real.cos x
• Real.iteratedDerivWithin_sin_Ioo 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n Real.sin (Set.Ioo a b) x = iteratedDeriv n Real.sin x
• Real.iteratedDeriv_add_one_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (n + 1) Real.cos = -iteratedDeriv n Real.sin
• Real.iteratedDerivWithin_cos_Icc 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n Real.cos (Set.Icc a b) x = iteratedDeriv n Real.cos x
• Real.iteratedDerivWithin_sin_Icc 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n Real.sin (Set.Icc a b) x = iteratedDeriv n Real.sin x
• Real.differentiable_iteratedDeriv_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : Differentiable ℝ (iteratedDeriv n Real.cos)
• Real.differentiable_iteratedDeriv_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : Differentiable ℝ (iteratedDeriv n Real.sin)
• Complex.differentiable_iteratedDeriv_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : Differentiable ℂ (iteratedDeriv n Complex.cos)
• Complex.differentiable_iteratedDeriv_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : Differentiable ℂ (iteratedDeriv n Complex.sin)
• Real.iteratedDeriv_even_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n) Real.cos = (-1) ^ n * Real.cos
• Real.iteratedDeriv_even_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n) Real.sin = (-1) ^ n * Real.sin
• Complex.iteratedDeriv_even_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n) Complex.cos = (-1) ^ n * Complex.cos
• Complex.iteratedDeriv_even_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n) Complex.sin = (-1) ^ n * Complex.sin
• Real.iteratedDeriv_odd_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n + 1) Real.sin = (-1) ^ n * Real.cos
• Complex.iteratedDeriv_odd_sin 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n + 1) Complex.sin = (-1) ^ n * Complex.cos
• Real.iteratedDeriv_odd_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n + 1) Real.cos = (-1) ^ (n + 1) * Real.sin
• Complex.iteratedDeriv_odd_cos 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
  (n : ℕ) : iteratedDeriv (2 * n + 1) Complex.cos = (-1) ^ (n + 1) * Complex.sin
• natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero 📋 Mathlib.Analysis.Analytic.Order
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {n : ℕ} {z₀ : 𝕜} [CharZero 𝕜] [CompleteSpace E] (hf : AnalyticAt 𝕜 f z₀) : ↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0
• analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero 📋 Mathlib.Analysis.Analytic.Order
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {z₀ : 𝕜} {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f z₀) {n : ℕ} : analyticOrderAt f z₀ = ↑n ↔ (∀ k < n, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv n f z₀ ≠ 0
• AnalyticAt.exists_eq_sum_add_pow_mul 📋 Mathlib.Analysis.Analytic.Order
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f 0) (n : ℕ) : ∃ F, AnalyticAt 𝕜 F 0 ∧ ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
• AnalyticAt.exists_eventuallyEq_sum_add_pow_mul 📋 Mathlib.Analysis.Analytic.Order
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f 0) (n : ℕ) : ∃ F, AnalyticAt 𝕜 F 0 ∧ ∀ᶠ (z : 𝕜) in nhds 0, f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z
• AbsolutelyMonotoneOn.of_contDiff 📋 Mathlib.Analysis.Calculus.AbsolutelyMonotone
  {f : ℝ → ℝ} {s : Set ℝ} (hf : ContDiff ℝ (↑⊤) f) (h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x) : AbsolutelyMonotoneOn f s
• iteratedDeriv_mul_pow_sub_of_analytic 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] {k t : ℕ} {z₀ : 𝕜} {R R₁ : 𝕜 → 𝕜} (hf1 : ∀ (z : 𝕜), AnalyticAt 𝕜 R₁ z) (hR₁ : ∀ (z : 𝕜), R z = (z - z₀) ^ (k + t) * R₁ z) : ∃ R₂, (∀ (z : 𝕜), AnalyticAt 𝕜 R₂ z) ∧ ∀ (z : 𝕜), iteratedDeriv k R z = (z - z₀) ^ t * (↑(k + t).factorial / ↑t.factorial * R₁ z + (z - z₀) * R₂ z)
• iteratedDeriv_comp_eq_sum_orderedFinpartition 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ} (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) (hi : ↑i ≤ n) : iteratedDeriv i (g ∘ f) x = ∑ c, iteratedDeriv c.length g (f x) * ∏ j, iteratedDeriv (c.partSize j) f x
• iteratedDeriv_scomp_eq_sum_orderedFinpartition 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ} (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) (hi : ↑i ≤ n) : iteratedDeriv i (g ∘ f) x = ∑ c, (∏ j, iteratedDeriv (c.partSize j) f x) • iteratedDeriv c.length g (f x)
• iteratedDeriv_vcomp_eq_sum_orderedFinpartition 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ} (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) (hi : ↑i ≤ n) : iteratedDeriv i (g ∘ f) x = ∑ c, (iteratedFDeriv 𝕜 c.length g (f x)) fun j => iteratedDeriv (c.partSize j) f x
• iteratedDeriv_comp_two 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {x : 𝕜} (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffAt 𝕜 2 f x) : iteratedDeriv 2 (g ∘ f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x
• iteratedDeriv_scomp_two 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {x : 𝕜} (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffAt 𝕜 2 f x) : iteratedDeriv 2 (g ∘ f) x = deriv f x ^ 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x)
• iteratedDeriv_comp_three 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {x : 𝕜} (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) : iteratedDeriv 3 (g ∘ f) x = iteratedDeriv 3 g (f x) * deriv f x ^ 3 + 3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x + deriv g (f x) * iteratedDeriv 3 f x
• iteratedDeriv_vcomp_two 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E} {x : 𝕜} (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffAt 𝕜 2 f x) : iteratedDeriv 2 (g ∘ f) x = ((iteratedFDeriv 𝕜 2 g (f x)) fun x_1 => deriv f x) + (fderiv 𝕜 g (f x)) (iteratedDeriv 2 f x)
• iteratedDeriv_scomp_three 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {x : 𝕜} (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) : iteratedDeriv 3 (g ∘ f) x = deriv f x ^ 3 • iteratedDeriv 3 g (f x) + 3 • iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x) + iteratedDeriv 3 f x • deriv g (f x)
• iteratedDeriv_vcomp_three 📋 Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E} {x : 𝕜} (hg : ContDiffAt 𝕜 3 g (f x)) (hf : ContDiffAt 𝕜 3 f x) : iteratedDeriv 3 (g ∘ f) x = ((iteratedFDeriv 𝕜 3 g (f x)) fun x_1 => deriv f x) + (iteratedFDeriv 𝕜 2 g (f x)) ![iteratedDeriv 2 f x, deriv f x] + 2 • (iteratedFDeriv 𝕜 2 g (f x)) ![deriv f x, iteratedDeriv 2 f x] + (fderiv 𝕜 g (f x)) (iteratedDeriv 3 f x)
• taylor_mean_remainder_lagrange_iteratedDeriv 📋 Mathlib.Analysis.Calculus.Taylor
  {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ ≠ x) (hf : ContDiffOn ℝ (↑n + 1) f (Set.uIcc x₀ x)) : ∃ x' ∈ Set.uIoo x₀ x, f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial
• InnerProductSpace.laplacian_eq_iteratedDeriv_real 📋 Mathlib.Analysis.InnerProductSpace.Laplacian
  {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {e : ℝ} (f : ℝ → F) : Laplacian.laplacian f e = iteratedDeriv 2 f e
• Complex.taylorSeries_eq_of_entire' 📋 Mathlib.Analysis.Complex.TaylorSeries
  (c z : ℂ) {f : ℂ → ℂ} (hf : Differentiable ℂ f) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
• Complex.taylorSeries_eq_on_ball' 📋 Mathlib.Analysis.Complex.TaylorSeries
  ⦃c : ℂ⦄ ⦃r : ℝ⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.ball c r) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c r)) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
• Complex.taylorSeries_eq_on_eball' 📋 Mathlib.Analysis.Complex.TaylorSeries
  ⦃c : ℂ⦄ ⦃r : ENNReal⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.eball c r)) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
• Complex.hasSum_taylorSeries_of_entire 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ (hf : Differentiable ℂ f) (c z : ℂ) : HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
• Complex.taylorSeries_eq_of_entire 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ (hf : Differentiable ℂ f) (c z : ℂ) : ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
• Complex.hasSum_taylorSeries_on_ball 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄ (hf : DifferentiableOn ℂ f (Metric.ball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.ball c r) : HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
• Complex.taylorSeries_eq_on_ball 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄ (hf : DifferentiableOn ℂ f (Metric.ball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.ball c r) : ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
• Complex.hasSum_taylorSeries_on_eball 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) : HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
• Complex.taylorSeries_eq_on_eball 📋 Mathlib.Analysis.Complex.TaylorSeries
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) : ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
• Differentiable.nonneg_of_iteratedDeriv_nonneg 📋 Mathlib.Analysis.Complex.Positivity
  {f : ℂ → ℂ} (hf : Differentiable ℂ f) {c : ℂ} (h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) : 0 ≤ f z
• Differentiable.apply_le_of_iteratedDeriv_nonneg 📋 Mathlib.Analysis.Complex.Positivity
  {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) : f c ≤ f z
• DifferentiableOn.nonneg_of_iteratedDeriv_nonneg 📋 Mathlib.Analysis.Complex.Positivity
  {f : ℂ → ℂ} {c : ℂ} {r : ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c r)) (h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz₁ : c ≤ z) (hz₂ : z ∈ Metric.ball c r) : 0 ≤ f z
• Differentiable.apply_le_of_iteratedDeriv_alternating 📋 Mathlib.Analysis.Complex.Positivity
  {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : z ≤ c) : f c ≤ f z
• Complex.iteratedDeriv_even_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n) Complex.cosh = Complex.cosh
• Complex.iteratedDeriv_even_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n) Complex.sinh = Complex.sinh
• Real.iteratedDeriv_even_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n) Real.cosh = Real.cosh
• Real.iteratedDeriv_even_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n) Real.sinh = Real.sinh
• Complex.iteratedDeriv_odd_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n + 1) Complex.cosh = Complex.sinh
• Complex.iteratedDeriv_odd_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n + 1) Complex.sinh = Complex.cosh
• Real.iteratedDeriv_odd_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n + 1) Real.cosh = Real.sinh
• Real.iteratedDeriv_odd_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (2 * n + 1) Real.sinh = Real.cosh
• Complex.iteratedDeriv_add_one_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (n + 1) Complex.cosh = iteratedDeriv n Complex.sinh
• Complex.iteratedDeriv_add_one_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (n + 1) Complex.sinh = iteratedDeriv n Complex.cosh
• Real.iteratedDeriv_add_one_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (n + 1) Real.cosh = iteratedDeriv n Real.sinh
• Real.iteratedDeriv_add_one_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : iteratedDeriv (n + 1) Real.sinh = iteratedDeriv n Real.cosh
• Real.iteratedDerivWithin_cosh_Ioo 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n Real.cosh (Set.Ioo a b) x = iteratedDeriv n Real.cosh x
• Real.iteratedDerivWithin_sinh_Ioo 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) {a b x : ℝ} (hx : x ∈ Set.Ioo a b) : iteratedDerivWithin n Real.sinh (Set.Ioo a b) x = iteratedDeriv n Real.sinh x
• Real.iteratedDerivWithin_cosh_Icc 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n Real.cosh (Set.Icc a b) x = iteratedDeriv n Real.cosh x
• Real.iteratedDerivWithin_sinh_Icc 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) {a b : ℝ} (h : a < b) {x : ℝ} (hx : x ∈ Set.Icc a b) : iteratedDerivWithin n Real.sinh (Set.Icc a b) x = iteratedDeriv n Real.sinh x
• Real.differentiable_iteratedDeriv_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : Differentiable ℝ (iteratedDeriv n Real.cosh)
• Real.differentiable_iteratedDeriv_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : Differentiable ℝ (iteratedDeriv n Real.sinh)
• Complex.differentiable_iteratedDeriv_cosh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : Differentiable ℂ (iteratedDeriv n Complex.cosh)
• Complex.differentiable_iteratedDeriv_sinh 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
  (n : ℕ) : Differentiable ℂ (iteratedDeriv n Complex.sinh)
• SchwartzMap.le_seminorm' 📋 Mathlib.Analysis.Distribution.SchwartzSpace.Basic
  (𝕜 : Type u_2) {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap ℝ F) (x : ℝ) : |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
• SchwartzMap.seminorm_le_bound' 📋 Mathlib.Analysis.Distribution.SchwartzSpace.Basic
  (𝕜 : Type u_2) {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap ℝ F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M) : (SchwartzMap.seminorm 𝕜 k n) f ≤ M
• Real.fourier_iteratedDeriv 📋 Mathlib.Analysis.Fourier.FourierTransformDeriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {N : ℕ∞} {n : ℕ} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedDeriv n f) MeasureTheory.volume) (hn : ↑n ≤ N) : FourierTransform.fourier (iteratedDeriv n f) = fun x => (2 * ↑Real.pi * Complex.I * ↑x) ^ n • FourierTransform.fourier f x
• Real.iteratedDeriv_fourier 📋 Mathlib.Analysis.Fourier.FourierTransformDeriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {N : ℕ∞} {n : ℕ} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun x => x ^ n • f x) MeasureTheory.volume) (hn : ↑n ≤ N) : iteratedDeriv n (FourierTransform.fourier f) = FourierTransform.fourier fun x => (-2 * ↑Real.pi * Complex.I * ↑x) ^ n • f x
• PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self 📋 Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
  (L : PeriodPair) (l : ℂ) {n : ℕ} : iteratedDeriv n (L.derivWeierstrassPExcept l) l = ↑(n + 2).factorial * L.sumInvPow l (n + 3)
• PeriodPair.iteratedDeriv_weierstrassPExcept_self 📋 Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
  (L : PeriodPair) (l : ℂ) {n : ℕ} : iteratedDeriv n (L.weierstrassPExcept l) l = if n = 0 then L.weierstrassPExcept l l else ↑(n + 1).factorial * L.sumInvPow l (n + 2)
• eqOn_iteratedDeriv_cotTerm 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  (k d : ℕ) : Set.EqOn (iteratedDeriv k fun z => cotTerm z d) (fun z => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) Complex.integerComplement
• MeasureTheory.iteratedDeriv_charFun_zero 📋 Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ} (hint : MeasureTheory.MemLp id (↑n) μ) : iteratedDeriv n (MeasureTheory.charFun μ) 0 = Complex.I ^ n * ↑(∫ (x : ℝ), x ^ n ∂μ)
• MeasureTheory.iteratedDeriv_charFun 📋 Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ} {t : ℝ} (hint : MeasureTheory.MemLp id (↑n) μ) : iteratedDeriv n (MeasureTheory.charFun μ) t = Complex.I ^ n * ∫ (x : ℝ), ↑x ^ n * Complex.exp (↑t * ↑x * Complex.I) ∂μ
• LSeries_iteratedDeriv 📋 Mathlib.NumberTheory.LSeries.Deriv
  {f : ℕ → ℂ} (m : ℕ) {s : ℂ} (h : LSeries.abscissaOfAbsConv f < ↑s.re) : iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (LSeries.logMul^[m] f) s
• LSeries.iteratedDeriv_alternating 📋 Mathlib.NumberTheory.LSeries.Positivity
  {a : ℕ → ℂ} (hn : 0 ≤ a) {x : ℝ} (h : LSeries.abscissaOfAbsConv a < ↑x) (n : ℕ) : 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) ↑x
• ArithmeticFunction.iteratedDeriv_LSeries_alternating 📋 Mathlib.NumberTheory.LSeries.Positivity
  (a : ArithmeticFunction ℂ) (hn : ∀ (n : ℕ), 0 ≤ a n) {x : ℝ} (h : LSeries.abscissaOfAbsConv ⇑a < ↑x) (n : ℕ) : 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries fun x => a x) ↑x
• UpperHalfPlane.qExpansion_coeff 📋 Mathlib.NumberTheory.ModularForms.QExpansion
  {h : ℝ} (f : UpperHalfPlane → ℂ) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h f) = (↑m.factorial)⁻¹ * iteratedDeriv m (UpperHalfPlane.cuspFunction h f) 0
• ProbabilityTheory.iteratedDeriv_complexMGF 📋 Mathlib.Probability.Moments.ComplexMGF
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (ProbabilityTheory.complexMGF X μ) z = ∫ (x : Ω), (fun ω => ↑(X ω) ^ n * Complex.exp (z * ↑(X ω))) x ∂μ
• ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF 📋 Mathlib.Probability.Moments.ComplexMGF
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ} (hz : z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : HasDerivAt (iteratedDeriv n (ProbabilityTheory.complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * Complex.exp (z * ↑(X ω))) x ∂μ) z
• ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (n : ℕ) : AnalyticOnNhd ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) (interior (ProbabilityTheory.integrableExpSet X μ))
• ProbabilityTheory.analyticOn_iteratedDeriv_mgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (n : ℕ) : AnalyticOn ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) (interior (ProbabilityTheory.integrableExpSet X μ))
• ProbabilityTheory.analyticAt_iteratedDeriv_mgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : AnalyticAt ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) v
• ProbabilityTheory.differentiableAt_iteratedDeriv_mgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : DifferentiableAt ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) v
• ProbabilityTheory.iteratedDeriv_mgf_zero 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (ProbabilityTheory.mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ
• ProbabilityTheory.iteratedDeriv_mgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (ProbabilityTheory.mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * Real.exp (t * X ω)) x ∂μ
• ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (h : v ∈ interior (ProbabilityTheory.integrableExpSet X μ)) : iteratedDeriv 2 (ProbabilityTheory.cgf X μ) v = (∫ (x : Ω), (fun ω => (X ω - deriv (ProbabilityTheory.cgf X μ) v) ^ 2 * Real.exp (v * X ω)) x ∂μ) / ProbabilityTheory.mgf X μ v
• ProbabilityTheory.iteratedDeriv_two_cgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (h : v ∈ interior (ProbabilityTheory.integrableExpSet X μ)) : iteratedDeriv 2 (ProbabilityTheory.cgf X μ) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * Real.exp (v * X ω)) x ∂μ) / ProbabilityTheory.mgf X μ v - deriv (ProbabilityTheory.cgf X μ) v ^ 2
• ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (ht : 0 < t) (hc : ∫ (x : Ω), X x ∂μ = 0) (hs : Set.Icc 0 t ⊆ interior (ProbabilityTheory.integrableExpSet X μ)) : ∃ u ∈ Set.Ioo 0 t, ProbabilityTheory.cgf X μ t = iteratedDeriv 2 (ProbabilityTheory.cgf X μ) u * t ^ 2 / 2
• ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf 📋 Mathlib.Probability.Moments.MGFAnalytic
  {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (ProbabilityTheory.integrableExpSet X μ)) (n : ℕ) : HasDerivAt (iteratedDeriv n (ProbabilityTheory.mgf X μ)) (∫ (x : Ω), (fun ω => X ω ^ (n + 1) * Real.exp (t * X ω)) x ∂μ) t
• ProbabilityTheory.variance_tilted_mul 📋 Mathlib.Probability.Moments.Tilted
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} (ht : t ∈ interior (ProbabilityTheory.integrableExpSet X μ)) : ProbabilityTheory.variance X (μ.tilted fun x => t * X x) = iteratedDeriv 2 (ProbabilityTheory.cgf X μ) t

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59