StepSevenCaccVolume

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

t.regularity Step 7c, the volume factor

The target

ABK26 t.regularity Step 7c, the sentence

Since (z + □_n) ∩ □_m ⊆ U_{n'-2}, passing to the smaller set costs a volume factor 3^{(d/2)(n'-n)} ≤ 3^{(d/2)(|𝓑|+6)}. By e.bad.scale.proportion.bound, this is at most C 3^{(1/4)(1-α)(m-n)}.

Two independent halves, both proved here unconditionally.

Half one — what "costs a volume factor" means

The manuscript asserts the factor by inspection. The decomposition it hides: the factor is the square root of the ratio of the two volumes, and the ratio is bounded by combining

• the inclusion (z + □_{n+1}) ∩ □_m ⊆ U_{n'-2} (the step's own stated hypothesis, coming from the selection and the window geometry), and
• the volume lower bound 3^{dn} ≤ |(z + □_{n+1}) ∩ □_m| against the upper bound |U_{n'-2}| ≤ |□_{n'}| = 3^{dn'}.

normalizedSqrt_le_volumeRatio_mul is that decomposition at the level of the volume-normalized L² masses: for S ⊆ T with 0 < |S|,

  ( |S|⁻¹ ∫_S f )^{1/2}  ≤  ( |T| / |S| )^{1/2} · ( |T|⁻¹ ∫_T f )^{1/2} ,

which is an identity plus monotonicity of the integral, no analysis. It is stated on the scalars IS ≤ IT and volS, volT so that it composes with any rendering of the two masses (: the ABK26 field is 𝐚_L = ν I + 𝐤 with 𝐤 antisymmetric, so ν^{1/2}‖∇u‖_{L²} IS the symmetric coefficient energy — the left-hand side of e.gradient.with.shom is a coefficient-energy mass and the comparison above is exactly what it needs).

Half two — the budget arithmetic

stepSevenVolumeExponent_le_of_gap is the tex's second sentence, in full:

  (d/2)(n'-n) ≤ (d/2)(|𝓑| + G)                        (the selection's gap)
              ≤ (d/2)·δ·((m-n) + 1) + (d/2)G          (e.bad.scale.proportion.bound)
              ≤ (d/2)·C₁⁻¹(1-α)((m-n) + 1) + (d/2)G   (δ ≤ C₁⁻¹(1-α))
              ≤ (1/4)(1-α)(m-n) + 1/4 + (d/2)G        (C₁ ≥ 2d+2, and 1-α ≤ 1)

At G = 6 — the printed gap max{n'-n, m-m'} ≤ |𝓑| + 6 — the constant is 3^{3d + 1/4}. strengthened the lower gap to the sharp n'-n ≤ |𝓑| + 3, and at G = 3 the constant improves to 3^{3d/2 + 1/4}. Both are delivered.

References

• ABK26, t.regularity Step 7c.
• ABK26, e.bad.scale.proportion.bound.

1. Half one — the volume-ratio cost of passing to a smaller set

theorem Algsuperdiff.Section4.Provider.Regularity.normalizedSqrt_le_volumeRatio_mul {IS IT volS volT : ℝ} (hvolS : 0 < volS) (hvolT : 0 < volT) (hmono : IS ≤ IT) : √(IS / volS) ≤ √(volT / volS) * √(IT / volT)

** (b), the scalar core.** If the mass IS carried by the smaller set is at most the mass IT carried by the larger one, then the volume-normalized square roots compare at the cost of the square root of the volume ratio:

  √(IS / volS)  ≤  √(volT / volS) · √(IT / volT) .

No hypothesis beyond positivity of the two volumes and monotonicity of the mass.

theorem Algsuperdiff.Section4.Provider.Regularity.sqrt_volumeRatio_le_rpow_three (d : ℕ) {volS volT : ℝ} {n n' : ℤ} (hvolSpos : 0 < volS) (hvolS : Real.rpow 3 (↑d * ↑n) ≤ volS) (hvolT : volT ≤ Real.rpow 3 (↑d * ↑n')) : √(volT / volS) ≤ Real.rpow 3 (↑d / 2 * (↑n' - ↑n))

The volume ratio at the two triadic scales. With 3^{dn} ≤ |S| (the tex-implicit lower bound on the truncated window (z + □_{n+1}) ∩ □_m) and |T| ≤ 3^{dn'} (the trivial upper bound on U_{n'-2} ⊆ z + □_{n'}), the square root of the volume ratio is the printed factor 3^{(d/2)(n'-n)}.

2. Half two — the budget arithmetic

theorem Algsuperdiff.Section4.Provider.Regularity.half_dim_mul_inv_le_quarter (d : ℕ) {C1 : ℝ} (hC1 : 2 * ↑d + 2 ≤ C1) : ↑d / 2 * C1⁻¹ ≤ 1 / 4

(d/2)·C₁⁻¹ ≤ 1/4's floor C₁ ≥ 2d + 2. This is the only place the C₁-largeness of the volume factor is used, and it is the +2 (not the naive C₁ ≥ 2d) that makes it go through with room to spare.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenVolumeExponent_le_of_gap (d : ℕ) {C1 alpha delta : ℝ} {B : ℕ} {n m n' G : ℤ} (hC1 : 2 * ↑d + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hnm : n ≤ m) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hgap : n' - n ≤ ↑B + G) (hbudget : ↑B ≤ delta * (↑(m - n).toNat + 1)) : ↑d / 2 * (↑n' - ↑n) ≤ ↑d / 2 * ↑G + 1 / 4 + 1 / 4 * stepSixExponent alpha n m

The volume exponent, bounded by the budget (second sentence).

At a gap n' - n ≤ |𝓑| + G, the budget |𝓑| ≤ δ((m-n)+1), the parameter choice δ ≤ C₁⁻¹(1-α)'s floor C₁ ≥ 2d + 2:

  (d/2)(n' - n)  ≤  (d/2)·G  +  1/4  +  (1/4)(1-α)(m-n) .

The +1/4 is the budget's own +1 (δ((m-n)+1) rather than δ(m-n)) weighted by (1/4)(1-α) ≤ 1/4.

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_stepSevenVolume_le (d : ℕ) {C1 alpha delta : ℝ} {B : ℕ} {n m n' : ℤ} (hC1 : 2 * ↑d + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hnm : n ≤ m) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hgap : n' - n ≤ ↑B + 6) (hbudget : ↑B ≤ delta * (↑(m - n).toNat + 1)) : Real.rpow 3 (↑d / 2 * (↑n' - ↑n)) ≤ Real.rpow 3 (3 * ↑d + 1 / 4) * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m)

The volume factor itself, at the printed gap n' - n ≤ |𝓑| + 6: 3^{(d/2)(n'-n)} ≤ 3^{3d + 1/4} · 3^{(1/4)(1-α)(m-n)}, i.e. the tex's C 3^{(1/4)(1-α)(m-n)} with the constant C = C(d) = 3^{3d + 1/4} made explicit.