Lᵖ oscillation on a preconnected space from local oscillation

Let μ be a finite measure on a preconnected space X that charges every nonempty open set, and let V i, i ∈ t, be finitely many open sets covering X. Suppose a function f deviates little from some constant on each V i: ‖f - a i‖_{Lᵖ(V i)} ≤ C i * G. Then f deviates little from a single constant on all of X: ‖f - c‖_{Lᵖ(X)} ≤ K * G, where the constant K depends only on the cover, the measure, p and the local constants C i, and not on f, the local constants a i or the bound G (TauCeti.exists_eLpNorm_sub_const_le_of_isOpen_cover).

This is the chaining step that turns a local Poincaré inequality into a global one on a connected domain or a closed connected manifold. On the overlap of two pieces both local constants approximate f, so they differ by at most a fixed multiple of G, because the overlap is a nonempty open set and so has positive measure. Connectedness joins every piece to a fixed one by a chain of overlapping pieces, and there are finitely many pieces.

Connectedness cannot be dropped: on a disjoint union of two open sets the function equal to 0 on one and 1 on the other is constant on each piece but not close to any single constant.

Main results

• TauCeti.enorm_sub_le_div_of_eLpNorm_restrict_sub_le: two constants approximating f in Lᵖ on overlapping sets are close.
• TauCeti.exists_eLpNorm_sub_const_le_of_isOpen_cover: local Lᵖ closeness to constants on a finite open cover of a preconnected space gives global closeness to one constant.

References

• D. Gilbarg and N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Springer (2001), §7.8.

theorem TauCeti.enorm_sub_le_div_of_eLpNorm_restrict_sub_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] {p : ENNReal} (hp : 1 ≤ p) {U W : Set X} (h0 : μ (U ∩ W) ≠ 0) (htop : μ (U ∩ W) ≠ ⊤) {f : X → F} {a b : F} {A B : ENNReal} (ha : MeasureTheory.eLpNorm (fun (x : X) => f x - a) p (μ.restrict U) ≤ A) (hb : MeasureTheory.eLpNorm (fun (x : X) => f x - b) p (μ.restrict W) ≤ B) : ‖b - a‖ₑ ≤ (A + B) / μ (U ∩ W) ^ (1 / p.toReal)

Constants approximating f on overlapping sets are close. If ‖f - a‖_{Lᵖ(U)} ≤ A and ‖f - b‖_{Lᵖ(W)} ≤ B, and the overlap U ∩ W has positive finite measure, then ‖b - a‖ ≤ (A + B) / μ (U ∩ W) ^ (1 / p).

theorem TauCeti.eLpNorm_restrict_sub_le_add_enorm_mul {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] {p : ENNReal} (hp : 1 ≤ p) {U : Set X} {f : X → F} {a b : F} : MeasureTheory.eLpNorm (fun (x : X) => f x - a) p (μ.restrict U) ≤ MeasureTheory.eLpNorm (fun (x : X) => f x - b) p (μ.restrict U) + ‖b - a‖ₑ * μ U ^ (1 / p.toReal)

Moving the constant. ‖f - a‖_{Lᵖ(U)} ≤ ‖f - b‖_{Lᵖ(U)} + ‖b - a‖ * μ U ^ (1 / p).

theorem TauCeti.exists_eLpNorm_sub_const_le_of_isOpen_cover {X : Type u_1} {F : Type u_2} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] {p : ENNReal} [PreconnectedSpace X] [MeasureTheory.IsFiniteMeasure μ] [μ.IsOpenPosMeasure] (hp : 1 ≤ p) {ι : Type u_3} (t : Finset ι) {V : ι → Set X} (hV : ∀ i ∈ t, IsOpen (V i)) (hcover : ∀ (x : X), ∃ i ∈ t, x ∈ V i) (C : ι → NNReal) : ∃ (K : NNReal), ∀ (f : X → F) (a : ι → F) (G : ENNReal), (∀ i ∈ t, MeasureTheory.eLpNorm (fun (x : X) => f x - a i) p (μ.restrict (V i)) ≤ ↑(C i) * G) → ∃ (c : F), MeasureTheory.eLpNorm (fun (x : X) => f x - c) p μ ≤ ↑K * G

Local Lᵖ closeness to constants on a connected cover gives global closeness. Let μ be a finite measure on a preconnected space, positive on nonempty open sets, and let V i, i ∈ t, be finitely many open sets covering the space. For constants C i there is a constant K such that whenever ‖f - a i‖_{Lᵖ(V i)} ≤ C i * G for every i ∈ t, some constant c satisfies ‖f - c‖_{Lᵖ} ≤ K * G. The constant K does not depend on f, a or G.