ConclusionCompetitor #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.sum-of-a-decomp at the Step-3 coefficient family and competitor #
Multiscale.sum_of_a_decomp (SubadditiveDecomposition.lean; ABK26) is stated
at an abstract cell coefficient family aS and an abstract competitor
pair (F, G); LayerUniform.sum_sum_ofReal_two_leg_le_ofReal_layerContrib and
LayerUniform.toReal_tsum_simplexPartition_two_leg_le_payload are stated at
abstract cell functionals g_good, g_col. This module performs the
local provider instantiation: it instantiates aS at the manuscript's own
coefficient family, reads off the two concrete per-cell functionals, and shows
they land exactly in the two-leg shape the layer theorems consume.
The instantiation #
The cell coefficient object is cellCutoffCoeffOn M L omega π°:= simplexCoeffOn (coefficientCutoffTriadicCoeffFamily M L omega) π°, the same object at which
Step3Seams and LayerUniform prove Step 1. Two facts make the instantiation
free:
SimplexDissection.simplexDomain π°andSimplexDomains.kuhnCellDomain π°are the sameCh02.Domain d(same carrier, and their remaining fields are proofs), sosimplexCoeffOn's value is literally aCh02.CoeffOn (kuhnCellDomain π°);coarseBlockMatrix_cellCutoffCoeffOnrecords the identification, byrfl.sum_of_a_decomp's compatibility binderhaS: (aS π°).toCoeffField = a.toCoeffFieldholds byrflata:= (coefficientCutoffTriadicCoeffFamily M L omega).coeffOn β‘_m:restrictCoeffOnkeeps the representative field, andcoefficientCutoffCoeffOn_toCoeffFieldsays the representative iscoefficientCutoff M.nu L omegaon every cube ("only its locally derived ellipticity witness changes with the cube").
So sum_of_a_decomp_cutoff carries no coefficient binder at all: aS and
haS are gone, and what is left is the eight-binder affine A of
l.piecewise.affine.approx, transported verbatim.
The two concrete cell functionals #
g_good π° = ((p,q) . π_L(π°) (p,q)) 1_{Β¬π(π°)}
g_col π° = ((Fc π°,Gc π°) . π_L(π°) (Fc π°,Gc π°)) 1_{Β¬π(π°)} 1_{π° β π©(β)}
(goodCellForm, collarCellForm).
The two sub-families, and what is discharged #
The layer theorems take four data per leg (hSβ¦, hβ¦, hβ¦z, hmassβ¦). At
the concrete functionals two of them are theorems, not data:
- the good leg's sub-family is the whole layer (
Sgood n = π²(β‘_m,n)): the indicator1_{Β¬π}is already insideg_good, so the bad cubes contribute0and no restriction is needed.hSgoodissubset_rflandhgoodzis vacuous. - the collar leg's sub-family is
collarLayer = π²(β‘_m,n) β© π©(β).hScolisFinset.filter_subsetandhcolziscollarIndicator_of_notMemcomposed withwhitneyCubeOf_of_mem_whitneySimplexCells(collarLayer_zero).
hgood, hcol, hmassgood, hmasscol remain the caller's, in exactly the
interface style of LayerUniform; see below for which of them this repository
can and cannot supply.
The per-cell bounds, and the one thing they are not #
goodCellForm_le_stepOneLayerMajorant_ae and
collarCellForm_le_stepOneLayerMajorant_ae are the concrete readings of
LayerUniform.blockVecDot_coarseBlockMatrix_whitneySimplexCells_le_ae and
LayerUniform.blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae:
almost surely, for every layer, every cube of the layer (bad ones included
--- there the indicator kills the term) and every cell,
g_good π° β€ M(β‘, n, i, L, Ο; p, q) ,
g_col π° β€ 4 CgradΒ² 3^{2b(n+h_n)} . M(β‘, n, i, L, Ο; p, q) ,
with M = stepOneLayerMajorant the Step-1 majorant.
M is not constant on a layer. Every factor of it is (β‘.scale = m - n - h_n is fixed on π²(β‘_m,n), and multiscaleDescendantWeight,
3^{-2Ξ³β‘.scale}, 3^{Ξ³(i-β‘.scale)} depend on β‘ only through β‘.scale)
except the increment gauge βk_L - k_{β‘.scale}β_{W^{1,β}(β‘)}Β², which
genuinely varies over the layer. Turning M into the layer constant Ktot 3^{Ξ³(n+h_n)} that layerContrib wants is precisely the |b_L| branch ---
Step 2's business, not this module's --- and it is why hgood is left as the
caller's datum here. Nothing below asserts that a deterministic Ktot exists.
What is not proved, and what is carried as data #
- The affine A associated with
l.piecewise.affine.approx: its eight clauses are the bindershF,hG,hFc,hGc,hbadF,hbadG,hoffF,hoffGofsum_of_a_decomp_cutoff, transported binder for binder fromsum_of_a_decomp; and its collar gradient conclusion in the layer-envelope reading leaves standing is the pairhFv,hGvcarried insidecollarCellForm_le_stepOneLayerMajorant_ae, exactly asLayerUniformcarries it. Nothing here constructs that source object or asserts it is satisfiable, andCgradis a free real. - The collar-vs-bad mass comparison is
hmasscol, an explicit A input as inLayerUniform. Its twinhmassgoodis now at the whole layer, i.e.LayerMass.sum_cubeMassRatio_whitneyLayer_leatMass n := 6d 3^{-n}discharges it for any caller who pinsMassthere; it is kept as a binder only becauseMassis a parameter oflayerContrib. - The layer-uniform good constant
Ktot: see above. - The real-valued join of
sum_of_a_decomp_cutoffwithConclusionRoot.tsum_simplexPartition_cutoff_two_leg_le_ofReal_payloadneeds the finiteness of the intermediate[0,β]sum; it is not performed here, and both halves are proved separately so that a consumer can perform it once the layer constants are pinned.
Main results #
sum_of_a_decomp_cutoff:e.sum-of-a-decompat the manuscript's own coefficient family, right-hand side in the exact two-leg cell shape.goodCellForm_le_stepOneLayerMajorant_ae,collarCellForm_le_stepOneLayerMajorant_ae: the two concrete per-cell bounds, a.e., uniformly over layers, cubes and cells.collarLayer_zero: the collar leg vanishes off the collar sub-family.
References #
- ABK26,
e.sum-of-a-decomp(the display carrying the collar indicators);e.good.simplex.consequence; Step 1; Step 3;e.bounds.on.slopes.when.bad;e.SW.def;l.piecewise.affine.approx;r.gradient.bound.simplified;e.homs.defs.U.diag.
The coefficient family at the cells of SW(β‘_m) #
aS of e.sum-of-a-decomp, instantiated. The coefficient object of
the cutoff a_L on one cell of SW(β‘_m): the restriction of the cell's
support-cube representative, i.e. the very object at which Step3Seams and
LayerUniform prove Step 1. Its type is stated at kuhnCellDomain because
that is the carrier sum_of_a_decomp uses; simplexDomain is the same
Ch02.Domain d.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two carriers agree, so the two spellings of the cell's coarse block matrix agree.
haS of e.sum-of-a-decomp, discharged. Every cube of the cutoff
family carries the same representative field coefficientCutoff M.nu L omega
(coefficientCutoffCoeffOn_toCoeffField), and restrictCoeffOn keeps it, so
the cell object and the root-cube object have literally equal representatives.
The two concrete cell functionals of e.sum-of-a-decomp #
The good leg's cell functional: the load's own π_L(π°) quadratic form,
trimmed by 1_{Β¬π(π°)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The collar leg's cell functional: the competitor's own π_L(π°) quadratic
form at its cell constants, trimmed by 1_{Β¬π(π°)} and by 1_{π° β π©(β)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
e.sum-of-a-decomp at the cutoff family #
e.sum-of-a-decomp at the manuscript's own coefficient family, with the
right-hand side in the exact cell shape that
LayerUniform.toReal_tsum_simplexPartition_two_leg_le_payload consumes:
ofReal | (p,q) . π_L(β‘_m) (p,q) |
β€ β'_{π° β SW(β‘_m)} ( ofReal( (|π°|/|β‘_m|) g_good π° ) + ofReal( (|π°|/|β‘_m|) g_col π° ) ) .
The coefficient binders aS, haS of sum_of_a_decomp are gone; every
remaining hypothesis is a clause of l.piecewise.affine.approx /
e.hat.linear.properties, transported verbatim (see the module docstring).
The Step-1 majorant, as a layer quantity #
The Step-1 majorant at a cell of a Whitney layer, read at the simplex
carrier. This is the right-hand side of
LayerUniform.blockVecDot_coarseBlockMatrix_whitneySimplexCells_le_ae, named
so that the two per-cell bounds below can be read.
Every factor depends on β‘ only through β‘.scale --- which is constant on a
Whitney layer --- except the increment gauge
βk_L - k_{β‘.scale}β_{W^{1,β}(β‘)}Β²; see the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two concrete per-cell bounds #
The good leg's per-cell bound, concretely. Almost surely, for every
layer, every cube of the layer --- bad cubes included, where 1_{Β¬π} kills the
term --- and every cell of it, the concrete g_good at the framed load
πhom_i^{-1/2}(p,q) is at most the Step-1 majorant.
This is LayerUniform.blockVecDot_coarseBlockMatrix_whitneySimplexCells_le_ae
with the indicator put back in; the bad-cube case is the indicator's own
vanishing plus stepOneLayerMajorant_nonneg.
Almost surely, for every layer, every cube of the layer, every cell of it,
every load and every competitor cell constants satisfying the collar A of
e.bounds.on.slopes.when.bad, the concrete g_col at the framed competitor
constants is at most 4 CgradΒ² 3^{2b(n+h_n)} times the Step-1 majorant at the
load (p, q) --- the competitor's slopes are traded for the load, so the
majorant argument is the load, not the competitor.
LayerUniform.blockVecDot_coarseBlockMatrix_collar_whitneySimplexCells_le_ae
with the two indicators put back in. The hypotheses hFv, hGv are the
conditional A shape of clause 2 of e.hat.linear.properties in the reading
leaves standing; they are hypotheses, not theorems of this repository.
The collar sub-family, and the vanishing of the collar leg off it #
(π©(β) β© π²(β‘_m,n)), the collar part of one Whitney layer: the sub-family
S_col that LayerUniform.sum_sum_ofReal_two_leg_le_ofReal_layerContrib takes
on its second leg. The classification is by meeting the collar, which is
exactly what collarIndicator performs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The collar leg vanishes off the collar sub-family --- the hcolz datum
of the two-leg theorems, discharged at the concrete functional.