Integrals of 1-forms along rectifiable curves

The integral ∫ t in a..b, ω (γ t) (deriv γ t) of a 1-form ω against the derivative of a parameter is the right notion only for absolutely continuous curves. A continuous curve of bounded variation can have zero derivative almost everywhere while tracing a circle: compose the circle with the Cantor function. Its derivative integral then vanishes for every 1-form.

The geometric integral TauCeti.rectifiableCurveIntegral ω γ a b of a 1-form ω along a curve γ on [a, b] is instead computed along Mathlib's natural parameterization naturalParameterization γ (Icc a b) a on the length interval [0, L], where L = eVariationOn γ (Icc a b). For a continuous curve of bounded variation this parametrization is 1-Lipschitz, hence absolutely continuous, and it traces the same points with the same multiplicity: γ factors as the natural parameterization composed with cumulative variation.

The integral is meaningful when E is finite-dimensional, where a Lipschitz curve is differentiable almost everywhere and is the integral of its derivative. In an infinite-dimensional space a Lipschitz curve can be nowhere differentiable (for instance t ↦ fun x ↦ |t - x| in C([0, 1], ℝ)), and the formula then gives a junk value. The comparison theorems below therefore assume [FiniteDimensional ℝ E]; the invariance theorems are identities of the formula and hold in every normed space. The invariance and linearity theorems also need no bounded-variation hypothesis: for a curve of infinite length on [a, b], or for b < a, the length interval is [0, 0] and the integral is zero (TauCeti.rectifiableCurveIntegral_of_not_boundedVariationOn, TauCeti.rectifiableCurveIntegral_of_lt).

The main results are:

• TauCeti.rectifiableCurveIntegral_eq_of_eqOn_comp_variationOnFromTo: the integral may be computed along any arclength factor of the curve, such as the one given by BoundedVariationOn.exists_arclength_factorization.
• TauCeti.rectifiableCurveIntegral_congr: the integral only depends on the curve on [a, b].
• TauCeti.rectifiableCurveIntegral_comp_of_monotoneOn: invariance under increasing continuous onto reparametrizations, which need not be absolutely continuous.
• TauCeti.rectifiableCurveIntegral_comp_of_antitoneOn: sign reversal under decreasing ones.
• TauCeti.rectifiableCurveIntegral_neg, TauCeti.rectifiableCurveIntegral_smul, TauCeti.rectifiableCurveIntegral_add and TauCeti.rectifiableCurveIntegral_sub: linearity in the 1-form.
• AbsolutelyContinuousOnInterval.rectifiableCurveIntegral_eq_intervalIntegral_deriv: for an absolutely continuous curve and a 1-form continuous on its trace, the geometric integral is the derivative integral ∫ t in a..b, ω (γ t) (deriv γ t); Path.rectifiableCurveIntegral_extend_eq_curveIntegral compares it with Mathlib's curveIntegral.
• TauCeti.rectifiableCurveIntegral_eq_of_eqOn_comp: independence of the factorization. If γ = η ∘ ψ on [a, b] with η absolutely continuous and ψ continuous and increasing, the geometric integral is the derivative integral of η.

The comparison with absolutely continuous curves uses the absolute continuity of cumulative variation and the reparametrization formula AbsolutelyContinuousOnInterval.integral_oneForm_comp. For a 1-form continuous on the trace, the integrand along the natural parameterization is integrable on the length interval (TauCeti.intervalIntegrable_oneForm_naturalParameterization).

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows, second edition, §1.1 (arclength parametrization of metric curves).

noncomputable def TauCeti.rectifiableCurveIntegral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ω : E → E →L[ℝ] F) (γ : ℝ → E) (a b : ℝ) : F

The geometric integral of a 1-form ω along a curve γ on [a, b]: the integral ∫ u in 0..L, ω (η u) (deriv η u) along the natural parameterization η of γ on its length interval, where L is the total variation of γ on [a, b]. It is meaningful for continuous curves of bounded variation with a ≤ b in a finite-dimensional space E; it then counts the trace with its traversal multiplicity and orientation. In infinite dimensions the natural parameterization need not be differentiable, and the value is junk.

