Calculus on spaces of continuous maps

This file develops bounded pointwise operations for differentiating superposition maps, together with bounded integration operators on continuous paths for constructing Picard residuals.

Main results

• ContinuousMap.applyContinuousLinearMap: pointwise application of a continuous family of continuous linear maps, as a bounded bilinear operator.
• ContinuousMap.hasFDerivAt_postcomp: the derivative of pointwise postcomposition by a C¹ map.
• ContinuousMap.contDiff_postcomp: finite-order or smooth pointwise postcomposition.
• ContinuousMap.unitIntervalIntegral: the Volterra integral operator on continuous paths over the unit interval.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map".

noncomputable def ContinuousMap.applyContinuousLinearMap {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] : C(K, E →L[𝕜] F) →L[𝕜] C(K, E) →L[𝕜] C(K, F)

Pointwise application of a continuous family of continuous linear maps to a continuous map, as a bounded bilinear operator.

Equations

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

@[simp]

theorem ContinuousMap.applyContinuousLinearMap_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (A : C(K, E →L[𝕜] F)) (f : C(K, E)) (x : K) : ((applyContinuousLinearMap A) f) x = (A x) (f x)

noncomputable def ContinuousMap.intervalIntegralOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (hab : a ≤ b) : C(↑(Set.Icc a b), E) →L[ℝ] C(↑(Set.Icc a b), E)

Volterra integration as a continuous linear operator on continuous paths over an arbitrary compact real interval. The input is extended constantly outside the interval before integration.

Equations

• ContinuousMap.intervalIntegralOperator a b hab = { toFun := ContinuousMap.intervalPrimitive✝ a b, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (b - a) ⋯

theorem ContinuousMap.norm_intervalIntegralOperator_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (hab : a ≤ b) : ‖intervalIntegralOperator a b hab‖ ≤ b - a

The Volterra integral operator on [a, b] has operator norm at most the interval length.

@[simp]

theorem ContinuousMap.intervalIntegralOperator_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) (hab : a ≤ b) (f : C(↑(Set.Icc a b), E)) (t : ↑(Set.Icc a b)) : ((intervalIntegralOperator a b hab) f) t = ∫ (s : ℝ) in a..↑t, f (Set.projIcc a b hab s)

Evaluating the Volterra operator at t integrates the input's constant extension from the left endpoint to t.

noncomputable def ContinuousMap.unitIntervalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : C(↑(Set.Icc 0 1), E) →L[ℝ] C(↑(Set.Icc 0 1), E)

Volterra integration on the unit interval, obtained from the general compact-interval operator.

Equations

• ContinuousMap.unitIntervalIntegral = ContinuousMap.intervalIntegralOperator 0 1 ⋯

theorem ContinuousMap.norm_unitIntervalIntegral_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : ‖unitIntervalIntegral‖ ≤ 1

The Volterra integral operator on the unit interval has operator norm at most one.

@[simp]

theorem ContinuousMap.unitIntervalIntegral_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : C(↑(Set.Icc 0 1), E)) (t : ↑(Set.Icc 0 1)) : (unitIntervalIntegral f) t = ∫ (s : ℝ) in 0..↑t, f (Set.projIcc 0 1 ⋯ s)

Evaluating the Volterra operator at t integrates the input's constant extension from zero to t.

theorem ContinuousMap.hasFDerivAt_postcomp {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type (max u v)} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : C(E, F)) (hf : ContDiff 𝕜 1 ⇑f) (g : C(K, E)) : HasFDerivAt (fun (h : C(K, E)) => f.comp h) (applyContinuousLinearMap ({ toFun := fderiv 𝕜 ⇑f, continuous_toFun := ⋯ }.comp g)) g

Pointwise postcomposition by a C¹ map is Fréchet differentiable. Its derivative applies the derivative of the original map pointwise along the input function.

theorem ContinuousMap.contDiff_postcomp {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type (max u v)} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ∞) (f : C(E, F)) (hf : ContDiff 𝕜 ↑n ⇑f) : ContDiff 𝕜 ↑n fun (g : C(K, E)) => f.comp g

Pointwise postcomposition by a C^n map is C^n on a compact-domain continuous-map space, for every finite or infinite differentiability order n.