Integrability of compactly supported continuous top forms

A finite open chart cover with compact coordinate bounds controls each local coefficient. Unsigned Jacobian transport then gives integrability on every preferred chart, using only the model's Borel measurable structure. No Hausdorff or orientation assumption on the manifold is needed; a model basis records the actual top degree.

The resulting chart formula characterizes the oriented integral of such forms; on a finite-dimensional normed space with a constant orientation it is the Haar integral of the coefficient in a positively oriented basis. On ℝ with its standard orientation TauCeti.Manifold.Orientation.real it is the Lebesgue integral of the value on 1 (TauCeti.integralTopForm_real_eq_integral).

theorem TauCeti.IsSmoothForm.integrableTopForm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {k : ℕ} {n : WithTop ℕ∞} {φ : RoughForm I M ℝ k} (hφ : IsSmoothForm I n φ) (hc : IsCompact (tsupport φ)) (b : Module.Basis (Fin k) ℝ E) : IntegrableTopForm φ

A compactly supported C0 top form satisfies the canonical integrability predicate. The explicit basis records the degree; the model's Borel structure is used only internally.

theorem TauCeti.IsSmoothForm.integrable_signedInChartAt_one {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {k : ℕ} {n : WithTop ℕ∞} {φ : RoughForm I M ℝ k} (hφ : IsSmoothForm I n φ) (hc : IsCompact (tsupport φ)) (b : Module.Basis (Fin k) ℝ E) (α : M) : MeasureTheory.Integrable (φ.signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => 1) b.addHaar

Every positive signed preferred-chart coefficient of a compactly supported C0 form is integrable, including when the manifold is nonorientable or non-Hausdorff.

theorem TauCeti.integralTopForm_of_tsupport_subset_chart {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] [IsManifold I 1 M] {k : ℕ} {φ : RoughForm I M ℝ k} (l : Manifold.OrientationLift I M (Fin k)) (hφ : IsSmoothForm I 0 φ) (hc : IsCompact (tsupport φ)) (α : M) (hs : tsupport φ ⊆ (chartAt H α).source) (b : Module.Basis (Fin k) ℝ E) (hb : b.orientation = l.modelOrientation) : integralTopForm (Manifold.Orientation.mk l) φ = ∫ (y : E) in (extChartAt I α).target, ↑↑(l.signAt α (↑(extChartAt I α).symm y)) * (mpullback (modelWithCornersSelf ℝ E) I (↑(extChartAt I α).symm) φ y) ⇑b ∂b.addHaar

The characteristic equation for compactly supported C0 top forms in a preferred chart. The coefficient uses the actual ordinary manifold pullback; its possible boundary difference from the within-range chart expression is Haar-null.

theorem TauCeti.integralTopForm_model_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {k : ℕ} (o : Orientation ℝ E (Fin k)) (hk : Fintype.card (Fin k) = Module.finrank ℝ E) {φ : RoughForm (modelWithCornersSelf ℝ E) E ℝ k} (hφ : IsSmoothForm (modelWithCornersSelf ℝ E) 0 φ) (hc : IsCompact (tsupport φ)) (b : Module.Basis (Fin k) ℝ E) (hb : b.orientation = o) : integralTopForm (Manifold.Orientation.model o hk) φ = ∫ (x : E), (φ x) ⇑b ∂b.addHaar

On a finite-dimensional normed space with a constant orientation, the oriented integral of a compactly supported C0 top form is the integral of its coefficient in any positively oriented basis against that basis's Haar measure.

theorem TauCeti.integralTopForm_real_eq_integral {φ : RoughForm (modelWithCornersSelf ℝ ℝ) ℝ ℝ 1} (hφ : IsSmoothForm (modelWithCornersSelf ℝ ℝ) 0 φ) (hc : IsCompact (tsupport φ)) : integralTopForm Manifold.Orientation.real φ = ∫ (t : ℝ), (φ t) fun (x : Fin 1) => 1

Against the standard orientation of ℝ, the oriented integral of a compactly supported continuous 1-form is the Lebesgue integral of its value on the unit vector.

theorem TauCeti.integralTopForm_add {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {k : ℕ} {φ : RoughForm I M ℝ k} (o : Manifold.Orientation I M (Fin k)) {ψ : RoughForm I M ℝ k} (hφ : IsSmoothForm I 0 φ) (hψ : IsSmoothForm I 0 ψ) (hcφ : IsCompact (tsupport φ)) (hcψ : IsCompact (tsupport ψ)) : integralTopForm o (φ + ψ) = integralTopForm o φ + integralTopForm o ψ

The oriented integral is additive for compactly supported C0 top forms.

theorem TauCeti.integralTopForm_add_of_compactSpace {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {k : ℕ} {φ : RoughForm I M ℝ k} [CompactSpace M] (o : Manifold.Orientation I M (Fin k)) {ψ : RoughForm I M ℝ k} (hφ : IsSmoothForm I 0 φ) (hψ : IsSmoothForm I 0 ψ) : integralTopForm o (φ + ψ) = integralTopForm o φ + integralTopForm o ψ

On a compact manifold, the oriented integral is additive for C0 top forms.