PayloadSandwich

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

The payload sandwich: joining the on-grid domination to the block payload

Two halves of the coarse-ellipticity payload are proved separately and left uncomposed:

• Provider/CoarseEllipticity/GridDomination.lean discharges hgrid --- the domination of each leg's observable by the weighted series of Chapter 4 grid maxima Ch04.maxDescendant{SigmaStarInv,B}MatrixNormCoeffFieldAtScale read at the coefficient cutoff --- against an arbitrary majorizing family G;
• Provider/CoarseEllipticity/BlockPayload.lean turns a per-cube block estimate into each leg's payload conjunction, but through the gridSupAbs carrier blockGridSup, i.e. through a supremum of a family indexed by triadic cubes.

The two carriers differ: the identification maxDescendantBMatrixNormAtScale_eq_gridSupAbs of GridWeights.lean is stated at the deterministic sample space Ch02.TriadicCoeffFamily d, and composing the halves at a random coefficient family is an additional step. This module proves that step, adds the missing sigma_*^{-1} twin, adds the top-scale step that prices the gap-0 fold's summand against the scale-m-1 grid, and supplies the folded-amplitude arithmetic in which the two halves meet.

What is joined, in one line

Ch04.maxDescendant...CoeffFieldAtScale (cu_m) (m-1-k) a  =  blockGridSup d m k F a
Ch04.maxDescendant...CoeffFieldAtScale (cu_m)  m     a  <=  blockGridSup d m 0 F a

with F the per-cube Chapter 4 coefficient-field norm defined here. The first is an equality (both sides are the same finite supremum, on both branches of the AELocallyUniformlyEllipticField dite); the second is the top-scale step, CoarseGraining's Ch02.coarse...MatrixNorm_le_maxDescendant...AtScale at the singleton descendantsAtScale Q Q.scale = {Q}, i.e. the one-cube half of e.ellipticities.monotone.ordered / e.bound.one.cube.by.lambdas. Its constant is 1.

What composes outright, and what remains an explicit obligation

• Upper leg: the identifications below discharge hgrid outright, at the leg's own cutoff index, with NO binder on the grid family. What is left over is the per-cube block estimate hblock / hblockO1 / hblockOexp (p.bfA.multiscalebound, i.e. e.bL.multiscale) together with the source's own series data --- the shape in which threeTermSplit_cutoffUpperEllipticity_of_finiteQLtTwoPresplit consumes them.
• Lower leg: hgrid can only be discharged against an L-free family built from one named binder hLunif, the per-cube L-uniform majorant. This is not a corollary of the identification: the Chapter 4 grid maxima read Cutoff.coefficientCutoff M.nu L omega, and no L-free majorant is constructible here. hLunif is exactly the sup_{L >= m-1} printed on the left of e.slstar.multiscale: together with hblock at the same Xc, the pair is that display. It stays an explicit proof obligation of the lower leg's producers (twoTermFamilySplit_cutoffLowerEllipticityInv_of_finiteQPresplit and its q < 2 twin), not evidence that the source display has been proved.

What is not proved here and remains an interface obligation

1. hblock / hblockO / hblockO1 / hblockOexp --- the per-cube block estimate p.bfA.multiscalebound (e.slstar.multiscale; e.bL.multiscale).
2. hLunif --- the lower leg's L-uniformity, as above.
3. The small-m branch (p.base.case / l.mathcal.E.to.Lambdas) is untouched here; it is a separate producer's.
4. The q > 2 re-plumb: everything at the observable layer here is at the exponent q = 2 (hqval).

References

• ABK26, p.cg.ellipticity.bounds from p.bfA.multiscalebound (the composite: lower upper; the summed poles; the absorption gate).
• ABK26, e.slstar.multiscale and e.bL.multiscale.
• ABK26, e.ellipticities.monotone.ordered and e.bound.one.cube.by.lambdas --- the one-cube/grid ordering implemented by the top-scale step.
• ABK26, l.maximums.Gamma.s (e.maxy.bound).
• Provider/CoarseEllipticity/GridWeights.lean (the local seam handled here), .../BlockPayload.lean and .../GridDomination.lean (the two halves), .../GridDominationAllQ.lean (the q >= 2 extension), Provider/ErrorComparison/ExponentMonotonicity.lean (the display whose one-cube half the top-scale step uses).

