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

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

Exact scale factors for the one-ball good-lambda estimate

This module isolates the elementary extended-real identities which convert the local harmonic and correction tails into a stopping-ball volume times the square of the level. Keeping them separate from the PDE comparison avoids any hidden finite-measure or cancellation assumptions in the one-ball proof.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_harmonic_threshold_rpow_factor {qR M level : ℝ} {A : ENNReal} (hM : 0 < M) (hlevel : 0 < level) (hA : A ≠ ⊤) : ENNReal.ofReal ((M * level / 2) ^ (2 - qR)) * (A * ENNReal.ofReal level) ^ qR = ENNReal.ofReal ((M / 2) ^ (2 - qR)) * A ^ qR * ENNReal.ofReal (level ^ 2)

At the harmonic-tail threshold, the negative threshold power cancels all but two powers of the positive level. Finiteness of A is precisely what allows the ENNReal product to pass through the real exponent.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_child_side_volume {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 ≤ r) : ENNReal.ofReal ((10 * r) ^ d) = 5 ^ d * MeasureTheory.volume (Metric.closedBall x r)

The side-10r cube has exactly 5^d times the volume of the sup-metric stopping ball of radius r.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_parent_side_volume {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 ≤ r) (n : ℕ) : ENNReal.ofReal ((10 * 3 ^ n * r) ^ d) = (5 * 3 ^ n) ^ d * MeasureTheory.volume (Metric.closedBall x r)

The side of the depth-n comparison parent contributes the exact relative factor (5 * 3^n)^d against the stopping ball of radius r.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_harmonic_tail_scale_factor {d : ℕ} {qR M level r : ℝ} {A : ENNReal} (x : Vec d) (hr : 0 ≤ r) (hM : 0 < M) (hlevel : 0 < level) (hA : A ≠ ⊤) : 2 * ENNReal.ofReal ((M * level / 2) ^ (2 - qR)) * (ENNReal.ofReal ((10 * r) ^ d) * (A * ENNReal.ofReal level) ^ qR) = 2 * 5 ^ d * A ^ qR * ENNReal.ofReal ((M / 2) ^ (2 - qR)) * ENNReal.ofReal (level ^ 2) * MeasureTheory.volume (Metric.closedBall x r)

The harmonic local-tail scale factor, already expressed relative to the stopping ball. Here A is the complete harmonic coefficient (for example, 2 * G.constant * d), so no factor is silently discarded.

theorem HCPolySupport.CubeCalderonZygmund.oneBall_correction_tail_scale_factor {d : ℕ} {eps level r : ℝ} (x : Vec d) (hr : 0 ≤ r) (heps : 0 ≤ eps) (hlevel : 0 ≤ level) (n : ℕ) : 6 * ENNReal.ofReal ((10 * 3 ^ n * r) ^ d) * ENNReal.ofReal (eps * level) ^ 2 = 6 * (5 * 3 ^ n) ^ d * ENNReal.ofReal (eps ^ 2) * ENNReal.ofReal (level ^ 2) * MeasureTheory.volume (Metric.closedBall x r)

The correction local-tail scale factor, already expressed relative to the stopping ball.