Chart integral comparison with ordinary manifold pullback

The coordinate expression uses derivatives within the model range. Ordinary pullback uses the unrestricted manifold derivative, and the two can differ at boundary points. The model range is convex, so its frontier is Haar-null. They agree almost everywhere on every preferred-chart target, giving the actual integral and integrability comparison required by chart integration.

theorem TauCeti.RoughForm.inChartAt_ae_eq_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} (φ : RoughForm I M ℝ k) (α : M) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] : ∀ᵐ (y : E) ∂μ.restrict (extChartAt I α).target, φ.inChartAt α y = mpullback (modelWithCornersSelf ℝ E) I (↑(extChartAt I α).symm) φ y

The within-range chart expression equals ordinary pullback almost everywhere on the target. No pointwise equality is claimed on the model boundary.

theorem TauCeti.Manifold.OrientationLift.signedInChartAt_ae_eq_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] : ∀ᵐ (y : E) ∂μ.restrict (extChartAt I α).target, φ.signedInChartAt b α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => l.signAt α ↑x) y = ↑↑(l.signAt α (↑(extChartAt I α).symm y)) * (mpullback (modelWithCornersSelf ℝ E) I (↑(extChartAt I α).symm) φ y) ⇑b

The actual source-signed coefficient agrees almost everywhere with the characteristic ordinary-pullback coefficient. The possible difference on model-boundary points is Haar-null.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_eq_integral_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) : l.chartIntegral φ α = ↑↑(l.modelOrientation.signBasis b) * ∫ (y : E) in (extChartAt I α).target, ↑↑(l.signAt α (↑(extChartAt I α).symm y)) * (mpullback (modelWithCornersSelf ℝ E) I (↑(extChartAt I α).symm) φ y) ⇑b ∂b.addHaar

The chart functional equals the ordinary-pullback target integral, with a relative basis sign. The characteristic formula also covers negative model orientation in dimension zero.

theorem TauCeti.Manifold.OrientationLift.integrable_signedInChartAt_iff_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] : MeasureTheory.Integrable (φ.signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => l.signAt α ↑x) μ ↔ MeasureTheory.IntegrableOn (fun (y : E) => ↑↑(l.signAt α (↑(extChartAt I α).symm y)) * (mpullback (modelWithCornersSelf ℝ E) I (↑(extChartAt I α).symm) φ y) ⇑b) (extChartAt I α).target μ

Genuine integrability of the signed chart coefficient is equivalent to integrability of the ordinary-pullback coefficient on the target, with both integrability statements retained.