Smooth Hadamard factorization

This file develops the first-order factorization of a smooth map through displacement from a basepoint. It is the analytic input for identifying point derivations on a finite-dimensional smooth manifold with tangent vectors.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The Lie algebra and the tangent space at 1".

noncomputable def segmentAverage {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (w : ℝ → ℝ) (g : E → F) (x v : E) : F

The weighted average of g along the segment from x to x + v.

Equations

• segmentAverage w g x v = ∫ (t : ℝ) in 0..1, w t • g (x + t • v)

theorem segmentAverage_eq_integral_Icc {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (w : ℝ → ℝ) (g : E → F) (x : E) : segmentAverage w g x = fun (v : E) => ∫ (t : ℝ) in Set.Icc 0 1, w t • g (x + t • v)

A weighted segment average written as an integral over the compact unit interval.

theorem ContDiff.contDiff_segmentAverage {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {n : ℕ∞} {w : ℝ → ℝ} {g : E → F} (hw : ContDiff ℝ (↑n) w) (hg : ContDiff ℝ (↑n) g) (x : E) : ContDiff ℝ (↑n) (segmentAverage w g x)

A weighted segment average depends smoothly on its displacement when its weight and integrand are smooth.

theorem ContinuousLinearMap.segmentAverage_apply {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (L : F →L[ℝ] G) (w : ℝ → ℝ) (g : E → F) (x v : E) (h : IntervalIntegrable (fun (t : ℝ) => w t • g (x + t • v)) MeasureTheory.volume 0 1) : L (segmentAverage w g x v) = ∫ (t : ℝ) in 0..1, L (w t • g (x + t • v))

A continuous linear map commutes with a weighted segment average.

@[simp]

theorem segmentAverage_zero {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (w : ℝ → ℝ) (g : E → F) (x : E) : segmentAverage w g x 0 = (∫ (t : ℝ) in 0..1, w t) • g x

At zero displacement, a weighted segment average is the integral of the weight times the value of the integrand at the basepoint.

noncomputable def hadamardFactor {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x y : E) : E →L[ℝ] F

The averaged derivative along the segment from x to y.

Equations

• hadamardFactor f x y = segmentAverage (fun (x : ℝ) => 1) (fderiv ℝ f) x (y - x)

theorem hadamardFactor_eq_integral_Icc {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x : E) : hadamardFactor f x = fun (y : E) => ∫ (t : ℝ) in Set.Icc 0 1, fderiv ℝ f (x + t • (y - x))

The averaged derivative written as an integral over the compact unit interval.

@[simp]

theorem hadamardFactor_self {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (x : E) : hadamardFactor f x x = fderiv ℝ f x

At the basepoint, the averaged derivative is the ordinary derivative.

theorem ContDiff.contDiff_hadamardFactor_of_succ {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (n : ℕ∞) (f : E → F) (hf : ContDiff ℝ (↑n + 1) f) (x : E) : ContDiff ℝ (↑n) (hadamardFactor f x)

If f is n + 1 times continuously differentiable, its Hadamard factor is n times continuously differentiable in the endpoint.

theorem ContDiff.sub_eq_hadamardFactor_apply {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (hf : ContDiff ℝ 1 f) (x y : E) : f y - f x = (hadamardFactor f x y) (y - x)

First-order Taylor expansion along a segment, with its coefficient bundled as a continuous linear map.

theorem ContDiff.contDiff_hadamardFactor {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : E → F) (hf : ContDiff ℝ (↑⊤) f) (x : E) : ContDiff ℝ (↑⊤) (hadamardFactor f x)

For a smooth function, the averaged derivative in Hadamard's factorization depends smoothly on the endpoint.