Hadamard's lemma

Here we prove variants of Hadamard's lemma, stating that a smooth function f : E → F between sufficiently nice vector spaces can for any point x and basis b be written as y ↦ f x + ∑ i, b.repr (y - x) i • g i y where b.repr (y - x) i is the i-th component of y - x in the basis b and each g i is a smooth function E → F. We do this by providing explicit functions hadamardFun f x (b i) to serve as the g i, characterising their smoothness and showing that f can be written in terms of them.

The functions we consider are specifically functions from finite-dimensional spaces to Banach spaces that are continuously differentiable on an open star-convex set.

See https://en.wikipedia.org/wiki/Hadamard%27s_lemma and https://ncatlab.org/nlab/show/Hadamard+lemma.

theorem ContinuousOn.intervalIntegral {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_1} [TopologicalSpace X] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NoAtoms μ] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : X × ℝ → E} {u : Set X} {a₀ b₀ : ℝ} (hf : ContinuousOn f (u ×ˢ Set.uIcc a₀ b₀)) : ContinuousOn (fun (x : X) => ∫ (t : ℝ) in a₀..b₀, f (x, t) ∂μ) u

theorem intervalIntegral.hasFDerivAt_integral_of_contDiffOn {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℝ E] {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H × ℝ → E} {x₀ : H} {u : Set H} (hu : u ∈ nhds x₀) {a b : ℝ} (hF : ContDiffOn ℝ 1 f (u ×ˢ Set.uIcc a b)) : HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..b, f (x, t) ∂μ) (∫ (t : ℝ) in a..b, fderiv ℝ (fun (x : H) => f (x, t)) x₀ ∂μ) x₀

A convenient special case of intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le: if f : H × ℝ → E is continuously differentiable on u ×ˢ [[a, b]] for a neighbourhood u of x₀, then a derivative of fun x => ∫ t in a..b, f (x, t) ∂μ in x₀ can be computed as ∫ t in a..b, fderiv ℝ (fun x ↦ f (x, t)) x₀ ∂μ.

theorem ContDiffOn.intervalIntegral {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.NoAtoms μ] {f : E × ℝ → F} {u : Set E} (hu : IsOpen u) {a b : ℝ} {n : ℕ∞} (hf : ContDiffOn ℝ (↑n) f (u ×ˢ Set.uIcc a b)) : ContDiffOn ℝ (↑n) (fun (x : E) => ∫ (t : ℝ) in a..b, f (x, t) ∂μ) u

noncomputable def hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] (f : E → F) (x b : E) : E → F

The function appearing in Hadamard's lemma applied to the function f at x for a basis vector b.

Equations

• hadamardFun f x b y = ∫ (t : ℝ) in 0..1, lineDeriv ℝ f (x + t • (y - x)) b

theorem ContDiffOn.hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {x : E} {s : Set E} (hs : IsOpen s) (hs' : StarConvex ℝ x s) {f : E → F} {n m : ℕ∞} (hf : ContDiffOn ℝ (↑n) f s) (hm : m + 1 ≤ n) (b : E) : ContDiffOn ℝ (↑m) (hadamardFun f x b) s

theorem ContDiff.hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E → F} {n m : ℕ∞} (hf : ContDiff ℝ (↑n) f) (hm : m + 1 ≤ n) (x b : E) : ContDiff ℝ (↑m) (hadamardFun f x b)

theorem eqOn_add_sum_hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace F] {x : E} {s : Set E} (hs : IsOpen s) (hs' : StarConvex ℝ x s) {f : E → F} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n f s) (hn : 1 ≤ n) {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℝ E) : Set.EqOn f (fun (y : E) => f x + ∑ i : ι, (b.repr (y - x)) i • hadamardFun f x (b i) y) s

theorem eq_add_sum_hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [CompleteSpace F] {x : E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiff ℝ n f) (hn : 1 ≤ n) {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℝ E) : f = fun (y : E) => f x + ∑ i : ι, (b.repr (y - x)) i • hadamardFun f x (b i) y