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

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

theorem HCPolySupport.CubeCalderonZygmund.goodLambdaCombinedEnergy_eq_tail_transfer {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) {ε level r : ℝ} (hε : 0 < ε) (hr : 0 < r) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (hfi : MeasureTheory.Integrable (fun (y : Vec d) => ‖f y‖ ^ 2) MeasureTheory.volume) (hgi : MeasureTheory.Integrable (fun (y : Vec d) => ‖g y‖ ^ 2) MeasureTheory.volume) (x : Vec d) (hstop : goodLambdaCombinedEnergy f g ε x r = level) : ENNReal.ofReal (level ^ 2) * MeasureTheory.volume (Metric.closedBall x r) ≤ 2 * (sqWeightedMeasure f MeasureTheory.volume) ({y : Vec d | level / 2 < ‖f y‖} ∩ Metric.closedBall x r) + 2 * ENNReal.ofReal (ε⁻¹ ^ 2) * (sqWeightedMeasure g MeasureTheory.volume) ({y : Vec d | ε * level / 2 < ‖g y‖} ∩ Metric.closedBall x r)

At an exact combined stopping radius, the normalized energy is forced into the two corresponding weighted superlevel tails.

theorem HCPolySupport.CubeCalderonZygmund.closedBallL2Energy_sqrt_bounds_of_goodLambdaCombinedEnergy_le {d : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedAddCommGroup G] (f : Vec d → F) (g : Vec d → G) {ε level r : ℝ} (hε : 0 < ε) (hr : 0 < r) (x : Vec d) (h : goodLambdaCombinedEnergy f g ε x r ≤ level) : √(closedBallL2Energy f x r) ≤ level ∧ √(closedBallL2Energy g x r) ≤ ε * level

A combined good-λ energy bound controls each component at the same radius.