Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaVitaliSum

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Measure summation after Vitali selection

This file isolates the purely measure-theoretic summation step used after a Vitali selection of stopping balls. It deliberately knows nothing about the origin of the high-level set or the control measure.

theorem HCPolySupport.CubeCalderonZygmund.measure_le_mul_measure_of_vitali_closedBall_cover {d : ℕ} {ι : Type u_1} (ν κ : MeasureTheory.Measure (Vec d)) (target ambient : Set (Vec d)) (u : Set ι) (centre : ι → Vec d) (radius : ι → ℝ) (τ : ℝ) (K : ENNReal) (hpositive : ∀ i ∈ u, 0 < radius i) (hdisjoint : u.PairwiseDisjoint fun (i : ι) => Metric.closedBall (centre i) (radius i)) (hcover : target ⊆ ⋃ i ∈ u, Metric.closedBall (centre i) (τ * radius i)) (hlocal : ∀ i ∈ u, ν (target ∩ Metric.closedBall (centre i) (τ * radius i)) ≤ K * κ (Metric.closedBall (centre i) (radius i))) (hambient : ⋃ i ∈ u, Metric.closedBall (centre i) (radius i) ⊆ ambient) : ν target ≤ K * κ ambient

Sum local estimates over a Vitali-selected family. The selected original balls are pairwise disjoint and have positive radius, hence are countable in the separable space Vec d; their enlarged balls only provide the cover and need not be disjoint.