Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaVitaliAssembly #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Global measure bound from a stopping-ball family #
This is the one-level assembly bridge for a good-λ argument. A stopping
radius is supplied at every point of the target set; Vitali selection and the
measure summation are internal to the theorem.
theorem
HCPolySupport.CubeCalderonZygmund.measure_le_mul_measure_of_vitali_stopping_family
{d : ℕ}
(ν κ : MeasureTheory.Measure (Vec d))
(target ambient : Set (Vec d))
(radius : Vec d → ℝ)
(R τ : ℝ)
(K : ENNReal)
(hradius : ∀ x ∈ target, radius x ≤ R)
(hpositive : ∀ x ∈ target, 0 < radius x)
(hτ : 3 < τ)
(hlocal : ∀ x ∈ target, ν (target ∩ Metric.closedBall x (τ * radius x)) ≤ K * κ (Metric.closedBall x (radius x)))
(hambient : ⋃ x ∈ target, Metric.closedBall x (radius x) ⊆ ambient)
:
A uniformly bounded positive stopping-ball family with a local estimate gives the corresponding global measure estimate. No countability or disjointness data are supplied by the caller: they are produced internally by Vitali selection.