1. The per-cube Chapter 4 coefficient-field norms

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseSigmaStarInvNormCoeffField {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : ℝ

|sigma_*^{-1}(R; a)| at the Chapter 4 ambient coefficient field: CoarseGraining's one-cube norm on the a.e.-locally elliptic support, 0 off it --- the per-cube datum whose grid maximum is Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseBNormCoeffField {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : ℝ

|b(R; a)| at the Chapter 4 ambient coefficient field, the upper leg's per-cube datum.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseSigmaStarInvNormCoeffField_nonneg {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : 0 ≤ coarseSigmaStarInvNormCoeffField R a

The lower per-cube datum is a matrix norm, hence nonnegative on both branches.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseBNormCoeffField_nonneg {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) : 0 ≤ coarseBNormCoeffField R a

The upper per-cube datum is a matrix norm, hence nonnegative on both branches.

2. blockGridSup A

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGridSup_comp {Omega : Type u_1} {Omega' : Type u_2} (d : ℕ) (m : ℤ) (k : ℕ) (X : HCPolySupport.TriadicCube d → Omega' → ℝ) (g : Omega → Omega') (omega : Omega) : blockGridSup d m k (fun (R : HCPolySupport.TriadicCube d) (o : Omega) => X R (g o)) omega = blockGridSup d m k X (g omega)

The grid maximum only reads the sample point through the family, so precomposing every cube's observable with one map is the same as evaluating the grid maximum at the image point. This is what carries the identification below from the coefficient field to the cutoff sample space.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockGridSup_const_mul {Omega : Type u_1} (d : ℕ) (m : ℤ) (k : ℕ) {c : ℝ} (hc : 0 ≤ c) (X : HCPolySupport.TriadicCube d → Omega → ℝ) (omega : Omega) : blockGridSup d m k (fun (R : HCPolySupport.TriadicCube d) (o : Omega) => c * X R o) omega = c * blockGridSup d m k X omega

A nonnegative constant passes through the grid maximum: the normalizer sigmabar_{m-1}^{(-1)} of the legs can sit inside the per-cube family or outside the maximum, indifferently.

3. The Chapter 2 identification, sigma_*^{-1} twin

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvMatrixNormAtScale_eq_gridSupAbs {d : ℕ} (m : ℤ) (k : ℕ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) a = gridSupAbs (HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) ⋯ (fun (R : HCPolySupport.TriadicCube d) (b : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) => HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R b) a

The on-grid carrier identification, sigma_*^{-1} twin. The missing companion of GridWeights.maxDescendantBMatrixNormAtScale_eq_gridSupAbs: CoarseGraining's per-scale grid maximum, the quantity Ch02.lambdaSqFinite is defined from, is exactly gridSupAbs at the one-cube norms |sigma_*^{-1}(R; a)|.

4. The Chapter 4 identification: the

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvCoeffField_eq_blockGridSup {d : ℕ} (m : ℤ) (k : ℕ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) a = blockGridSup d m k coarseSigmaStarInvNormCoeffField a

The, lower half. The Chapter 4 ambient grid maximum at scale m-1-k IS this repository's blockGridSup at the per-cube Chapter 4 norms --- on the a.e.-locally elliptic branch by the Chapter 2 identification, off it because both sides are the supremum of the zero family. This is the equality GridWeights.lean flags as "an additional, unlanded step".

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBCoeffField_eq_blockGridSup {d : ℕ} (m : ℤ) (k : ℕ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) a = blockGridSup d m k coarseBNormCoeffField a

The, upper half: the b twin of maxDescendantSigmaStarInvCoeffField_eq_blockGridSup.

5. The top-scale step

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvMatrixNormAtScale_top_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q Q.scale a = HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q a

At its own scale a cube's only descendant is itself, so the grid maximum there is the one-cube norm.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBMatrixNormAtScale_top_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q Q.scale a = HCPolySupport.Book.Ch02.coarseBMatrixNorm Q a

The b twin of maxDescendantSigmaStarInvMatrixNormAtScale_top_eq.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvMatrixNormAtScale_top_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {l : ℤ} (hl : l ≤ Q.scale) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q Q.scale a ≤ HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q l a

The top-scale step (Chapter 2, lower). The depth-0 one-cube quantity is dominated by the grid maximum at any deeper scale, with constant 1. This is the one-cube half of e.ellipticities.monotone.ordered / e.bound.one.cube.by.lambdas (ABK26), already available in CoarseGraining, and it is what lets the gap-0 fold be priced against the scale-m-1 grid rather than against a separate object.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBMatrixNormAtScale_top_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {l : ℤ} (hl : l ≤ Q.scale) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q Q.scale a ≤ HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q l a

The top-scale step (Chapter 2, upper).

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvCoeffField_top_le_blockGridSup {d : ℕ} [NeZero d] (m : ℤ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) m a ≤ blockGridSup d m 0 coarseSigmaStarInvNormCoeffField a

The top-scale step at the Chapter 4 carrier, lower: the depth-0 grid maximum is dominated by blockGridSup at gap 1.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBCoeffField_top_le_blockGridSup {d : ℕ} [NeZero d] (m : ℤ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) m a ≤ blockGridSup d m 0 coarseBNormCoeffField a

The top-scale step at the Chapter 4 carrier, upper.

6. The sandwich at the observable carrier

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffSigmaStarInvBlockFamily {d : ℕ} (M : ABKModel d) (L : ℤ) (scaling : ℝ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : ℝ

The lower leg's per-cube normalized grid datum at the cutoff index L.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffBBlockFamily {d : ℕ} (M : ABKModel d) (L : ℤ) (scaling : ℝ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : ℝ

The upper leg's per-cube normalized grid datum at the cutoff index L.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.scaledB_le_blockGridSup {d : ℕ} (M : ABKModel d) (m : ℤ) (k : ℕ) {scaling T : ℝ} (hscaling : 0 ≤ scaling) {Y : HCPolySupport.TriadicCube d → Cutoff.CutoffSample d → ℝ} {L : ℤ} {omega : Cutoff.CutoffSample d} (hT : T ≤ HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k) (Cutoff.coefficientCutoff M.nu L omega)) (hdom : ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), scaling * coarseBNormCoeffField R (Cutoff.coefficientCutoff M.nu L omega) ≤ Y R omega) : scaling * T ≤ blockGridSup d m k Y omega

The sandwich, upper leg, one scale.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvCoeffField_top_le {d : ℕ} [NeZero d] (m : ℤ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) m a ≤ HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - 1 - ↑0) a

The top-scale step, stated between the two grid maxima the fold compares.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBCoeffField_top_le {d : ℕ} [NeZero d] (m : ℤ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) m a ≤ HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - 1 - ↑0) a

The top-scale step, upper, between the two grid maxima the fold compares.

7. The folded split and the folded amplitude

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedAmp (sigma ctop : ℝ) (a : ℕ → ℝ) (k : ℕ) : ℝ

The amplitude of a folded lane ctop * U_0 + U_k, at the two-term l.Gamma.sigma.triangle constant.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedAmp sigma ctop a k = HCPolySupport.IndependentSums.gammaTriangleConst sigma * (ctop * a 0 + a k)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedAmp_pos {sigma ctop : ℝ} {a : ℕ → ℝ} (hctop : 0 ≤ ctop) (ha : ∀ (k : ℕ), 0 < a k) (k : ℕ) : 0 < foldedAmp sigma ctop a k

The folded amplitude is positive whenever the unfolded one is.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_foldedAmp {mass rho sigma ctop : ℝ} {a : ℕ → ℝ} (hrho : 0 < rho) (hasum : Summable fun (k : ℕ) => mass * gridWeight rho k * a k) : Summable fun (k : ℕ) => mass * gridWeight rho k * foldedAmp sigma ctop a k

Folding adds one constant series to the amplitude series, so summability is inherited.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_foldedAmp_le {mass rho sigma ctop S : ℝ} {a : ℕ → ℝ} (hmass : 0 ≤ mass) (hrho : 0 < rho) (hctop : 0 ≤ ctop) (ha : ∀ (k : ℕ), 0 ≤ a k) (hasum : Summable fun (k : ℕ) => mass * gridWeight rho k * a k) (hS : ∑' (k : ℕ), mass * gridWeight rho k * a k ≤ S) : ∑' (k : ℕ), mass * gridWeight rho k * foldedAmp sigma ctop a k ≤ HCPolySupport.IndependentSums.gammaTriangleConst sigma * (ctop * a 0 * (mass * rho⁻¹) + S)

The folded scale sum: the gap-0 fold costs one extra rho^{-1} slot at the top-scale amplitude, nothing else.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.foldedBlockPole (d : ℕ) (sigma A mass rho ctop : ℝ) (p : ℕ) : ℝ

The explicit folded pole: the constant the exceptional lane's amplitude sums to after the gap-0 fold and the rounded-up e.maxy.bound polynomial.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaTriangleConst_mul_tsum_foldedGridBlockAmp_le {d : ℕ} {mass rho sigma A ctop : ℝ} (hmass : 0 ≤ mass) (hrho : 0 < rho) (hctop : 0 ≤ ctop) (hA : 0 ≤ A) (p : ℕ) (hp : sigma⁻¹ ≤ ↑p) : HCPolySupport.IndependentSums.gammaTriangleConst sigma * ∑' (k : ℕ), mass * gridWeight rho k * foldedAmp sigma ctop (fun (j : ℕ) => gridBlockAmp d sigma A j) k ≤ foldedBlockPole d sigma A mass rho ctop p

The consumers' hBexp input, at the folded e.maxy.bound amplitude and the explicit pole.

8. The composed payload producers

9. The elementary ell^{q/2} pre-split

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_add_le_mul_rpow_add_rpow {x y t : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (ht : 1 ≤ t) : (x + y) ^ t ≤ 2 ^ (t - 1) * (x ^ t + y ^ t)

The elementary ell^{q/2} pre-split, at an abstract exponent: (x + y)^t <= 2^{t-1} (x^t + y^t) for 1 <= t and nonnegative x, y. This is the real-valued form of Mathlib's NNReal.rpow_add_le_mul_rpow_add_rpow, which Mathlib does not export over ℝ.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_half_add_le_mul_rpow_half_add_rpow_half {x y q : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hq : 2 ≤ q) : (x + y) ^ (q / 2) ≤ 2 ^ (q / 2 - 1) * (x ^ (q / 2) + y ^ (q / 2))

The pre-split at the exponent the coarse-grained ellipticity aggregate carries: (x + y)^{q/2} <= 2^{q/2 - 1} (x^{q/2} + y^{q/2}) for 2 <= q.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_inv_add_le_add_rpow_inv {a b t : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : 1 ≤ t) : (a + b) ^ (1 / t) ≤ a ^ (1 / t) + b ^ (1 / t)

The companion root step: (a + b)^{1/t} <= a^{1/t} + b^{1/t} for 1 <= t, i.e. (a+b)^{2/q} <= a^{2/q} + b^{2/q} at t = q/2.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_rpow_presplit_le {w X Y : ℕ → ℝ} {t : ℝ} (hw : ∀ (n : ℕ), 0 ≤ w n) (hX : ∀ (n : ℕ), 0 ≤ X n) (hY : ∀ (n : ℕ), 0 ≤ Y n) (ht : 1 ≤ t) (hXs : Summable fun (n : ℕ) => w n * X n ^ t) (hYs : Summable fun (n : ℕ) => w n * Y n ^ t) (hsum : Summable fun (n : ℕ) => w n * (X n + Y n) ^ t) : ∑' (n : ℕ), w n * (X n + Y n) ^ t ≤ 2 ^ (t - 1) * (∑' (n : ℕ), w n * X n ^ t + ∑' (n : ℕ), w n * Y n ^ t)

The pre-split, applied termwise inside a weighted ell^t aggregate.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_inv_tsum_presplit_le {w X Y : ℕ → ℝ} {t : ℝ} (hw : ∀ (n : ℕ), 0 ≤ w n) (hX : ∀ (n : ℕ), 0 ≤ X n) (hY : ∀ (n : ℕ), 0 ≤ Y n) (ht : 1 ≤ t) (hXs : Summable fun (n : ℕ) => w n * X n ^ t) (hYs : Summable fun (n : ℕ) => w n * Y n ^ t) (hsum : Summable fun (n : ℕ) => w n * (X n + Y n) ^ t) : (∑' (n : ℕ), w n * (X n + Y n) ^ t) ^ (1 / t) ≤ 2 * ((∑' (n : ℕ), w n * X n ^ t) ^ (1 / t) + (∑' (n : ℕ), w n * Y n ^ t) ^ (1 / t))

The application shape at the aggregate. Splitting the deterministic and the random part INSIDE the ell^{q/2} aggregate, before taking the 2/q root, costs a dimension-free factor 2 and no pole.