Step3Seams #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-3 seams of p.bfA.multiscalebound: Step 1 at the simplex carrier, #
and the per-layer majorant
This module supplies the two halves of that hypothesis that are provable below the competitor construction:
Step 1 at the manuscript's own simplex carrier.
Step1Assemblyprovese.good.simplex.consequence(assembled) at a triadic descendant cubeRof the Whitney cubeQ = z + square_j; the manuscript states it at a simplexspxofSW(square_n)contained inQ.SimplexResponseBoundproves the corresponding local estimates for the two crude legs, at the cost of the explicit dissection constantsimplexCrudeConst d s = 6 d (d+1)/(1-3^{2s-1})in place of the cube-carrier1/2. Below, that substitution is run through the whole of Step 1: the two normalized legs and the polarization assembly are re-derived at the simplex carrier, with the samesigmabararithmetic, the same correctioncstar^{-1}, and the constants80 -> 160 C(d,s),40 -> 80 C(d,s),320 -> 640 C(d,s),160 -> 320 C(d,s). The1/2 -> C(d,s)substitution is isolated in two abstract-real cores (normalized_flux_core,normalized_slope_core) which carry no cube, no sample and norpow: they take the four proved inequalities (Lambda <= 10 sigmabar_j,lambda^{-1} <= 10 sigmabar_j^{-1},sigmabar_j <= 4 sigmabar_i,sigmabar_j^{-2} <= T) and the crude base bound at an arbitrary nonnegative constantc, and return the assembled leg. Instantiated atc = 1/2they reproduceStep1Assembly's own constants (machine-checked by the twoexamples following the cores).The sub-family
Sof the statement is the good part of the layer for the first leg oflayerContriband the collar part for the second.The
4 gamma <= 1 - bgate, discharged.ConclusionAssembly/LayerMasscarryhgamma : 4 * gamma <= 1 - bas an explicit numeric A input. Wherever the printed admissibilityC(d) <= E cstar(or just4 <= E) and the printed scale restrictiongamma <= E^{-5}are in scope, the gate is a consequence, not a new assumption:AdmissibleGates.gamma_le_one_div_twenty_of_four_legivesgamma <= 1/20's own9 b <= 1givesb <= 1/9, so4 gamma <= 1/5 <= 8/9 <= 1 - bwith a factor~228of slack. This module is the first consumer with both in scope and proves the discharge.
What is not proved in this file #
- The collar leg's slope input
e.bounds.on.slopes.when.bad,|(grad. hatD_q)(spx)|^2/|q|^2 + |grad hatlinear_p(spx)|^2/|p|^2 <=^{2 b (k+h_k)}, is a statement about the piecewise-affine competitor(hatlinear_p, hatD_q)ofl.piecewise.affine.approx, not aboutbfA. It is not proved or assumed here:sum_sum_ofReal_cellWeight_le_ofReal_multakes the per-cell bound of whichever leg as its own abstract datumC.LayerUniform.leanand the later affine envelope providers supply concrete versions downstream. - The instantiation of
sum_of_a_decomp'saSatsimplexCoeffOn (coefficientCutoffTriadicCoeffFamily M L omega)— i.e. the at-consumer wiring with the competitor pair(F, G)— is downstream of the competitor construction and is not performed here;ConclusionCompetitor.leanlater performs that instantiation. - Seams 2 (the squared three-term composition) and 3 (the Orlicz half of the
3^{gamma hsep}reduction) are untouched in this file; seeConclusionSeam2*.lean,ConclusionSeam3*.lean, andConclusionAssemblyFinal.leanfor the later route.
Main results #
responseJ_simplexDomain_normalized_flux_le_of_notMem_bad_ae,responseJ_simplexDomain_normalized_slope_le_of_notMem_bad_ae: the two legs at the simplex carrier.blockVecDot_coarseBlockMatrix_simplexDomain_normalized_le_of_notMem_bad_ae:e.good.simplex.consequenceat the manuscript's own carrier.sum_cellWeight_whitneySimplexCells_le: the cells of a Whitney cube carry at most the cube's mass.sum_sum_ofReal_cellWeight_le_ofReal_mul: one Whitney layer ofe.sum-of-a-decomp, majorized in the shape of one leg oflayerContrib.
References #
- ABK26,
e.sum-of-a-decomp,e.good.simplex.consequence, Step 1, Step 3,e.SW.def.
The 4 gamma <= 1 - b gate, discharged #
The two abstract-real cores of the Step-1 assembly #
The two normalized legs at the simplex carrier #
Almost surely, on not B_osc(z + square_j) and not B_loc(z + square_j) and
under the induction state, for every L >= j, every scale i with j <= i <= m0, every Kuhn cell spx whose support cube is a triadic descendant of z + square_j at scale k, and every p̂,
J(spx, sigmabar_i^{-1/2} p̂, 0; a_L)
<= 160 C(d,1/4) . 3^{(j-k)/2}
( 1 + 8 C_{(e.big.Lambda.sensitivity)} cstar^{-1} gamma 3^{-2 gamma j}
||k_L - k_j||^2 ) |p̂|^2 ,
with C(d,1/4) = simplexCrudeConst d (1/4) = 6 d (d+1)/(1 - 3^{-1/2}). This is
Step1Assembly.responseJ_normalized_flux_le_of_notMem_bad_ae with the
cube-carrier crude constant 1/2 replaced by the dissection constant of
SimplexResponseBound.responseJ_simplexDomain_zero_flux_le_LambdaSq; the rest
of the chain (Lambda <= 10 sigmabar_j, lambda^{-1} <= 10 sigmabar_j^{-1},
sigmabar_j sigmabar_i^{-1} <= 4, the cstar^{-1} correction) is verbatim the
same.
Almost surely, on not B_osc and not B_loc and under the induction state,
J(spx, 0, sigmabar_i^{1/2} q̂; a_L)
<= 80 C(d,1/4) . 3^{(j-k)/2} . 3^{gamma (i - j)} |q̂|^2 .
Step1Assembly.responseJ_normalized_slope_le_of_notMem_bad_ae with 40
replaced by 80 C(d,1/4).
e.good.simplex.consequence at the manuscript's own carrier #
Almost surely, on not B_osc(z + square_j) and not B_loc(z + square_j) and
under the induction state, for every L >= j, every scale i with j <= i <= m0, every Kuhn cell spx whose support cube is a triadic descendant of z + square_j at scale k and every P̂ = (p̂, q̂),
| bfA_L^{1/2}(spx) bfAhom_i^{-1/2} P̂ |^2
<= 640 C(d,1/4) . 3^{(j-k)/2}
( 1 + 8 C_{(e.big.Lambda.sensitivity)} cstar^{-1} gamma 3^{-2 gamma j}
||k_L - k_j||^2 ) |p̂|^2
+ 320 C(d,1/4) . 3^{(j-k)/2} . 3^{gamma (i - j)} |q̂|^2 .
This is the local response-leg shape estimate for the simplex carrier: the
manuscript's spx is a genuine Kuhn simplex of SW(square_n), not a triadic
descendant cube, and the price of the carrier is exactly the explicit
dissection constant simplexCrudeConst d (1/4). At i = n - 1 and Q a
layer-k Whitney cube the q̂ exponent is the manuscript's gamma (k + h_k)
by Step1Assembly.rpow_gamma_mul_sub_scale_le_of_mem_whitneyLayer; that
instantiation is the consumer's.
The mass carried by the cells of one Whitney cube #
|R| / |square_m| in volume form.
The cells of a Whitney cube carry at most the cube's mass. The open
carriers of the cells of S_{m-(n+1)-h_{n+1}}(square) are pairwise disjoint
subsets of the cube, so their e.sum-of-a-decomp weights |spx| / |square_m|
sum to at most |square| / |square_m|. (Equality holds --- the cells tile the
cube --- but only the upper bound is consumed.)
One Whitney layer of e.sum-of-a-decomp, in the layerContrib shape #
The per-layer majorant, from a uniform per-cell bound. Let g be a
nonnegative cell functional which is bounded by C on the cells of the cubes of
a sub-family S of the layer, and vanishes on the cells of the layer's other
cubes. Then the layer's e.sum-of-a-decomp total is majorized by
C times the mass of S:
∑_{□ ∈ 𝒲(□_m,n)} ∑_{𝔰 ∈ S(□)} ofReal(|𝔰|/|□_m| . g 𝔰)
≤ ofReal( C . ∑_{□ ∈ S} |□|/|□_m| ) .
This is exactly the shape of one leg of ConclusionAssembly.layerContrib: for
the good leg S is the layer minus its bad cubes, g the quadratic form times
1_{¬𝓑}, and C = Ktot 3^{gamma(k+h_k)} (the layer reading of
e.good.simplex.consequence); for the collar leg S is the collar part of
the layer, g the competitor's quadratic form times 1_{¬𝓑} 1_{𝒩(ℐ)}, and C = Ccol 3^{2b(k+h_k)} (e.bounds.on.slopes.when.bad). The mass of S is
then weakened to the layer mass (good leg) or to the bad mass (collar leg) by
Finset.sum_le_sum_of_subset_of_nonneg, giving hlayer of
LayerMass.toReal_tsum_simplexPartition_le_payload.