Basis independence of signed chart integrals #
The source-indexed chart sign and the relative basis sign serve different purposes. The former corrects a chart's orientation; the latter lets integration use an arbitrary basis, including negative model orientations in dimension zero. The actual signed chart integral is independent of that arbitrary basis, with the corresponding normalized Haar measure.
theorem
TauCeti.RoughForm.integral_signedInChartAt_basis_eq
{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]
{k : ℕ}
(φ : RoughForm I M ℝ k)
(o : Orientation ℝ E (Fin k))
(b b' : Module.Basis (Fin k) ℝ E)
(α : M)
(σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ)
:
The actual signed chart integral does not depend on the chosen basis, even if neither basis is positively oriented for the model orientation.
theorem
TauCeti.RoughForm.integrable_signedInChartAt_basis_iff
{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]
{k : ℕ}
(φ : RoughForm I M ℝ k)
(b b' : Module.Basis (Fin k) ℝ E)
(α : M)
(σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ)
:
MeasureTheory.Integrable (φ.signedInChartAt b' α σ) b'.addHaar ↔ MeasureTheory.Integrable (φ.signedInChartAt b α σ) b.addHaar
Genuine signed coefficient integrability is independent of the model basis and its normalized Haar measure, without a regularity assumption on the form or chart sign.