Basis independence of alternating-form integrals

A basis determines a real top-degree coefficient and normalized Haar measure. Their integral changes by the orientation sign of the basis change. Relative orientation signs make it independent of an arbitrary basis, including negative orientations in dimension zero.

theorem Module.Basis.integral_apply_basis_change {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [DecidableEq ι] (b b' : Basis ι ℝ E) (ω : E → E [⋀^ι]→L[ℝ] ℝ) : ∫ (x : E), (ω x) ⇑b' ∂b'.addHaar = b.det ⇑b' / |b.det ⇑b'| * ∫ (x : E), (ω x) ⇑b ∂b.addHaar

Arbitrary basis changes transform the actual top-form coefficient integral by their orientation sign. Positive Haar scaling and signed form coefficients are both retained.

theorem Module.Basis.integral_apply_eq_of_orientation_eq {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [DecidableEq ι] (b b' : Basis ι ℝ E) (ho : b.orientation = b'.orientation) (ω : E → E [⋀^ι]→L[ℝ] ℝ) : ∫ (x : E), (ω x) ⇑b ∂b.addHaar = ∫ (x : E), (ω x) ⇑b' ∂b'.addHaar

The actual integral of a top-form coefficient is invariant under an orientation-compatible basis change. The compensating Haar normalization is essential.

theorem Module.Basis.integral_signed_apply_eq {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] [DecidableEq ι] (o : Orientation ℝ E ι) (b b' : Basis ι ℝ E) (ω : E → E [⋀^ι]→L[ℝ] ℝ) : ↑↑(o.signBasis b) * ∫ (x : E), (ω x) ⇑b ∂b.addHaar = ↑↑(o.signBasis b') * ∫ (x : E), (ω x) ⇑b' ∂b'.addHaar

The actual signed coefficient integral is independent of an arbitrary basis. The model orientation is fixed; the relative basis sign handles both determinant signs and dimension zero.

theorem Module.Basis.integrable_apply_basis_iff {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [Fintype ι] (b b' : Basis ι ℝ E) (ω : E → E [⋀^ι]→L[ℝ] ℝ) : MeasureTheory.Integrable (fun (x : E) => (ω x) ⇑b') b'.addHaar ↔ MeasureTheory.Integrable (fun (x : E) => (ω x) ⇑b) b.addHaar

Top-form coefficient integrability is independent of the basis and its Haar normalization.