theorem TauCeti.rectifiableCurveIntegral_def {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (ω : E → E →L[ℝ] F) (γ : ℝ → E) (a b : ℝ) : rectifiableCurveIntegral ω γ a b = ∫ (u : ℝ) in 0..(eVariationOn γ (Set.Icc a b)).toReal, (ω (naturalParameterization γ (Set.Icc a b) a u)) (deriv (naturalParameterization γ (Set.Icc a b) a) u)

The defining formula of TauCeti.rectifiableCurveIntegral.

theorem TauCeti.rectifiableCurveIntegral_of_not_boundedVariationOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} (h : ¬BoundedVariationOn γ (Set.Icc a b)) : rectifiableCurveIntegral ω γ a b = 0

The geometric integral along a curve of infinite length on [a, b] is zero.

theorem TauCeti.rectifiableCurveIntegral_of_lt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} (h : b < a) : rectifiableCurveIntegral ω γ a b = 0

The geometric integral on [a, b] with b < a is zero.

@[simp]

theorem TauCeti.rectifiableCurveIntegral_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a : ℝ} : rectifiableCurveIntegral ω γ a a = 0

The geometric integral on a degenerate interval [a, a] is zero.

@[simp]

theorem TauCeti.rectifiableCurveIntegral_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → E} {a b : ℝ} : rectifiableCurveIntegral 0 γ a b = 0

The geometric integral of the zero 1-form is zero.

theorem TauCeti.rectifiableCurveIntegral_eq_of_eqOn_comp_variationOnFromTo {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} (hcont : ContinuousOn γ (Set.Icc a b)) {g : ℝ → E} (hg : Set.EqOn (g ∘ variationOnFromTo γ (Set.Icc a b) a) γ (Set.Icc a b)) : rectifiableCurveIntegral ω γ a b = ∫ (u : ℝ) in 0..(eVariationOn γ (Set.Icc a b)).toReal, (ω (g u)) (deriv g u)

The geometric integral along a continuous curve is the integral along any curve g through which the curve factors by cumulative variation.

@[simp]

theorem TauCeti.rectifiableCurveIntegral_neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} : rectifiableCurveIntegral (-ω) γ a b = -rectifiableCurveIntegral ω γ a b

The geometric integral of the negative of a 1-form is the negative of the geometric integral.

@[simp]

theorem TauCeti.rectifiableCurveIntegral_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} {𝕜 : Type u_3} [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : 𝕜) : rectifiableCurveIntegral (k • ω) γ a b = k • rectifiableCurveIntegral ω γ a b

The geometric integral is homogeneous in the 1-form.

theorem TauCeti.rectifiableCurveIntegral_congr {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} {γ' : ℝ → E} (h : Set.EqOn γ γ' (Set.Icc a b)) : rectifiableCurveIntegral ω γ a b = rectifiableCurveIntegral ω γ' a b

The geometric integral only depends on the curve on [a, b].

theorem TauCeti.rectifiableCurveIntegral_comp_of_monotoneOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b c d : ℝ} (hcont : ContinuousOn γ (Set.Icc a b)) {φ : ℝ → ℝ} (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc c d)) (hφm : MonotoneOn φ (Set.Icc c d)) (hφc : φ c = a) (hφd : φ d = b) : rectifiableCurveIntegral ω (γ ∘ φ) c d = rectifiableCurveIntegral ω γ a b

The geometric integral is invariant under increasing continuous reparametrizations of [c, d] onto [a, b]. The reparametrization need not be absolutely continuous.

theorem TauCeti.rectifiableCurveIntegral_comp_of_antitoneOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b c d : ℝ} (hcont : ContinuousOn γ (Set.Icc a b)) {φ : ℝ → ℝ} (hcd : c ≤ d) (hφ : ContinuousOn φ (Set.Icc c d)) (hφm : AntitoneOn φ (Set.Icc c d)) (hφc : φ c = b) (hφd : φ d = a) : rectifiableCurveIntegral ω (γ ∘ φ) c d = -rectifiableCurveIntegral ω γ a b

The geometric integral changes sign under decreasing continuous reparametrizations of [c, d] onto [a, b]. The reparametrization need not be absolutely continuous.

