Signed change of variables for alternating-form coefficients #
The Jacobian theorem transports top-degree coefficients and their integrability under injective differentiable coordinate changes. Source and target signs account for both orientations through their compatibility with the signed determinant.
theorem
MeasureTheory.integral_image_signed_apply_basis_eq_integral_pullback
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{μ : Measure E}
[μ.IsAddHaarMeasure]
{T : E → E}
{T' : E → E →L[ℝ] E}
{s : Set E}
(b : Module.Basis ι ℝ E)
(hs : MeasurableSet s)
(hT : ∀ x ∈ s, HasFDerivWithinAt T (T' x) s x)
(hinj : Set.InjOn T s)
(σsource σtarget : E → ℤˣ)
(hσ : ∀ x ∈ s, ↑↑(σsource x) * LinearMap.det ↑(T' x) = |LinearMap.det ↑(T' x)| * ↑↑(σtarget (T x)))
(ω : E → E [⋀^ι]→L[ℝ] ℝ)
:
The actual coefficient integral is compatible with chart signs, allowing reversing coordinate changes. The signs need only agree with the signed Jacobian on the overlap.
theorem
MeasureTheory.integrableOn_image_signed_apply_basis_iff_pullback
{E : Type u_1}
{ι : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{μ : Measure E}
[μ.IsAddHaarMeasure]
{T : E → E}
{T' : E → E →L[ℝ] E}
{s : Set E}
(b : Module.Basis ι ℝ E)
(hs : MeasurableSet s)
(hT : ∀ x ∈ s, HasFDerivWithinAt T (T' x) s x)
(hinj : Set.InjOn T s)
(σsource σtarget : E → ℤˣ)
(hσ : ∀ x ∈ s, ↑↑(σsource x) * LinearMap.det ↑(T' x) = |LinearMap.det ↑(T' x)| * ↑↑(σtarget (T x)))
(ω : E → E [⋀^ι]→L[ℝ] ℝ)
:
IntegrableOn (fun (y : E) => ↑↑(σtarget y) * (ω y) ⇑b) (T '' s) μ ↔ IntegrableOn (fun (x : E) => ↑↑(σsource x) * ((ω (T x)).compContinuousLinearMap (T' x)) ⇑b) s μ
Genuine integrability of signed top-form coefficients transports with the chart signs, including orientation-reversing changes of coordinates.