Operations on signed chart coefficients

Signed coefficients respect addition and scalar localization of actual rough differential forms. Reversing the chart signs reverses the coefficient, whereas simultaneously reversing the model orientation and chart signs preserves the relative-basis coefficient integral.

theorem TauCeti.RoughForm.signedInChartAt_add {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 = φ.signedInChartAt b α σ y + ψ.signedInChartAt b α σ y

Signed coefficients commute with addition of actual forms.

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

Scalar localization of a form commutes with the source-indexed signed coefficient.

theorem TauCeti.RoughForm.signedInChartAt_indicator {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 : ℕ} (s : Set M) (φ : RoughForm I M ℝ k) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) (y : E) : signedInChartAt (fun (x : M) => s.indicator (fun (x : M) => 1) x • φ x) b α σ y = ((extChartAt I α).target ∩ ↑(extChartAt I α).symm ⁻¹' s).indicator (φ.signedInChartAt b α σ) y

Restriction of a form by an indicator restricts its signed coefficient to the corresponding coordinate piece. This uses only the form values, so it also applies to discontinuous pieces.

theorem TauCeti.RoughForm.signedInChartAt_neg_sign {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 α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => -σ x) y = -φ.signedInChartAt b α σ y

Reversing every chart sign reverses the actual coefficient.

theorem TauCeti.RoughForm.integral_signedInChartAt_diagonal_flip {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] [BorelSpace E] (φ : RoughForm I M ℝ k) (o : Orientation ℝ E (Fin k)) (b : Module.Basis (Fin k) ℝ E) (α : M) (σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ) : ↑↑((-o).signBasis b) * ∫ (y : E), φ.signedInChartAt b α (fun (x : { x : M // x ∈ (extChartAt I α).source }) => -σ x) y ∂b.addHaar = ↑↑(o.signBasis b) * ∫ (y : E), φ.signedInChartAt b α σ y ∂b.addHaar

The actual relative-basis coefficient integral descends through simultaneous reversal of model orientation and chart signs, including in dimension zero.