Hadamard's lemma

Here we restate Hadamard's lemma in terms of the API around DSmoothMap.

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

noncomputable def DSmoothMap.hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [DiffeologicalSpace E] [DiffeologicalSpace F] [ContDiffCompatible E] [ContDiffCompatible F] [FiniteDimensional ℝ E] (f : DSmoothMap E F) (x b : E) : DSmoothMap E F

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

Equations

• f.hadamardFun x b = { toFun := hadamardFun (⇑f) x b, dsmooth := ⋯ }

theorem ContinuousLinearMap.dsmooth {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [DiffeologicalSpace E] [DiffeologicalSpace F] [ContDiffCompatible E] [ContDiffCompatible F] [FiniteDimensional ℝ E] (f : E →L[ℝ] F) : DSmooth ⇑f

def ContinuousLinearMap.toDSmoothMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [DiffeologicalSpace E] [DiffeologicalSpace F] [ContDiffCompatible E] [ContDiffCompatible F] [FiniteDimensional ℝ E] (f : E →L[ℝ] F) : DSmoothMap E F

Equations

• f.toDSmoothMap = { toFun := ⇑f, dsmooth := ⋯ }

@[simp]

theorem ContinuousLinearMap.toDSmoothMap_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [DiffeologicalSpace E] [DiffeologicalSpace F] [ContDiffCompatible E] [ContDiffCompatible F] [FiniteDimensional ℝ E] (f : E →L[ℝ] F) (a : E) : f.toDSmoothMap a = f a

theorem DSmoothMap.eq_add_sum_hadamardFun {E F : Type u} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] [DiffeologicalSpace E] [DiffeologicalSpace F] [ContDiffCompatible E] [ContDiffCompatible F] [FiniteDimensional ℝ E] [CompleteSpace F] (f : DSmoothMap E F) (x : E) {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℝ E) : f = const E (f x) + ∑ i : ι, ((LinearMap.toContinuousLinearMap (b.coord i)).toDSmoothMap - const E ((b.repr x) i)) • f.hadamardFun x (b i)