Signed top-form integrals in preferred charts

A chart sign is indexed only by points of that chart's source. Signed coefficients are extended by zero outside the coordinate target. On an actual chart overlap, the signed coefficient integrals and their integrability agree by the Jacobian theorem and the top-form chart cocycle. Only the model carries a measurable structure; no measurable structure on the manifold is used.

noncomputable def TauCeti.RoughForm.signedInChartAt {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] {k : ℕ} (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (y : E) : ℝ

A signed top-form coefficient in a preferred chart, extended by zero outside its target. The sign data have no values outside the source of the chart.

theorem TauCeti.RoughForm.signedInChartAt_apply {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] {k : ℕ} (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (y : E) : φ.signedInChartAt b α σ y = if hy : y ∈ (extChartAt I α).target then ↑↑(σ ⟨↑(extChartAt I α).symm y, ⋯⟩) * (φ.inChartAt α y) ⇑b else 0

Evaluation of the signed coefficient, with its zero extension outside the target.

theorem TauCeti.RoughForm.signedInChartAt_one {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] {j : ℕ} (ψ : RoughForm I M ℝ j) (b : Module.Basis (Fin j) ℝ E) (α : M) (y : E) : ψ.signedInChartAt b α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => 1) y = ((extChartAt I α).target.indicator (ψ.inChartAt α) y) ⇑b

A chart coefficient with constant positive sign is the evaluation of the coordinate form extended by zero outside the target.

theorem TauCeti.RoughForm.signedInChartAt_apply_of_mem_source {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] {k : ℕ} (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) {x : M} (hx : x ∈ (extChartAt I α).source) : φ.signedInChartAt b α σ (↑(extChartAt I α) x) = ↑↑(σ ⟨x, hx⟩) * (φ.inChartAt α (↑(extChartAt I α) x)) ⇑b

Within the chart source, the coefficient uses precisely the sign at the original point.

theorem TauCeti.RoughForm.eqOn_signedInChartAt_image {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] {k : ℕ} {φ ψ : RoughForm I M ℝ k} {s : Set M} (h : ∀ x ∈ s, φ x = ψ x) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (hs : s ⊆ (extChartAt I α).source) : Set.EqOn (φ.signedInChartAt b α σ) (ψ.signedInChartAt b α σ) (↑(extChartAt I α) '' s)

Signed coefficients only read the values of the form: two forms that agree on a subset of a chart source have the same signed coefficients on its coordinate image.

theorem TauCeti.RoughForm.signedInChartAt_changeChart {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] {k : ℕ} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [IsManifold I 1 M] (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α β : M) (σα : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (σβ : { x : M // x ∈ (extChartAt I β).source } → ℤˣ) {s : Set M} (hsub : s ⊆ (extChartAt I α).source ∩ (extChartAt I β).source) (hs : MeasurableSet (↑(extChartAt I α) '' s)) (hσ : ∀ (x : M) (hx : x ∈ s), ↑↑(σα ⟨x, ⋯⟩) * LinearMap.det ↑(fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) (↑(extChartAt I α) x)) = |LinearMap.det ↑(fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) (↑(extChartAt I α) x))| * ↑↑(σβ ⟨x, ⋯⟩)) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] : ∫ (y : E) in ↑(extChartAt I α) '' s, φ.signedInChartAt b α σα y ∂μ = ∫ (y : E) in ↑(extChartAt I β) '' s, φ.signedInChartAt b β σβ y ∂μ ∧ (MeasureTheory.IntegrableOn (φ.signedInChartAt b α σα) (↑(extChartAt I α) '' s) μ ↔ MeasureTheory.IntegrableOn (φ.signedInChartAt b β σβ) (↑(extChartAt I β) '' s) μ)

Signed preferred-chart integrals and integrability agree on an actual overlap. The compatibility condition is the signed transition Jacobian, not an assumed integral identity. The derivatives are taken within range I, so the result includes boundary and corner models.

theorem TauCeti.RoughForm.integrableOn_signedInChartAt_one_changeChart {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] {k : ℕ} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [IsManifold I 1 M] (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α β : M) {s : Set M} (hsub : s ⊆ (extChartAt I α).source ∩ (extChartAt I β).source) (hs : MeasurableSet (↑(extChartAt I α) '' s)) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] : MeasureTheory.IntegrableOn (φ.signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => 1) (↑(extChartAt I α) '' s) μ ↔ MeasureTheory.IntegrableOn (φ.signedInChartAt b β fun (x : { x : M // x ∈ (extChartAt I β).source }) => 1) (↑(extChartAt I β) '' s) μ

Actual integrability of unsigned top-form coefficients is invariant under a chart change. The absolute Jacobian theorem and a measurable determinant sign preserve both strong measurability and integrability, even for arbitrary rough forms on nonorientable manifolds.

theorem TauCeti.RoughForm.signedInChartAt_eq_const_mul_unsigned {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] {k : ℕ} (ψ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : ↑(extChartAt I α).source → ℤˣ) (c : ℤˣ) (hσ : ∀ (x : ↑(extChartAt I α).source), ↑x ∈ tsupport ψ → σ x = c) : ψ.signedInChartAt b α σ = fun (y : E) => ↑↑c * ψ.signedInChartAt b α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => 1) y

A source sign constant on the form's support factors out of the actual chart coefficient.