StepSevenVolume

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

t.regularity Step 7c: the hvol producer at the general triadic ratio

The gap this module closes

The composition gaps open with hvol: stepSevenGradientWithShom takes the volume cost

  gradLoc  ≤  3^{(d/2)(n'-n)} · gradCore

as a hypothesis, and no producer exists at that literal shape. The obstruction is a side condition: the manuscript asserts the inclusion

Since (z + □_n) ∩ □_m ⊆ U_{n'-2}, passing to the smaller set costs a volume factor 3^{(d/2)(n'-n)}

and the inclusion of the two truncated windows at scales n+1 and n'-2 needs n + 1 ≤ n' - 2, which appears in NO binder of the printed display and in no binder of stepSevenGradientWithShom.

  n + 3 ≤ n'      ↔      n + 1 ≤ n' - 2 ,

so the unstated hypothesis is free at the consumption site. The arithmetic is tight: the printed selection range [n+3, m-3] is what makes the Caccioppoli core at n'-2 contain the window at n+1; had the manuscript written [n+2, m-3] the display would be false as printed.

What is produced

• truncatedWindow_succ_subset_caccCore — the tex's own inclusion (z+□_{n+1}) ∩ □_m ⊆ (z+□_{n'-2}) ∩ □_m, with the side condition discharged.
• three_rpow_le_volume_toReal_truncatedWindow / volume_toReal_truncatedWindow_le_rpow — the two volume bounds (b) needs, the lower one from the inscribed well-placed cube and the upper one from truncatedWindow_subset_translate. The lower bound is where the shift n+1 ↦ n happens: the window at scale k contains a full cube of scale k-1, so the window at n+1 has volume at least 3^{dn} — the printed 3^{dn} denominator, not an approximation of it.
• stepSevenVolumeRatio_le — the general-ratio producer on the two masses.

The masses IS ≤ IT remain the caller's: ν^{1/2}‖∇u‖_{L²(S)} is read as the symmetric coefficient energy, and its monotonicity in the domain is an integral monotonicity, not an estimate. No new estimate is derived here; every step is a proved atom or Real.rpow arithmetic.

References

• ABK26, t.regularity Step 7c; Step 7a.

1. The side condition, and the inclusion it unlocks

theorem Algsuperdiff.Section4.Provider.Regularity.truncatedWindow_succ_subset_caccCore {d : ℕ} (z : HCPolySupport.Vec d) (m : ℤ) {n n' : ℤ} (hgap : n + 1 ≤ n' - 2) : ExcessDecay.truncatedWindow z m (n + 1) ⊆ ExcessDecay.truncatedWindow z m (n' - 2)

The tex's own inclusion (z+□_{n+1}) ∩ □_m ⊆ (z+□_{n'-2}) ∩ □_m, at the derived side condition.

2. The two volume bounds

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_three_dim_mul (d : ℕ) (j : ℤ) : Real.rpow 3 (↑d * ↑j) = (3 ^ j) ^ d

3^{d j} = (3^j)^d in the rpow spelling the volume comparison uses.

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_le_volume_toReal_truncatedWindow (d : ℕ) {m k : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k - 1 ≤ m) : Real.rpow 3 (↑d * ↑(k - 1)) ≤ (MeasureTheory.volume (ExcessDecay.truncatedWindow z m k)).toReal

The window's volume lower bound (lower half). For z ∈ □_m and k - 1 ≤ m, the truncated window (z+□_k) ∩ □_m contains a full translate of □_{k-1} — the inscribed well-placed cube — so its volume is at least 3^{d(k-1)}. At k = n+1 this is the printed 3^{dn}.

theorem Algsuperdiff.Section4.Provider.Regularity.volume_toReal_truncatedWindow_le_rpow (d : ℕ) (z : HCPolySupport.Vec d) (m j : ℤ) : (MeasureTheory.volume (ExcessDecay.truncatedWindow z m j)).toReal ≤ Real.rpow 3 (↑d * ↑j)

The window's volume upper bound ((b), upper half). The truncated window sits inside the full translate z + □_j, whose volume is 3^{dj}.

theorem Algsuperdiff.Section4.Provider.Regularity.volume_toReal_caccCore_le_rpow (d : ℕ) (z : HCPolySupport.Vec d) (m n' : ℤ) : (MeasureTheory.volume (ExcessDecay.truncatedWindow z m (n' - 2))).toReal ≤ Real.rpow 3 (↑d * ↑n')

The volume upper bound, moved from the core scale n'-2 up to the printed n'.

3. The general-ratio producer

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenVolumeRatio_le (d : ℕ) {m n n' : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n ≤ m) {IS IT : ℝ} (hmono : IS ≤ IT) : √(IS / (MeasureTheory.volume (ExcessDecay.truncatedWindow z m (n + 1))).toReal) ≤ Real.rpow 3 (↑d / 2 * (↑n' - ↑n)) * √(IT / (MeasureTheory.volume (ExcessDecay.truncatedWindow z m (n' - 2))).toReal)

hvol at the general triadic ratio ((b)).

For z ∈ □_m, n ≤ m, and any two masses with IS ≤ IT carried by the window (z+□_{n+1}) ∩ □_m and the Caccioppoli core (z+□_{n'-2}) ∩ □_m, the volume-normalized square roots compare at the printed factor:

  √(IS/|S|)  ≤  3^{(d/2)(n'-n)} · √(IT/|T|) .

This is normalizedSqrt_le_volumeRatio_mul composed with sqrt_volumeRatio_le_rpow_three at the two window volume bounds above — the two halves, now with both of them supplied rather than assumed. The mass monotonicity IS ≤ IT is the caller's integral comparison and is the only input.