theorem TauCeti.intervalIntegrable_oneForm_naturalParameterization {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} [FiniteDimensional ℝ E] (hcont : ContinuousOn γ (Set.Icc a b)) (hω : ContinuousOn ω (γ '' Set.Icc a b)) : IntervalIntegrable (fun (u : ℝ) => (ω (naturalParameterization γ (Set.Icc a b) a u)) (deriv (naturalParameterization γ (Set.Icc a b) a) u)) MeasureTheory.volume 0 (eVariationOn γ (Set.Icc a b)).toReal

Along a continuous curve, the integrand of the geometric integral of a 1-form continuous on the trace is integrable on the length interval.

theorem AbsolutelyContinuousOnInterval.rectifiableCurveIntegral_eq_intervalIntegral_deriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hab : a ≤ b) (hω : ContinuousOn ω (γ '' Set.Icc a b)) : TauCeti.rectifiableCurveIntegral ω γ a b = ∫ (t : ℝ) in a..b, (ω (γ t)) (deriv γ t)

For an absolutely continuous curve and a 1-form continuous on its trace, the geometric integral is the integral ∫ t in a..b, ω (γ t) (deriv γ t) against the derivative of the parameter.

theorem TauCeti.rectifiableCurveIntegral_eq_of_eqOn_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {γ : ℝ → E} {a b c d : ℝ} {η : ℝ → E} {ψ : ℝ → ℝ} (hη : AbsolutelyContinuousOnInterval η c d) (hab : a ≤ b) (hψ : ContinuousOn ψ (Set.Icc a b)) (hψm : MonotoneOn ψ (Set.Icc a b)) (hψa : ψ a = c) (hψb : ψ b = d) (h : Set.EqOn (η ∘ ψ) γ (Set.Icc a b)) (hω : ContinuousOn ω (γ '' Set.Icc a b)) : rectifiableCurveIntegral ω γ a b = ∫ (u : ℝ) in c..d, (ω (η u)) (deriv η u)

Independence of the factorization. If a curve factors on [a, b] as an absolutely continuous curve η on [c, d] composed with a continuous increasing map of [a, b] onto [c, d], then its geometric integral against a 1-form continuous on its trace is the integral along η against the derivative of η.

theorem TauCeti.rectifiableCurveIntegral_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → E} {a b : ℝ} {ω₁ ω₂ : E → E →L[ℝ] F} (hcont : ContinuousOn γ (Set.Icc a b)) (hω₁ : ContinuousOn ω₁ (γ '' Set.Icc a b)) (hω₂ : ContinuousOn ω₂ (γ '' Set.Icc a b)) : rectifiableCurveIntegral (ω₁ + ω₂) γ a b = rectifiableCurveIntegral ω₁ γ a b + rectifiableCurveIntegral ω₂ γ a b

The geometric integral along a continuous curve is additive in 1-forms continuous on the trace.

theorem TauCeti.rectifiableCurveIntegral_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : ℝ → E} {a b : ℝ} {ω₁ ω₂ : E → E →L[ℝ] F} (hcont : ContinuousOn γ (Set.Icc a b)) (hω₁ : ContinuousOn ω₁ (γ '' Set.Icc a b)) (hω₂ : ContinuousOn ω₂ (γ '' Set.Icc a b)) : rectifiableCurveIntegral (ω₁ - ω₂) γ a b = rectifiableCurveIntegral ω₁ γ a b - rectifiableCurveIntegral ω₂ γ a b

The geometric integral along a continuous curve of a difference of 1-forms continuous on the trace is the difference of the geometric integrals.

theorem Path.rectifiableCurveIntegral_extend_eq_curveIntegral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : E → E →L[ℝ] F} {x y : E} (γ : Path x y) (hγ : AbsolutelyContinuousOnInterval (⇑γ.extend) 0 1) (hω : ContinuousOn ω (Set.range ⇑γ)) : TauCeti.rectifiableCurveIntegral ω (⇑γ.extend) 0 1 = ∫ᶜ (z : E) in γ, ω z

For a path whose extension is absolutely continuous on [0, 1] and a 1-form continuous on its range, the geometric integral is Mathlib's curveIntegral.