HomSpineCarrierBridge

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

Theorem B, §4.5: the two carrier bridges

What is still open

HomStepThreeShallow proved the analytic core of route (a): the normalized average over a cube is the AVERAGE of the normalized averages over its depth-j descendants, hence at most their maximum, so the deep-range bound transfers to the shallow range with NO loss. Its module docstring named two purely mechanical identifications as the remaining plug-in, and this module supplies exactly those two:

1. the real / ℝ≥0∞ average bridge — the abstract family F j z = ν^{1/2}‖∇u‖_{L²(z+□_j)} is built from the REAL Homogenization.volumeAverage (CoarseGraining's normalizedSetAverage is that abbreviation), while cubeAverage_le_of_descendants speaks about ∫⁻ · ∂normalizedCubeMeasure R. volumeAverage_eq_toReal_lintegral and its two one-sided corollaries identify them for a nonnegative integrable density;
2. the indexing bridge — descendantsAtDepth Q j versus the manuscript's {z + □_{j₀}: z ∈ 3^{j₀}ℤ^d ∩ □_m} at j₀ = Q.scale - j. latticeTranslate_of_mem_descendantsAtDepth produces, for each descendant, its scale, its lattice centre (z ∈ 3^{j₀}ℤ^d, the integer vector displayed), the identification □_R = z + □_{j₀} in the translate spelling the main statements use, and z ∈ □_m.

With these two, route (a) plugs into the hence_holds_on_deep_range with nothing left over.

Disposition of

Unchanged, and this module does not change it: the correction records a GAP IN THE MANUSCRIPT'S JUSTIFICATION (the word "Hence" in the paper), not a false display. Route (a) is sound, the printed constant 3^{(1-α)X}3^{(1-α)(m-j)} is in fact generous, and route (a) does not need the author.

1. Bridge one: the real average versus the ℝ≥0∞ cube integral

theorem Algsuperdiff.Section4.Provider.Homogenization.volumeAverage_eq_toReal_lintegral {d : ℕ} (R : HCPolySupport.TriadicCube d) {f : HCPolySupport.Vec d → ℝ} (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hint : MeasureTheory.IntegrableOn f (HCPolySupport.openCubeSet R) MeasureTheory.volume) : ∫⁻ (x : HCPolySupport.Vec d), ENNReal.ofReal (f x) ∂HCPolySupport.normalizedCubeMeasure R = ENNReal.ofReal (HCPolySupport.volumeAverage (HCPolySupport.openCubeSet R) f)

Bridge one. For a nonnegative density integrable on the cube, the manuscript's real normalized average and CoarseGraining's ℝ≥0∞ normalized cube integral are the same number.

2. Bridge two: descendants versus the manuscript's lattice translates

theorem Algsuperdiff.Section4.Provider.Homogenization.triadicCubeShift_eq_cubeCenter {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.triadicCubeShift R = HCPolySupport.cubeCenter R

The triadic shift of a cube is its centre.

theorem Algsuperdiff.Section4.Provider.Homogenization.triadicCubeShift_mem_lattice {d : ℕ} (R : HCPolySupport.TriadicCube d) (i : Fin d) : HCPolySupport.triadicCubeShift R i = ↑(R.index i) * 3 ^ R.scale

The centre of a triadic cube lies on the lattice 3^{scale} ℤ^d — the manuscript's z ∈ 3^{j₀}ℤ^d.

theorem Algsuperdiff.Section4.Provider.Homogenization.latticeTranslate_of_mem_descendantsAtDepth {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {j : ℕ} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) : R.scale = Q.scale - ↑j ∧ HCPolySupport.openCubeSet R = (fun (y : HCPolySupport.Vec d) => HCPolySupport.triadicCubeShift R + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d R.scale) ∧ (∀ (i : Fin d), HCPolySupport.triadicCubeShift R i = ↑(R.index i) * 3 ^ R.scale) ∧ HCPolySupport.triadicCubeShift R ∈ HCPolySupport.openCubeSet Q

Bridge two. Each depth-j descendant of Q is exactly one of the manuscript's lattice translates z + □_{j₀} at j₀ = Q.scale - j, with z ∈ 3^{j₀}ℤ^d ∩ □_{Q.scale}.

The four conjuncts are the four things a consumer of route (a) needs: the scale, the translate spelling that the main statements' windows use ((fun y => z + y) '' openCubeSet (originCube d j₀)), the lattice membership of the centre, and its membership in the ambient cube.