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

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

The real-variable core of the cube Calderón--Zygmund argument

This file records the two source-independent steps in the global Caffarelli--Peral argument from CZestimates.tex:

• a bounded family of stopping balls has a disjoint Vitali subfamily whose fixed enlargements cover the original family; and
• once layer-cake has turned a one-level good-λ estimate into a scalar inequality, the term carrying the unknown quantity can be reabsorbed.

The construction of the stopping balls, the cube doubling estimate, and the conversion of local comparison estimates to the one-level estimate belong to the later cube-specific packet. In particular, neither a harmonic approximant nor a final Calderón--Zygmund estimate is made a hypothesis here.

theorem HCPolySupport.CubeCalderonZygmund.exists_disjoint_closedBall_subfamily_covering_union {α : Type u_1} {ι : Type u_2} [PseudoMetricSpace α] (t : Set ι) (centre : ι → α) (radius : ι → ℝ) (R : ℝ) (hradius : ∀ a ∈ t, radius a ≤ R) (τ : ℝ) (hτ : 3 < τ) : ∃ u ⊆ t, (u.PairwiseDisjoint fun (a : ι) => Metric.closedBall (centre a) (radius a)) ∧ ⋃ a ∈ t, Metric.closedBall (centre a) (radius a) ⊆ ⋃ b ∈ u, Metric.closedBall (centre b) (τ * radius b)

A bounded family of closed balls admits a pairwise disjoint subfamily whose τ-enlargements cover the union of the original family. This is the form of Vitali selection used after the stopping-radius construction in the global good-λ argument.

theorem HCPolySupport.CubeCalderonZygmund.goodLambda_reabsorb {θ X C Y : ℝ} (hθ : θ < 1) (h : X ≤ θ * X + C * Y) : X ≤ C / (1 - θ) * Y

The scalar reabsorption step at the end of a good-λ proof. Typically X is the weighted layer-cake integral of the solution, Y that of the data, and θ < 1 is arranged by choosing the good-λ parameters internally.