Linearity of actual signed chart integrals

Signed chart coefficients commute with finite sums and constant scalar multiplication. The actual orientation-lift chart integral is additive when its coefficients are integrable, and homogeneous even for the total integral of an arbitrary rough form. All integrability hypotheses refer to the actual signed coefficients in an explicitly supplied model basis.

@[simp]

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

The zero form has zero signed coefficient, including outside the chart target.

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

Constant scalar multiplication commutes with the actual signed chart coefficient.

theorem TauCeti.RoughForm.signedInChartAt_sum {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 : ℕ} {ι : Type u_4} (φ : ι → RoughForm I M ℝ k) (s : Finset ι) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (y : E) : (∑ i ∈ s, φ i).signedInChartAt b α σ y = ∑ i ∈ s, (φ i).signedInChartAt b α σ y

The signed coefficient of a finite sum of actual forms is the finite sum of coefficients.

theorem TauCeti.RoughForm.integrable_signedInChartAt_sum {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 : ℕ} [MeasurableSpace E] {ι : Type u_4} (φ : ι → RoughForm I M ℝ k) (s : Finset ι) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (μ : MeasureTheory.Measure E) (h : ∀ i ∈ s, MeasureTheory.Integrable ((φ i).signedInChartAt b α σ) μ) : MeasureTheory.Integrable ((∑ i ∈ s, φ i).signedInChartAt b α σ) μ

Integrability of the actual signed coefficients is preserved by finite sums, for any measure.

@[simp]

theorem TauCeti.Manifold.OrientationLift.chartIntegral_zero {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)) (α : M) : l.chartIntegral 0 α = 0

The actual orientation-lift chart integral of zero is zero.

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

The actual chart integral is additive under integrability of its two signed coefficients.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_smul {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)) (c : ℝ) (φ : RoughForm I M ℝ k) (α : M) : l.chartIntegral (c • φ) α = c * l.chartIntegral φ α

Constant scalar multiplication commutes with the actual total chart integral, with no integrability or regularity hypothesis.

theorem TauCeti.Manifold.OrientationLift.chartIntegral_sum {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 : ℕ} {ι : Type u_4} (l : OrientationLift I M (Fin k)) (b : Module.Basis (Fin k) ℝ E) (φ : ι → RoughForm I M ℝ k) (s : Finset ι) (α : M) (h : ∀ i ∈ s, MeasureTheory.Integrable ((φ i).signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => l.signAt α ↑x) b.addHaar) : l.chartIntegral (∑ i ∈ s, φ i) α = ∑ i ∈ s, l.chartIntegral (φ i) α

The actual lift chart integral of a finite sum is the sum of chart integrals when the actual signed coefficients in the supplied basis are integrable.