Chart integrals against actual orientation lifts

An orientation lift determines an actual signed chart functional, expressed using an arbitrary model basis and its normalized Haar measure. The relative basis sign makes the functional independent of the basis, including in dimension zero. Actual lift compatibility then gives agreement between charts containing the compact support of the form.

noncomputable def TauCeti.Manifold.OrientationLift.chartIntegral {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] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (α : M) : ℝ

The chart integral against a lift, with actual source-indexed chart signs and normalized Haar measure. Its basis choice is removed by chartIntegral_eq_integral.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_eq_integral {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] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) : l.chartIntegral φ α = ↑↑(l.modelOrientation.signBasis b) * ∫ (y : E), φ.signedInChartAt b α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => l.signAt α ↑x) y ∂b.addHaar

Any model basis gives the actual chart integral, with its relative orientation sign.

theorem TauCeti.Manifold.OrientationLift.integrable_signedInChartAt {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 : OrientationLift I M (Fin k)) {φ : RoughForm I M ℝ k} {n : WithTop ℕ∞} (hφ : IsSmoothForm I n φ) (b : Module.Basis (Fin k) ℝ E) (α : M) (hc : IsCompact (tsupport φ)) (hs : tsupport φ ⊆ (extChartAt I α).source) : MeasureTheory.Integrable (φ.signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => l.signAt α ↑x) b.addHaar

A continuous compact chart-supported form has an integrable actual coefficient for the lift.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_eq_of_tsupport_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 : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (α β : M) (hα : tsupport φ ⊆ (extChartAt I α).source) (hβ : tsupport φ ⊆ (extChartAt I β).source) : l.chartIntegral φ α = l.chartIntegral φ β

The actual lift chart integrals agree when both charts contain the form support. The signed Jacobian relation is derived from the lift, rather than supplied as an extra premise.

theorem TauCeti.Manifold.OrientationLift.integrable_signedInChartAt_iff_of_tsupport_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 : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α β : M) (hα : tsupport φ ⊆ (extChartAt I α).source) (hβ : tsupport φ ⊆ (extChartAt I β).source) : MeasureTheory.Integrable (φ.signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => l.signAt α ↑x) b.addHaar ↔ MeasureTheory.Integrable (φ.signedInChartAt b β fun (x : { x : M // x ∈ (extChartAt I β).source }) => l.signAt β ↑x) b.addHaar

Genuine coefficient integrability of arbitrary rough forms is preserved between charts containing the support, using the actual lift compatibility.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_neg {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] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (α : M) : (-l).chartIntegral φ α = -l.chartIntegral φ α

Reversing the actual manifold orientation reverses the lift's chart integral.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_flip {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] {k : ℕ} (l : OrientationLift I M (Fin k)) (φ : RoughForm I M ℝ k) (α : M) : l.flip.chartIntegral φ α = l.chartIntegral φ α

Simultaneous reversal of the model orientation and source signs preserves the actual chart integral, so the functional depends only on the manifold orientation.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_eq_const_mul_unsigned {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] {k : ℕ} (l : OrientationLift I M (Fin k)) (ψ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (c : ℤˣ) (hσ : ∀ x ∈ tsupport ψ, l.signAt α x = c) : l.chartIntegral ψ α = ↑↑(l.modelOrientation.signBasis b) * ↑↑c * ∫ (y : E), ψ.signedInChartAt b α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => 1) y ∂b.addHaar

A lift sign constant on the support factors out of its genuine normalized chart integral.