Integrability of chart-supported signed top forms #
The signed coordinate coefficient of a form supported compactly within one chart has support in the compact coordinate image of its manifold support. Continuity on the chart target gives actual Haar integrability; extending by zero outside the target causes no boundary assumption.
theorem
TauCeti.RoughForm.support_signedInChartAt_subset
{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 } → ℤˣ)
:
Function.support (φ.signedInChartAt b α σ) ⊆ ↑(extChartAt I α) '' tsupport φ
The signed chart coefficient is supported within the coordinate image of the form support.
theorem
TauCeti.RoughForm.continuousOn_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 } → ℤˣ)
(hσ : Continuous σ)
(hφ : ContinuousOn (φ.inChartAt α) (extChartAt I α).target)
:
ContinuousOn (φ.signedInChartAt b α σ) (extChartAt I α).target
Source-continuous chart signs preserve continuity of the coefficient on the chart target.
theorem
TauCeti.RoughForm.support_signedInChartAt_subset_target
{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 } → ℤˣ)
:
Function.support (φ.signedInChartAt b α σ) ⊆ (extChartAt I α).target
Signed coefficients vanish outside the actual coordinate target.
theorem
TauCeti.RoughForm.integrable_signedInChartAt_iff_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 : ℕ}
[MeasurableSpace E]
[BorelSpace E]
(φ : RoughForm I M ℝ k)
(b : Module.Basis (Fin k) ℝ E)
(α : M)
(σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ)
(hσ : Continuous σ)
(μ : MeasureTheory.Measure E)
:
MeasureTheory.Integrable (φ.signedInChartAt b α σ) μ ↔ MeasureTheory.Integrable (φ.signedInChartAt b α fun (x : { x : M // x ∈ (extChartAt I α).source }) => 1) μ
Actual continuous source signs do not change integrability of a rough coefficient. No continuity of the form or measurable structure on the manifold is assumed.
theorem
TauCeti.RoughForm.integrable_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 : ℕ}
[MeasurableSpace E]
[BorelSpace E]
(φ : RoughForm I M ℝ k)
(b : Module.Basis (Fin k) ℝ E)
(α : M)
(σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ)
(hσ : Continuous σ)
(hφ : ContinuousOn (φ.inChartAt α) (extChartAt I α).target)
(hc : IsCompact (tsupport φ))
(hs : tsupport φ ⊆ (extChartAt I α).source)
(μ : MeasureTheory.Measure E)
[μ.IsAddHaarMeasure]
:
MeasureTheory.Integrable (φ.signedInChartAt b α σ) μ
A compactly supported chart coefficient is genuinely integrable against normalized Haar measure, using only continuity in coordinates and continuity of the source-indexed sign.
theorem
TauCeti.RoughForm.integral_signedInChartAt_eq_of_tsupport_subset
{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]
[FiniteDimensional ℝ 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 } → ℤˣ)
(hsub : tsupport φ ⊆ (extChartAt I α).source ∩ (extChartAt I β).source)
(hσ :
∀ (x : M) (hx : x ∈ (extChartAt I α).source ∩ (extChartAt I β).source),
↑↑(σα ⟨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]
:
Chart-supported top forms have the same actual signed coefficient integral in any two charts containing their support. Only the model is equipped with a measurable structure.
theorem
TauCeti.RoughForm.integrable_signedInChartAt_iff_of_tsupport_subset
{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]
[FiniteDimensional ℝ 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 } → ℤˣ)
(hsub : tsupport φ ⊆ (extChartAt I α).source ∩ (extChartAt I β).source)
(hσ :
∀ (x : M) (hx : x ∈ (extChartAt I α).source ∩ (extChartAt I β).source),
↑↑(σα ⟨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]
:
MeasureTheory.Integrable (φ.signedInChartAt b α σα) μ ↔ MeasureTheory.Integrable (φ.signedInChartAt b β σβ) μ
Genuine integrability of an arbitrary rough chart-supported form transports between charts containing its support. This does not assume continuity of the form.
theorem
TauCeti.IsSmoothForm.integrable_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]
[IsManifold I 1 M]
[MeasurableSpace E]
[BorelSpace E]
{k : ℕ}
{n : WithTop ℕ∞}
{φ : RoughForm I M ℝ k}
(hφ : IsSmoothForm I n φ)
(b : Module.Basis (Fin k) ℝ E)
(α : M)
(σ : { x : M // x ∈ (extChartAt I α).source } → ℤˣ)
(hσ : Continuous σ)
(hc : IsCompact (tsupport φ))
(hs : tsupport φ ⊆ (extChartAt I α).source)
(μ : MeasureTheory.Measure E)
[μ.IsAddHaarMeasure]
:
MeasureTheory.Integrable (φ.signedInChartAt b α σ) μ
A regular form with compact support in one chart has a genuinely integrable signed
coefficient. C⁰ regularity already suffices.