Integration in a chart containing the interior

A convex model's boundary has Haar measure zero. A chart containing every intrinsic interior point therefore computes the whole top-form integral, even if it omits endpoints or corner faces.

theorem TauCeti.integralTopForm_eq_chartIntegral_of_interior_subset {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 : ℕ} (l : Manifold.OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (hi : IntegrableTopForm φ) (α : M) (hs : ModelWithCorners.interior M ⊆ (extChartAt I α).source) : integralTopForm (Manifold.Orientation.mk l) φ = l.chartIntegral φ α

A preferred chart containing all intrinsic interior points computes the actual integral. No regularity of the integrable form or measurable structure on the manifold is required.