ConclusionSeam1PerCube

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

Seam 1 of Step 3: the per-simplex fourth moment, regrouped onto the cubes

Provider/Multiscale/ConclusionSeam2.lean records, in its "What is not proved" list, exactly one geometric gap of the |b_L| display of ABK26's p.bfA.multiscalebound Step 3:

The first printed inequality of the display, which converts the per-simplex fourth moment ⨍_{𝔰 ∈ SW(□_n) ∩ 𝒲(□_n,k)} |(k_L - k_{n-k-h_k})_𝔰|⁴ into the per-cube one. It needs the piecewise-constant reading of k on the cells of SW(□_m), which is not proved.

ConclusionSeam3Closure's own list of open items repeats it verbatim. This module proves that conversion, in the corrected reading.

The step, exactly

(h)_𝔰 is read as the manuscript reads it: the constant value that a piecewise-affine field takes on the cell, i.e. its cell mean ⨍_𝔰 h (CoarseGraining's volumeAverageMat T.openCarrier). With that reading the step is Jensen on each cell followed by the exact tiling of a Whitney cube by its cells:

∑_{𝔰 ∈ S(□)} (|𝔰|/|□_m|) |(k_L − k_j)_𝔰|⁴
      ≤ C(d) · (|□|/|□_m|) ⨍_□ |k_L − k_j|⁴ ,

sum_cellWeight_mul_simplexIncrementFourth_le, and its sum over the Whitney layer 𝒲(□_m,k) is layerSimplexFourthMass_le. Under the square root and the display's own prefactor γ 3^{−2γℓ} this is seamSimplexObject_le_mul_seamLayerObject: the per-simplex object is bounded by √(C(d)) times ConclusionSeam3.seamLayerObject, the per-cube object that seams 2 and 3 already price.

The weight |𝔰|/|□_m| is the proved SubadditiveDecomposition.cellWeight, i.e. the weight the manuscript's own subadditive decomposition carries ( e.sum-of-a-decomp); the cube weight |□|/|□_m| is the proved cubeMassRatio.

The constant, disclosed

simplexToCubeConst d = d⁴. It is a dimension-only constant and it sits under the printed C. Nothing else is lost: the two Jensen steps and the regrouping are sharp. A constant-free route would need ‖⨍_𝔰 h‖ ≤ ⨍_𝔰 ‖h‖ for the Euclidean operator norm, which is not proved anywhere (CoarseGraining has only the finite-sum form matrixOperatorNorm_descendantsAverageMat_le_descendantsAverage), and is not proved here.

The average convention, stated plainly (NOT hidden)

The printed display writes \avsum --- the cardinal average |A|⁻¹ ∑, --- over the simplices of the layer, and again over the cubes. The corrected route replaces the cube-side cardinal average by the volume-weighted sum ∑_□ (|□|/|□_m|), and that is the object ConclusionSeam2PerCube / ConclusionSeam3 carry. This module therefore runs the simplex side in the same volume-weighted normalization --- which is also the normalization of the manuscript's own subadditive decomposition, where the simplex sum first appears with the weights |𝔰|/|□_n|. The two normalizations differ by the layer's mass fraction W_k = ∑_{□ ∈ 𝒲(□_m,k)} |□|/|□_m|, and the identity W_k = ∑_{𝔰 ∈ layer} |𝔰|/|□_m| is proved here (sum_cellWeight_whitneySimplexCells_eq, summed over the layer). See "What is not proved".

What is not proved

• No cardinal-average form. Nothing below states the printed ⨍_{𝔰 ∈ SW(□_n) ∩ 𝒲(□_n,k)}; see the paragraph above. The exact missing input is volume (KuhnCell.openCarrier T) = cubeVolume T.supportCube / d ! (equivalently: any two cells of one cube have equal volume).
• No |b_L| assembly. The display's first inequality also produces the per-simplex sum from σ_{m-1}^{-1}|b_L(□_n)| − C, through e.sum-of-a-decomp, e.good.simplex.consequence, e.bounds.on.slopes.when.bad, l.bad.cubes.density and Hölder. None of that is here: this module proves only the per-simplex → per-cube conversion of the fourth-moment factor.
• No per-layer weight and no k-sum. records that the printed C 3^{−3k/4}(1 + 3^{2bh_hat_sep}e^{−cE⁻²γ⁻¹}) is not derivable in the corrected degree-2 reading; no sum over k is formed below and no per-layer weight is produced, used or approached.
• The printed step is neither stated nor used.'s false transition (→ 6468, √(av X²) ≤ av X) does not appear: the square root stays outside the volume-weighted fourth mass throughout.
• No e.bL.multiscale headline, no k₀ tuning, no terminal exp(−cE⁻²γ⁻¹) absorption, no seam-3 h_hat_sep reconciliation (the composition theorems below inherit ConclusionSeam3's own indices character for character).
• No face-to-face or simplicial-complex property of SW(□_m), and no claim that the closed cells cover: the tiling used is the proved exact half-open one plus the proved null boundary.

Main results

• Algsuperdiff.Section3.Provider.Multiscale.matrixOperatorNorm_simplexIncrementValue_pow_four_le
• Algsuperdiff.Section3.Provider.Multiscale.sum_cellWeight_mul_volumeAverage_eq
• Algsuperdiff.Section3.Provider.Multiscale.sum_cellWeight_whitneySimplexCells_eq
• Algsuperdiff.Section3.Provider.Multiscale.sum_cellWeight_mul_simplexIncrementFourth_le
• Algsuperdiff.Section3.Provider.Multiscale.layerSimplexFourthMass_le
• Algsuperdiff.Section3.Provider.Multiscale.seamSimplexObject_le_mul_seamLayerObject

References

• ABK26, p.bfA.multiscalebound Step 3, the |b_L| branch (align*; first inequality); \avsum; e.SW.def; e.simplex.def and the simplex volume; e.sum-of-a-decomp; the cell value (·)_𝔰; e.kmn.bounds.
• Provider/Whitney/SimplexPartition.lean (SW(□_m) and its exact tiling), Provider/Multiscale/SimplexDomains.lean (the null cell boundary), Provider/Multiscale/SubadditiveDecomposition.lean (cellWeight), Provider/Multiscale/Step3Seams.lean (cubeMassRatio_originCube_eq_div), Provider/Multiscale/ConclusionSeam3.lean (seamLayerObject, the consumers), Provider/Multiscale/ConclusionSeam2.lean and Provider/Multiscale/ConclusionSeam3Closure.lean (the proved local Γ₁ results consumed by the composition theorems; the single import of this module is the latter, which is already in the dependency cone of Algsuperdiff/Section3.lean).

Elementary matrix-norm arithmetic

Both directions of the Frobenius comparison, in squared form. These are CoarseGraining's proved matrixOperatorNorm_le_matrixFrobeniusNorm and abs_entry_le_matrixOperatorNorm, restated at the exponent the fourth moment uses.

The cell as a set of positive finite volume

Integrability on a cell

Every integrand below is continuous, and a cell is contained in the closed ball around its support cube; this is the containment chain the proved integrableOn_cubeSet_streamIncrementLpDensity already uses.

theorem Algsuperdiff.Section3.Provider.Multiscale.integrableOn_openCarrier_streamIncrementLpDensity {d : ℕ} {p : ℝ} (hp : 0 < p) (T : Whitney.KuhnCell d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : MeasureTheory.IntegrableOn (Stream.streamIncrementLpDensity p n m omega) T.openCarrier MeasureTheory.volume

The L^p density of a stream increment is integrable on a Kuhn cell.

Two elementary facts about the CoarseGraining volume average

The monotone form and the squared Jensen.

The cell value of the stream increment, and the per-cell Jensen

def Algsuperdiff.Section3.Provider.Multiscale.simplexToCubeConst (d : ℕ) : ℝ

The dimension-only constant of the per-simplex to per-cube step, d⁴. See the module docstring: it is the price of scalarizing the Euclidean operator norm through the Frobenius norm, and it sits under the printed C.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexToCubeConst d = ↑d ^ 4

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexIncrementValue {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) (T : Whitney.KuhnCell d) : HCPolySupport.Mat d

The manuscript's (k_m − k_n)_𝔰: the constant value of the stream increment on a cell of SW(□_m), read as the cell mean.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.simplexIncrementValue n m omega T = HCPolySupport.volumeAverageMat T.openCarrier (Algsuperdiff.Section3.Cutoff.finiteShellIncrement omega n m).toFun

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.simplexIncrementFourth {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) (T : Whitney.KuhnCell d) : ℝ

The per-simplex fourth moment |(k_m − k_n)_𝔰|⁴, in the exact Euclidean matrix operator norm the whole Stream chain uses.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Multiscale.simplexIncrementFourth_nonneg {d : ℕ} (n m : ℤ) (omega : Cutoff.ShellSeq d) (T : Whitney.KuhnCell d) : 0 ≤ simplexIncrementFourth n m omega T

theorem Algsuperdiff.Section3.Provider.Multiscale.matrixOperatorNorm_simplexIncrementValue_pow_four_le {d : ℕ} (T : Whitney.KuhnCell d) (n m : ℤ) (omega : Cutoff.ShellSeq d) : simplexIncrementFourth n m omega T ≤ simplexToCubeConst d * HCPolySupport.volumeAverage T.openCarrier (Stream.streamIncrementLpDensity 4 n m omega)

The per-cell Jensen step. The fourth power of the cell value is dominated by d⁴ times the cell average of the fourth-power density. Two squared Jensen applications and CoarseGraining's Frobenius pair; no hypothesis at all.

Regrouping the cells of one Whitney cube

The cells of a layer-k Whitney cube tile it exactly in the half-open realization, and each cell exceeds its open realization by a null set; so the open cells exhaust the cube up to a null set, and the integral over the cube splits as a finite sum over the cells.

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cellWeight_mul_volumeAverage_eq {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {k : ℕ} (hstep : hn k ≤ hn (k + 1) + 1) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn k) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f (HCPolySupport.cubeSet Q) MeasureTheory.volume) : ∑ T ∈ Whitney.whitneySimplexCells m hn k Q, cellWeight m T * HCPolySupport.volumeAverage T.openCarrier f = Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q * HCPolySupport.cubeAverage Q f

The regrouping, as an exact identity. For an integrand integrable on a layer-k Whitney cube □, the e.sum-of-a-decomp weighted sum of the cell means over the cells of □ is the cubeMassRatio-weighted cube mean.

No cell volume is evaluated: it cancels between the weight |𝔰|/|□_m| and the normalization of the cell mean. This is why the unproved simplex volume |△_n^π| = 3^{dn}/d! is not needed.

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cellWeight_whitneySimplexCells_eq {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {k : ℕ} (hstep : hn k ≤ hn (k + 1) + 1) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn k) : ∑ T ∈ Whitney.whitneySimplexCells m hn k Q, cellWeight m T = Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q

The layer mass fraction, at the simplices. Taking f = 1 in the regrouping identity: the cells of a layer-k Whitney cube carry exactly the cube's own mass. This upgrades the proved inequality Step3Seams.sum_cellWeight_whitneySimplexCells_le to an equality, and it is half of the dictionary between the printed cardinal average and the volume-weighted sum (the other half --- equal cell volumes --- is not proved; see the module docstring).

theorem Algsuperdiff.Section3.Provider.Multiscale.sum_cellWeight_mul_simplexIncrementFourth_le {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {k : ℕ} (hstep : hn k ≤ hn (k + 1) + 1) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn k) (n1 n2 : ℤ) (omega : Cutoff.ShellSeq d) : ∑ T ∈ Whitney.whitneySimplexCells m hn k Q, cellWeight m T * simplexIncrementFourth n1 n2 omega T ≤ simplexToCubeConst d * (Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q * HCPolySupport.cubeAverage Q (Stream.streamIncrementLpDensity 4 n1 n2 omega))

The per-simplex to per-cube step at one Whitney cube. Jensen on each cell, then the exact regrouping.

The Whitney layer, and the display

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.layerSimplexFourthMass {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) (n1 n2 : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The per-simplex fourth mass of the Whitney layer SW(□_m) ∩ 𝒲(□_m,k), in the volume-weighted normalization of e.sum-of-a-decomp. The index set is the layer's own cell family, written as the iterated sum over the layer's cubes and their cells.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Multiscale.layerSimplexFourthMass_le {d : ℕ} {m : ℤ} {hn : ℕ → ℕ} {k : ℕ} (hstep : hn k ≤ hn (k + 1) + 1) (n1 n2 : ℤ) (omega : Cutoff.CutoffSample d) : layerSimplexFourthMass m hn k n1 n2 omega ≤ simplexToCubeConst d * ∑ Q ∈ Whitney.whitneyLayer m hn k, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q * HCPolySupport.cubeAverage Q (Stream.streamIncrementLpDensity 4 n1 n2 ↑omega)

The per-simplex to per-cube step, over the whole Whitney layer. This is the fourth-moment content of the display's first printed inequality, in the corrected reading: the right-hand side is the volume-weighted layer fourth mass that ConclusionSeam2PerCube and ConclusionSeam3 price.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.seamSimplexObject {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) (ell : ℤ) (h : ℕ) (L : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The display's per-simplex left-hand object (with the prefactor pulled out of the square root): γ 3^{−2γℓ} (∑_{𝔰} (|𝔰|/|□_m|) |(k_L − k_{ℓ−h})_𝔰|⁴)^{1/2}.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Multiscale.seamSimplexObject_le_mul_seamLayerObject {d : ℕ} (M : ABKModel d) {m : ℤ} {hn : ℕ → ℕ} {k : ℕ} (hstep : hn k ≤ hn (k + 1) + 1) (ell : ℤ) (h : ℕ) (L : ℤ) (omega : Cutoff.CutoffSample d) : seamSimplexObject M m hn k ell h L omega ≤ ↑d ^ 2 * seamLayerObject M m hn k ell h L omega

The step, at the display. The per-simplex object of the b_L display's first printed inequality is bounded by √(simplexToCubeConst d) = d² times ConclusionSeam3.seamLayerObject, the per-cube object that seams 2 and 3 already price. Everything is pathwise and deterministic: no Orlicz index is created or moved.

Composition with the proved local seam-2 / seam-3 results