HomStepThreeShallow #

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

Theorem B, §4.5: the shallow range (unit A2) #

The gap #

The correction: the word "Hence" in the paper silently extends Theorem C's display from j ≤ m - X_m(α) to ALL j ≤ m. It is proved (hence_holds_on_deep_range) that on the DEEP range the extension is free, so the gap is EXACTLY the shallow range m - X_m(α) < j ≤ m. The correction lists two routes, neither written in the manuscript:

(a) averaging over the scale-(m - X_m) descendants;
(b) invoking Theorem C at n₀ = min{j, m - X_m(α)}.

The obvious alternative — a volume comparison from □_m down to z + □_j — costs 3^{(d/2)(m-j)}, MUCH larger than the printed 3^{(1-α)X_m(α)}, and is what makes the gap real.

What is proved here: the analytic core of route (a) #

Route (a) is exact and costs NOTHING beyond the deep-range bound, because the normalized average over a cube is the average of the normalized averages over its descendants at any depth — CoarseGraining's descendantsENNAverage_lintegral_normalizedCubeMeasure_eq — and an average is at most a maximum. Hence:

  ⨍_R |∇u|² ≤ B  for every scale-(m - X) descendant R of Q
      ⟹  ⨍_Q |∇u|² ≤ B,

cubeAverage_le_of_descendants, at the depth where the descendants sit. Consequently the shallow-range display holds with the SAME constant as the deep-range one, i.e. the printed 3^{(1-α)X_m(α)} 3^{(1-α)(m-j)} is not merely sufficient but generous by the factor 3^{(1-α)(m-j)} ≥ 1.

What this module does NOT do — the two named identifications #

Plugging this into the abstract family F j z = ν^{1/2}‖∇u‖_{L²(z+□_j)} needs two carrier identifications, both absent and both purely mechanical:

the real/ℝ≥0∞ average bridge — Real.sqrt (normalizedSetAverage (openCubeSet R) (fun y => vecNormSq (∇u y))) versus (∫⁻ x, ENNReal.ofReal (vecNormSq (∇u x)) ∂normalizedCubeMeasure R).toReal (equal once vecNormSq ∘ ∇u is integrable on the cube, which the H1Function carrier supplies);
the indexing bridge — descendantsAtDepth Q n versus the manuscript's {z + □_{j₀}: z ∈ 3^{j₀}ℤ^d ∩ Q} at j₀ = Q.scale - n (scale_eq_sub_of_mem_descendantsAtDepth gives the scale; the centre enumeration is the missing half).

Neither is a statement-level item and neither needs the author: is a GAP IN THE MANUSCRIPT'S JUSTIFICATION, not a false display, and route (a) is sound. The correction's disposition is therefore unchanged — the display stands, the justification is recorded — and this module supplies the part of route (a) that is genuine analysis.

1. An average is at most a maximum #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.descendantsENNAverage_le_of_forall_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) {F : HCPolySupport.TriadicCube d → ENNReal} {B : ENNReal} (hF : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, F R ≤ B) :

HCPolySupport.descendantsENNAverage Q j F ≤ B

The descendant average of a family dominated by B is dominated by B.

2. Route (a): the shallow cube's average is controlled by its deep #

descendants

source

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeAverage_le_of_descendants {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (f : HCPolySupport.Vec d → ENNReal) {B : ENNReal} (hdeep : ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, ∫⁻ (x : HCPolySupport.Vec d), f x ∂HCPolySupport.normalizedCubeMeasure R ≤ B) :

∫⁻ (x : HCPolySupport.Vec d), f x ∂HCPolySupport.normalizedCubeMeasure Q ≤ B

The analytic core of route (a).

The normalized average over a triadic cube is the AVERAGE of the normalized averages over its depth-j descendants (CoarseGraining's exact partition identity), hence at most their maximum. So a bound valid at every deep scale-(Q.scale - j) descendant transfers to the shallow cube Q itself, with NO loss — in particular without the 3^{(d/2)(m-j)} volume factor the naive argument would pay.

Documentation