PrincipalResponseBudget

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the budget delta <=^2 |log gamma|^2 gamma

This module assembles the budget printed in ABK26, inside the proof of e.use.also.for.the.upper.bound, for the annealed defect

  delta = 2 E[ bfJ(cu_n, bfAhom_L^{-1/2} e, bfAhom_L^{1/2} e; a_L) ]

proved as cubeAnnealedProbeDefect in ...ApproximateRecurrence.PrincipalResponseSwitch, at the cutoff index L (the manuscript's m - h).

The manuscript's own chain is

  delta <= C 3^{t(m-h-n)} E[ mathcalE_{t,infinity,2}(cu_{m-h}; a_{m-h}, shom_{m-h})^2 ]
        <= C E^2 |log gamma|^2 gamma ,        t := |log gamma|^{-1} .

Its three legs are supplied by the three sibling modules and combined here:

• the deterministic leg (e.mathcalE.monotone.ordered squared, then e.bound.one.cube.by.mathcalE) is ...PrincipalResponseBudgetDescent.doubledResponseJ_annealedProbe_originCube_le;
• the Orlicz-to-moment leg -- the only consumption of the induction state d.mathcalS.def -- is ...PrincipalResponseBudgetMoment.integral_sq_le_of_isTwoTermBigOWith_gammaSigma;
• the domination of the heavy Gamma_{1/2} scale by the light Gamma_2 scale is ...PrincipalResponseBudgetScales.exp_leg_le_window_gaussian_leg.

What this module adds is the carrier bookkeeping: the defect is an integral against the pushforward Cutoff.coefficientCutoffLaw M L, whereas the induction state lives on the cutoff-sample law, so the integral is transported by integral_map and the integrand identified, cube by cube, with the Chapter 2 doubled response of the literal cutoff coefficient family.

The regime, stated honestly

l.approximate.recurrence.formula assumes e.lower.bound.cgamma.cond.again.0: E >= C cstar^{-1} and gamma <= E^{-5}, with C = C(d) free until e.cgamma.constraints. Two hypotheses below encode it: hgamE is literally gamma <= E^{-5}, and h: 6 <= E is a numerical floor on that free constant. The floor is what E >= C cstar^{-1} delivers once cstar <= 1; that last inequality is a separately tracked development gap and is not invoked, the floor being carried as an explicit hypothesis instead.

The window hsw : s in [8 gamma, 1] is the window of e.new.induction.for.shom itself. The manuscript's t := |log gamma|^{-1} is the instance s = |log gamma|^{-1}, and cubeAnnealedProbeDefect_le_logSq_budget is that instance, with s^{-2} become the printed |log gamma|^2; the hypothesis that |log gamma|^{-1} lies in the window is then explicit, as it must be.

What is not here

The cube is the origin cube cu_n, not the translate z + cu_n printed in the display of e.use.also.for.the.upper.bound; the transfer by real-translation stationarity is the one step a consumer at a translated cube still owes, exactly as recorded in ...PrincipalResponseSwitch. The manuscript's own random vector G_{-(h)_{z+cu_n}} P_z is still absent, P_z having no definition in this repository. Consequently nothing below claims e.use.also.for.the.upper.bound itself, nor any source node, nor any fraction of one: what is established is the budget for the proved defect cubeAnnealedProbeDefect, which is the input the proved switch ...PrincipalResponseSwitch.annealedCubeBlockQuadratic_le_annealedLimitBlockQuadratic consumes.

Main results

• integral_blockJObservable_coefficientCutoffLaw_eq_integral_cutoffSampleLaw, blockJObservableCubeSetBlockVec_coefficientCutoff_eq_doubledResponseJ: the carrier transfer.
• cubeAnnealedProbeDefect_le_rpow_mul_orliczScales: the defect against the two scales of e.new.induction.for.shom.
• principalResponseBudgetConst: the absolute constant, and its positivity.
• cubeAnnealedProbeDefect_le_budget: the budget, at a free window exponent s.
• cubeAnnealedProbeDefect_le_budget_of_gap: the same with the scale gap behind an explicit gate.
• cubeAnnealedProbeDefect_le_logSq_budget: the manuscript's own instance s = |log gamma|^{-1}, i.e. delta <=^{2K} E^2 |log gamma|^2 gamma.

References

• ABK26, d.mathcalS.def, e.new.induction.for.shom.
• ABK26, the labels l.approximate.recurrence.formula, e.lower.bound.cgamma.cond.again.0, e.cgamma.constraints, e.recurrence.params, d.mathcalS.def, e.new.induction.for.shom, e.mathcalE.monotone.ordered, e.bound.one.cube.by.mathcalE, e.use.also.for.the.upper.bound.
• ABK26, (e.use.also.for.the.upper.bound and its proof; the chain is the align* display, its third line and its final bound).

Carrier transfer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integral_blockJObservable_coefficientCutoffLaw_eq_integral_cutoffSampleLaw {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) (P Qv : HCPolySupport.BlockVec d) : ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec (HCPolySupport.originCube d n) P Qv a ∂Cutoff.coefficientCutoffLaw M L = ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec (HCPolySupport.originCube d n) P Qv (Cutoff.coefficientCutoff M.nu L omega) ∂↑(Cutoff.cutoffSampleLaw M)

The annealed integral defining the defect, transported from the pushforward coefficient law to the cutoff-sample carrier on which the induction state lives. The integrand is almost-everywhere measurable by CoarseGraining's Chapter 4 local random-variable representative of the block response.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockJObservableCubeSetBlockVec_coefficientCutoff_eq_doubledResponseJ {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) (P Qv : HCPolySupport.BlockVec d) (omega : Cutoff.CutoffSample d) : HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec (HCPolySupport.originCube d n) P Qv (Cutoff.coefficientCutoff M.nu L omega) = HCPolySupport.Book.Ch02.doubledResponseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d n)) ((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn (HCPolySupport.originCube d n)) P Qv

The Chapter 4 carrier block response at a genuine cutoff realization is the Chapter 2 doubled response of the literal cutoff coefficient family on the same cube. The two triadic families differ only in their ellipticity witnesses, so they are Chapter 2 a.e. equal and the doubled response is unchanged.

The defect against the two Orlicz scales of e.new.induction.for.shom

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect_le_rpow_mul_orliczScales {d : ℕ} [NeZero d] (M : ABKModel d) {m0 L n : ℤ} {Ec : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ec) (hL : L ≤ m0) (hn : n ≤ L) {s : ℝ} (hsw : s ∈ Set.Icc (8 * M.gamma) 1) {Ev : HCPolySupport.BlockVec d} (hE : HCPolySupport.blockVecDot Ev Ev = 1) : cubeAnnealedProbeDefect M L n Ev ≤ 2 * (3 ^ (2 * s * ↑(L - n).toNat) * (orliczSecondMomentConst 2 * (↑Ec * s⁻¹ * √M.gamma) ^ 2 + orliczSecondMomentConst (1 / 2) * (s⁻¹ ^ 2 * Real.exp (-((↑Ec)⁻¹ ^ 3 * M.gamma⁻¹))) ^ 2))

The budget

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalResponseBudgetConst : ℝ

The absolute constant of the budget: twice the sum of the two class second-moment constants of orliczSecondMomentConst. It depends on nothing -- not on the dimension, the model, the parameters, or the scales.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalResponseBudgetConst_pos : 0 < principalResponseBudgetConst

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect_le_budget {d : ℕ} [NeZero d] (M : ABKModel d) {m0 L n : ℤ} {Ec : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ec) (hL : L ≤ m0) (hn : n ≤ L) (hE6 : 6 ≤ ↑Ec) (hgamE : M.gamma ≤ (↑Ec ^ 5)⁻¹) {s : ℝ} (hsw : s ∈ Set.Icc (8 * M.gamma) 1) {Ev : HCPolySupport.BlockVec d} (hE : HCPolySupport.blockVecDot Ev Ev = 1) : cubeAnnealedProbeDefect M L n Ev ≤ principalResponseBudgetConst * 3 ^ (2 * s * ↑(L - n).toNat) * (↑Ec ^ 2 * s⁻¹ ^ 2 * M.gamma)

The budget of ABK26, at a free window exponent.

At the cutoff index L, every cube scale n <= L and every window exponent s in [8 gamma, 1], the annealed defect of e.use.also.for.the.upper.bound obeys

  delta  <=  C 3^{2 s (L-n)} E^2 s^{-2} gamma ,

with C = principalResponseBudgetConst absolute. The manuscript's own display is the instance s = |log gamma|^{-1}, where s^{-2} is |log gamma|^2; see cubeAnnealedProbeDefect_le_logSq_budget.

This does not claim e.use.also.for.the.upper.bound, whose printed display is at the translated cube and at the random vector G_{-(h)_{z+cu_n}} P_z; see the module header.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect_le_budget_of_gap {d : ℕ} [NeZero d] (M : ABKModel d) {m0 L n : ℤ} {Ec : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ec) (hL : L ≤ m0) (hn : n ≤ L) (hE6 : 6 ≤ ↑Ec) (hgamE : M.gamma ≤ (↑Ec ^ 5)⁻¹) {s : ℝ} (hsw : s ∈ Set.Icc (8 * M.gamma) 1) {Ev : HCPolySupport.BlockVec d} (hE : HCPolySupport.blockVecDot Ev Ev = 1) {K : ℝ} (hgap : s * ↑(L - n).toNat ≤ K) : cubeAnnealedProbeDefect M L n Ev ≤ principalResponseBudgetConst * 3 ^ (2 * K) * (↑Ec ^ 2 * s⁻¹ ^ 2 * M.gamma)

A consumer that fixes any buffer -- the printed 16 ceil|log_3 gamma| of e.recurrence.params or a corrected larger one -- discharges hgap and reads off delta <=^{2K} E^2 s^{-2} gamma.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect_le_logSq_budget {d : ℕ} [NeZero d] (M : ABKModel d) {m0 L n : ℤ} {Ec : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ec) (hL : L ≤ m0) (hn : n ≤ L) (hE6 : 6 ≤ ↑Ec) (hgamE : M.gamma ≤ (↑Ec ^ 5)⁻¹) (hsw : |Real.log M.gamma|⁻¹ ∈ Set.Icc (8 * M.gamma) 1) {Ev : HCPolySupport.BlockVec d} (hE : HCPolySupport.blockVecDot Ev Ev = 1) {K : ℝ} (hgap : |Real.log M.gamma|⁻¹ * ↑(L - n).toNat ≤ K) : cubeAnnealedProbeDefect M L n Ev ≤ principalResponseBudgetConst * 3 ^ (2 * K) * (↑Ec ^ 2 * Real.log M.gamma ^ 2 * M.gamma)

The manuscript's own instance, t = |log gamma|^{-1} (ABK26 and the budget):

  delta  <=  C 3^{2K} E^2 |log gamma|^2 gamma .

Both are conditions on the parameters alone.