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

def nhdsSetWithin {X : Type u_1} [TopologicalSpace X] (s t : Set X) : Filter X

The "neighbourhood within" filter for sets. Elements of 𝓝[t] s are sets containing the intersection of t and a neighbourhood of s.

Equations

• nhdsSetWithin s t = nhdsSet s ⊓ Filter.principal t

def Topology.«term𝓝ˢ[_]_» : Lean.ParserDescr

The "neighbourhood within" filter for sets. Elements of 𝓝[t] s are sets containing the intersection of t and a neighbourhood of s.

Equations

• One or more equations did not get rendered due to their size.

theorem nhdsSetWithin_mono_left {X : Type u_1} [TopologicalSpace X] {s s' t : Set X} (h : s ⊆ s') : nhdsSetWithin s t ≤ nhdsSetWithin s' t

theorem nhdsSetWithin_mono_right {X : Type u_1} [TopologicalSpace X] {s t t' : Set X} (h : t ⊆ t') : nhdsSetWithin s t ≤ nhdsSetWithin s t'

theorem nhdsSetWithin_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : Sort u_3} {p : ι → Prop} {s' : ι → Set X} {s : Set X} (h : (nhdsSet s).HasBasis p s') (t : Set X) : (nhdsSetWithin s t).HasBasis p fun (i : ι) => s' i ∩ t

theorem nhdsSetWithin_basis_open {X : Type u_1} [TopologicalSpace X] (s t : Set X) : (nhdsSetWithin s t).HasBasis (fun (u : Set X) => IsOpen u ∧ s ⊆ u) fun (u : Set X) => u ∩ t

theorem mem_nhdsSetWithin {X : Type u_1} [TopologicalSpace X] {s t u : Set X} : u ∈ nhdsSetWithin s t ↔ ∃ (v : Set X), IsOpen v ∧ s ⊆ v ∧ v ∩ t ⊆ u

@[simp]

theorem nhdsSetWithin_singleton {X : Type u_1} [TopologicalSpace X] {x : X} {s : Set X} : nhdsSetWithin {x} s = nhdsWithin x s

@[simp]

theorem nhdsSetWithin_univ {X : Type u_1} [TopologicalSpace X] {s : Set X} : nhdsSetWithin s Set.univ = nhdsSet s

@[simp]

theorem nhdsSetWithin_self {X : Type u_1} [TopologicalSpace X] {s : Set X} : nhdsSetWithin s s = Filter.principal s

theorem ContinuousOn.preimage_mem_nhdsSetWithin {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : ContinuousOn f s) {t u t' : Set Y} (h : u ∈ nhdsSetWithin t t') : f ⁻¹' u ∈ nhdsSetWithin (s ∩ f ⁻¹' t) (s ∩ f ⁻¹' t')

theorem ContinuousOn.preimage_mem_nhdsSetWithin_of_mem_nhdsSet {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : ContinuousOn f s) {t u : Set Y} (h : u ∈ nhdsSet t) : f ⁻¹' u ∈ nhdsSetWithin (s ∩ f ⁻¹' t) s

If f is continuous on s and u is a neighbourhood of t, then f ⁻¹' u is a neighbourhood of s ∩ f ⁻¹' t within s.

theorem nhdsSetWithin_prod_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} {t t' : Set Y} : nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') ≤ nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'

theorem IsCompact.nhdsSetWithin_prod_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} {t t' : Set Y} (hs : IsCompact s) (ht : IsCompact t) : nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') = nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'

theorem generalized_tube_lemma' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} (hs : IsCompact s) {t t' : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t')) : ∃ u ∈ nhdsSetWithin s s', ∃ v ∈ nhdsSetWithin t t', u ×ˢ v ⊆ n

Variant of generalized_tube_lemma in terms of nhdsSetWithin.

theorem generalized_tube_lemma_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s s' : Set X} (hs : IsCompact s) {t : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s' ×ˢ t)) : ∃ u ∈ nhdsSetWithin s s', u ×ˢ t ⊆ n

Variant of generalized_tube_lemma that only replaces the set in one direction.

theorem generalized_tube_lemma_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsCompact s) {t t' : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : n ∈ nhdsSetWithin (s ×ˢ t) (s ×ˢ t')) : ∃ u ∈ nhdsSetWithin t t', s ×ˢ u ⊆ n

Variant of generalized_tube_lemma that only replaces the set in one direction.

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