Compact-parameter integration

This file uses Mathlib's continuity theorem for parameterized interval integrals and proves that integration over the compact unit interval preserves differentiation and continuous differentiability in a normed-space parameter. Continuous differentiability is preserved at every finite or infinite order and with independent domain and codomain universes.

These results supply the analytic regularity used by smooth Hadamard factorization, a prerequisite for the point-derivation/tangent-space equivalence in the Lie groups roadmap.

The file also differentiates a parametrized interval integral x ↦ ∫ t in a..b, G (x, t) in a real parameter x at a point x₀, assuming only that G is C¹ on an open set containing the compact segment {x₀} × [a, b]: the derivative is the integral of the partial derivative of G in x.

Finally, for a compact parameter space α mapped continuously into a normed space P by ι, an integrable weight g on α, and F that is C^n on an open set W ⊆ E × P, the integral x ↦ ∫ y, g y • F (x, ι y) ∂μ is C^n on every open set U with U × ι(α) ⊆ W (TauCeti.contDiffOn_integral_smul_of_contDiffOn), with derivative the integral of the partial derivatives of F in x (TauCeti.hasFDerivAt_integral_smul_of_contDiffOn). The weight need not be continuous; this is the regularity of kernel integrals such as the Poisson integral of integrable boundary data on a sphere.

References

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

theorem hasFDerivAt_integral_Icc_of_contDiff {E : Type u} {F : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (h : E → ℝ → F) (hh : ContDiff ℝ 1 (Function.uncurry h)) (x₀ : E) : HasFDerivAt (fun (x : E) => ∫ (t : ℝ) in Set.Icc 0 1, h x t) (∫ (t : ℝ) in Set.Icc 0 1, fderiv ℝ (Function.uncurry h) (x₀, t) ∘SL ContinuousLinearMap.inl ℝ E ℝ) x₀

Differentiation under an integral over the compact unit interval for a continuously differentiable parameterized function.

theorem contDiff_integral_Icc_of_contDiff {V : Type u} {W : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] (n : ℕ∞) (h : V → ℝ → W) (hh : ContDiff ℝ (↑n) (Function.uncurry h)) : ContDiff ℝ ↑n fun (x : V) => ∫ (t : ℝ) in Set.Icc 0 1, h x t

Integration over the compact unit interval preserves continuous differentiability of any possibly infinite order in a parameter.

theorem TauCeti.hasDerivAt_intervalIntegral_of_contDiffOn {F : Type v} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : ℝ × ℝ → F} {U : Set (ℝ × ℝ)} (hU : IsOpen U) (hG : ContDiffOn ℝ 1 G U) {x₀ a b : ℝ} (hsub : {x₀} ×ˢ Set.uIcc a b ⊆ U) : IntervalIntegrable (fun (t : ℝ) => (fderiv ℝ G (x₀, t)) (1, 0)) MeasureTheory.volume a b ∧ HasDerivAt (fun (x : ℝ) => ∫ (t : ℝ) in a..b, G (x, t)) (∫ (t : ℝ) in a..b, (fderiv ℝ G (x₀, t)) (1, 0)) x₀

Differentiation under a parametrized interval integral. If G is C¹ on an open set containing the segment {x₀} × [a, b], then the partial derivative of G in the first variable is interval integrable along that segment, and x ↦ ∫ t in a..b, G (x, t) is differentiable at x₀ with derivative the integral of this partial derivative.

Integration against a weight over a compact parameter space

theorem ContDiffOn.fderiv_partial_of_isOpen {E : Type u} {P : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] {W : Set (E × P)} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {F : E × P → G} {m : WithTop ℕ∞} (hF : ContDiffOn ℝ (m + 1) F W) (hW : IsOpen W) : ContDiffOn ℝ m (fun (p : E × P) => fderiv ℝ (fun (x : E) => F (x, p.2)) p.1) W

Partial derivatives in the first variable. If F is C^(m+1) on an open set W ⊆ E × P, then the derivative of x ↦ F (x, p.2) at p.1 is C^m in p on W.

theorem TauCeti.integrable_smul_of_continuousOn {E : Type u} {P : Type u_1} {α : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup P] [TopologicalSpace α] [CompactSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : α → P} {g : α → ℝ} {W : Set (E × P)} {H : Type u_3} [NormedAddCommGroup H] [NormedSpace ℝ H] {F : E × P → H} (hg : MeasureTheory.Integrable g μ) (hι : Continuous ι) (hF : ContinuousOn F W) {x : E} (hx : ∀ (y : α), (x, ι y) ∈ W) : MeasureTheory.Integrable (fun (y : α) => g y • F (x, ι y)) μ

An integrable weight on a compact space times a function continuous along {x} × ι(α) is integrable.

theorem TauCeti.continuousAt_integral_smul_of_continuousOn {E : Type u} {P : Type u_1} {α : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup P] [TopologicalSpace α] [CompactSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : α → P} {g : α → ℝ} {W : Set (E × P)} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {F : E × P → G} (hg : MeasureTheory.Integrable g μ) (hι : Continuous ι) (hW : IsOpen W) (hF : ContinuousOn F W) {x₀ : E} (hx₀ : ∀ (y : α), (x₀, ι y) ∈ W) : ContinuousAt (fun (x : E) => ∫ (y : α), g y • F (x, ι y) ∂μ) x₀

Integration against an integrable weight over a compact parameter space is continuous in a parameter x of the integrand, at any x₀ with {x₀} × ι(α) inside the open set where the integrand is continuous.

theorem TauCeti.hasFDerivAt_integral_smul_of_contDiffOn {E : Type u} {P : Type u_1} {α : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [TopologicalSpace α] [CompactSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : α → P} {g : α → ℝ} {W : Set (E × P)} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {F : E × P → G} (hg : MeasureTheory.Integrable g μ) (hι : Continuous ι) (hW : IsOpen W) (hF : ContDiffOn ℝ 1 F W) {x₀ : E} (hx₀ : ∀ (y : α), (x₀, ι y) ∈ W) : HasFDerivAt (fun (x : E) => ∫ (y : α), g y • F (x, ι y) ∂μ) (∫ (y : α), g y • fderiv ℝ (fun (x : E) => F (x, ι y)) x₀ ∂μ) x₀

Differentiation under the integral sign over a compact parameter space. If F is C¹ on an open set W ⊆ E × P containing {x₀} × ι(α), then integrating F (x, ι y) against an integrable weight g is differentiable at x₀, with derivative the integral of the partial derivative of F in x.

theorem TauCeti.contDiffOn_integral_smul_of_contDiffOn {E : Type u} {P : Type u_1} {α : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup P] [NormedSpace ℝ P] [TopologicalSpace α] [CompactSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : α → P} {g : α → ℝ} {W : Set (E × P)} {G : Type v} [NormedAddCommGroup G] [NormedSpace ℝ G] {n : ℕ∞} {F : E × P → G} (hg : MeasureTheory.Integrable g μ) (hι : Continuous ι) (hW : IsOpen W) (hF : ContDiffOn ℝ (↑n) F W) {U : Set E} (hU : IsOpen U) (hUW : ∀ x ∈ U, ∀ (y : α), (x, ι y) ∈ W) : ContDiffOn ℝ (↑n) (fun (x : E) => ∫ (y : α), g y • F (x, ι y) ∂μ) U

Smoothness of integrals over a compact parameter space. If F is C^n on an open set W ⊆ E × P and {x} × ι(α) ⊆ W for every x in an open set U, then integrating F (x, ι y) against an integrable weight g is C^n in x on U.