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

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

One-ball good-lambda algebra

These are the purely extended-real algebraic steps in the one-stopping-ball comparison. They contain no PDE, stopping, or comparison hypotheses: the analytic proof supplies the two local L² bounds, and this file records the constant bookkeeping that turns their sum into the conventional factor two.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_harmonicGain_scale_le_two {A L e : ENNReal} (he : e ≤ 1) : A * (L + e * L) ≤ 2 * A * L

If the correction energy is at most e times the original local energy and e ≤ 1, then the harmonic-remainder energy costs at most a factor two. The statement is deliberately pure ENNReal algebra, so it can be used after the local normalized-energy and Minkowski estimates without importing any comparison conclusion.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_tail_coefficient_factor (K K' m e Tf Tg : ENNReal) : (K * m + K' * e) * (2 * Tf + 2 * Tg) ≤ (2 * K + 2 * K') * (m + e) * (Tf + Tg)

Factor the two local weighted-tail contributions through a single uniform coefficient. This is the exact overestimate used by the one-ball tail assembly: K * m + K' * e is bounded by (K + K') * (m + e), and the two tail masses are then factored together.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_lintegral_ofReal_norm_rpow_le_volume_mul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (p : FiniteLpExponent) (V : Vec d → E) {B : ENNReal} (hV : MeasureTheory.eLpNorm V p.exponent (axisCubeNormalizedMeasure z L) ≤ B) : ∫⁻ (y : Vec d) in axisCube z L, ENNReal.ofReal (‖V y‖ ^ p.exponent.toReal) ≤ ENNReal.ofReal (L ^ d) * B ^ p.exponent.toReal

The powered normalized L^p bound on a positive axis cube yields the raw local integral bound on that open cube. The factor is exactly L^d, obtained by cancelling the positive normalized-volume density. This is the open-cube form used when the final comparison tail is restricted to the triadic child.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_lintegral_ofReal_norm_sq_le_volume_mul {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (V : Vec d → E) {B : ENNReal} (hV : MeasureTheory.eLpNorm V 2 (axisCubeNormalizedMeasure z L) ≤ B) : ∫⁻ (y : Vec d) in axisCube z L, ENNReal.ofReal (‖V y‖ ^ 2) ≤ ENNReal.ofReal (L ^ d) * B ^ 2

The p=2 specialization of axisCube_lintegral_ofReal_norm_rpow_le_volume_mul.

theorem HCPolySupport.CubeCalderonZygmund.closedBall_lintegral_ofReal_norm_rpow_le_axisCube_volume_mul {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (p : FiniteLpExponent) (V : Vec d → E) {B : ENNReal} (hV : MeasureTheory.eLpNorm V p.exponent (axisCubeNormalizedMeasure z L) ≤ B) : ∫⁻ (y : Vec d) in Metric.closedBall (axisCubeCenter z L) (L / 2), ENNReal.ofReal (‖V y‖ ^ p.exponent.toReal) ≤ ENNReal.ofReal (L ^ d) * B ^ p.exponent.toReal

The powered normalized L^p bound on a positive axis cube yields the raw local integral bound over its a.e.-equal closed ball. The factor is exactly the cube volume L^d: it is obtained by cancelling the positive normalized-volume density, not by a comparison estimate.

theorem HCPolySupport.CubeCalderonZygmund.closedBall_lintegral_ofReal_norm_sq_le_axisCube_volume_mul {d : ℕ} [NeZero d] {E : Type u_1} [NormedAddCommGroup E] (z : Vec d) {L : ℝ} (hL : 0 < L) (V : Vec d → E) {B : ENNReal} (hV : MeasureTheory.eLpNorm V 2 (axisCubeNormalizedMeasure z L) ≤ B) : ∫⁻ (y : Vec d) in Metric.closedBall (axisCubeCenter z L) (L / 2), ENNReal.ofReal (‖V y‖ ^ 2) ≤ ENNReal.ofReal (L ^ d) * B ^ 2

The p=2 specialization of closedBall_lintegral_ofReal_norm_rpow_le_axisCube_volume_mul.