Gluing locally constant distributions

On a connected nonempty open set, a distribution which is locally integration against a constant is globally integration against one unique constant. No finite-mass or order-zero assumption is made. The constants are identified by integral-one tests on overlaps, and finite smooth partitions of unity identify the resulting global distribution.

The result applies to Banach-valued distributions and any locally finite measure positive on nonempty open sets. With Lebesgue measure it supplies the local-to-global step in distributional constancy proofs: establishing the local constant formulas is a separate analytic task.

References

• Hörmander, The Analysis of Linear Partial Differential Operators I, §2.2 (Localization), Theorem 2.2.4: piecing together compatible local distributions.

theorem Distribution.ofFun_const_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hne : (↑Ω).Nonempty) : Function.Injective fun (c : F) => ofFun Ω (fun (x : E) => c) μ n

On a nonempty open domain, the constant inducing a distribution is uniquely determined.

theorem Distribution.existsUnique_eq_ofFun_const_of_locally {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (T : Distribution Ω F n) (hΩ : IsConnected ↑Ω) (h : ∀ x ∈ Ω, ∃ (U : Set E), IsOpen U ∧ x ∈ U ∧ ∃ (c : F), ∀ (φ : TestFunction Ω ℝ n), tsupport ⇑φ ⊆ U → T φ = (∫ (y : E), φ y ∂μ) • c) : ∃! c : F, T = ofFun Ω (fun (x : E) => c) μ n

Local constant evaluation formulas for a distribution glue to one unique global constant on a connected nonempty domain. Neighborhoods need not form a finite cover, and their local constants are not assumed compatible.