PrefDischarge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.mathcalE.annular.decomp.pre at the development's own carriers: the hpref slot #
ABK26, Section 4.1, e.mathcalE.annular.decomp.pre, Step 1. This module
discharges the last open mathematical input of the annular clause-(i)
endpoint:
IsAnnularDecompPre s m (jLegField M L m ω) (annularResponseMax M L m ω) C₁
at the absolute constant C₁ = 4, for every sample ω, every L, every
m, and every s ∈ (0, 1/4].
The three legs #
Step1.annularDecompPre_of reduces the target to hgrid, hcov and hcen. With
Jcov n := Σ_{j = n+1}^{m} Jann j n(the annular cover leg), andJcen n := J(□_n)(the centre leg,centreResponseMax),
the three legs are:
hgrid-- the manuscript's cover,3^n ℤ^d ∩ □_m = {0} ∪ ⋃_{j=n+1}^m (3^n ℤ^d ∩ (□_j ∖ □_{j-1})). Landed asStep1.exists_mem_latticeAnnulusSet; the carrier identification ofCarrierIdentificationis what lets the annulus entries be recognized asjLegFieldentries.hcov-- the interchange, whichStep1Assembly.tsum_annFam_rowandStep1Assembly.annDouble_eq_tsum_rowsmake an identity:C_cov = 1, no loss.hcen-- the centre resummation. Its only structural input is the one-step subadditivity ofJat depth one and constant one, which is CoarseGraining's unconditionalCh05.Section53.JUpperBoundWeakNorms.responseJOnCube_le_childResponseJAverageOnFamilyAtDepthread at the origin cube, plus the identification of the3^dchildren of□_nas{□_{n-1}} ∪ (3^{n-1}ℤ^d ∩ (□_n ∖ □_{n-1})).Step1Assembly.tsum_centre_lethen closes it atC_cen = 3.
C₁ = C_cov + C_cen = 1 + 3 = 4.
Three things worth recording #
- No event, no probability, no regime. Step 1 is deterministic: the
target holds for every
ω. The finiteness the closure needs comes fromAssemblyFeed.jLegField_le_uniform, which is CoarseGraining's scale-free uniform response bound -- itself unconditional. Consequently the honest clause-(i) event never enters, and nom ≤ Lside condition is needed either. - Because the theorem below is proved on the full sample space, that
obligation is vacuous: the
∀ ωstatement is invariant under every map of the sample space,Nincluded. The slot wrapperannularDecompPre_slot_of_mem_annularEventtherefore also holds at−ωwhenever it holds atω, with no extra input. - The subadditivity is at depth one and constant one, exactly as printed.
Shared carrier #
The annulus family used here is the canonical annularResponseMaxPref from
CarrierIdentification. The annularResponseMax name in FinalStitch aliases
that family, so the endpoint's hpref slot uses the same object.
References #
- ABK26.
Part A -- the centre leg J(□_n) #
The centre leg of the Step-1 split: the scalar response maximum of
ã_{L,m} on the origin cube □_n, 0-floored through the singleton lattice
maximum (the entries of every J-maximum in Section 4.1 are 0-floored the same
way; see AssemblyFeed.jLegField).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The centre leg is dominated by the full-grid J-leg at the same scale.
Part B -- the 3^d children of □_n in the lattice enumeration #
Part C -- the one-step subadditivity of the centre leg #
The Step-1 centre step:
J(□_n) ≤ ⨍_{z' ∈ 3^{n-1}ℤ^d ∩ □_n} J(z' + □_{n-1})
≤ max_{z' ∈ 3^{n-1}ℤ^d ∩ (□_n ∖ □_{n-1})} J(z' + □_{n-1}) + 3^{-d} J(□_{n-1}) .
The first inequality is CoarseGraining's unconditional response
subadditivity at depth one
(responseJOnCube_le_childResponseJAverageOnFamilyAtDepth, zero side
hypotheses); the second splits the 3^d children of □_n into the central one
□_{n-1} and the 3^d − 1 others, which are precisely the scale-(n−1)
lattice cubes of the annulus □_n ∖ □_{n-1} -- the manuscript's own indexing,
and the family annularResponseMaxPref … n (n−1) maximizes over exactly them.
The printed coefficient 1 on the maximum is what 3^{-d}·(3^d − 1) ≤ 1
gives.
Part D -- the annular cover leg and the grid split #
The annular cover leg: the sum, over the annuli □_j ∖ □_{j-1} meeting
□_m, of the scale-n annulus maxima.
Equations
- Algsuperdiff.Section4.Provider.Annular.annCoverSum M L m omega n = ∑ j ∈ Finset.Icc (n + 1) m, Algsuperdiff.Section4.Provider.Annular.annularResponseMaxPref M L m omega j n
Instances For
The Step-1 grid split: the full-grid J-maximum is at most the annular
cover leg plus the centre leg. This is the lattice cover 3^n ℤ^d ∩ □_m = {0} ∪ ⋃_{j=n+1}^m (3^n ℤ^d ∩ (□_j ∖ □_{j-1})) together with the carrier
identification.
Part E -- the summability of the annular family, and the interchange #
The annular family of annularResponseMaxPref against the Step-1 weight is
summable, unconditionally: it is dominated by one scale-free ellipticity constant
times a geometric weight.
The guarded cover row is the n-row of the annular family: the
manuscript's interchange, as an identity.
Part F -- the Step-1 shape at the development's carriers #
e.mathcalE.annular.decomp.pre at the development's own carriers, at the
absolute constant C₁ = 4.
Unconditional in the sample: no good event, no probability, no smallness regime
and no m ≤ L side condition. The hypotheses are exactly the manuscript's own
typing and range data.
Part G -- the hpref slot of the clause-(i) endpoint #
The hpref slot of the annular clause-(i) endpoint, discharged.
This is the exact binder shape the endpoint carries -- the honest clause-(i) event
𝒢₀(m; C_cg) ∩ 𝒢₁(m; s, √c⋆ γ^{−1/2}) in front, ∀ L ≥ m inside -- at the
absolute constant C₁ = 4.
Both quantifiers are pure weakenings of annularDecompPre_jLegField: neither
the event nor m ≤ L is used.