Canonical oriented interval integration

Pullback along the actual inclusion of [a,b] gives a top form on Mathlib's interval manifold. The left/right coordinate derivatives and chart signs compensate, and the normalized Euclidean line measure is real Lebesgue measure. The canonical integral therefore equals ∫ t in a..b.

theorem TauCeti.inChartAt_mpullback_subtypeVal_Icc {a b : ℝ} [hab : Fact (a < b)] (ω : RoughForm (modelWithCornersSelf ℝ ℝ) ℝ ℝ 1) (α : ↑(Set.Icc a b)) {z : EuclideanSpace ℝ (Fin 1)} (hz : z ∈ (extChartAt (modelWithCornersEuclideanHalfSpace 1) α).target) : ((mpullback (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) Subtype.val ω).inChartAt α z) ⇑(EuclideanSpace.basisFun (Fin 1) ℝ).toBasis = (if ↑α < b then 1 else -1) * (ω ↑(↑(extChartAt (modelWithCornersEuclideanHalfSpace 1) α).symm z)) fun (x : Fin 1) => 1

The actual pullback coefficient of a real one-form in an interval chart is its real coefficient multiplied by that chart's inclusion derivative.

theorem TauCeti.integralTopForm_mpullback_subtypeVal_Icc {a b : ℝ} [hab : Fact (a < b)] (ω : RoughForm (modelWithCornersSelf ℝ ℝ) ℝ ℝ 1) (hf : IntervalIntegrable (fun (t : ℝ) => (ω t) fun (x : Fin 1) => 1) MeasureTheory.volume a b) : IntegrableTopForm (mpullback (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) Subtype.val ω) ∧ integralTopForm (Manifold.Orientation.interval a b) (mpullback (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) Subtype.val ω) = ∫ (t : ℝ) in a..b, (ω t) fun (x : Fin 1) => 1

Actual pullback of an interval-integrable real one-form is intrinsically integrable, and its canonical increasing-orientation integral is the ordinary interval integral.

theorem TauCeti.integralTopForm_mpullback_curve_Icc {a b : ℝ} [hab : Fact (a < b)] {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (ω : RoughForm (modelWithCornersSelf ℝ X) X ℝ 1) (γ : ℝ → X) (hγ : ContDiffOn ℝ 1 γ (Set.Icc a b)) (hf : IntervalIntegrable (fun (t : ℝ) => (ω (γ t)) fun (x : Fin 1) => (NormedSpace.fromTangentSpace (γ t)).symm (deriv γ t)) MeasureTheory.volume a b) : IntegrableTopForm (mpullback (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ X) (fun (t : ↑(Set.Icc a b)) => γ ↑t) ω) ∧ integralTopForm (Manifold.Orientation.interval a b) (mpullback (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ X) (fun (t : ↑(Set.Icc a b)) => γ ↑t) ω) = ∫ (t : ℝ) in a..b, (ω (γ t)) fun (x : Fin 1) => (NormedSpace.fromTangentSpace (γ t)).symm (deriv γ t)

Integration of the actual manifold pullback along a model-valued curve that is C1 on the closed interval is its raw velocity integral. Endpoint derivatives are read within the interval; they agree with ordinary derivatives at every interior point.