BfaLocalLane #

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

The local-descendant lane for `p.bfA.multiscalebound` #

ABK26 applies p.bfA.multiscalebound separately on every translated cube R = z + cu_n before invoking e.maxy.bound over the finite grid (especially). Consequently the random separation scale at R is not the root observable hsep M m E b omega: it is the origin observable at scale R.scale, read at the translated sample

hsep M R.scale E b
  (Cutoff.translateCutoffSample (triadicCubeShift R) omega).

This file records exactly that local lane. Stationarity transports the proved local Gamma_(bfaTau sigma gam b) bound from BfaPerCube without changing its amplitude. The subsequent finite-grid maximum is deliberately priced by the existing BlockPayload.isBigOWith_gammaSigma_blockGridSup; thus the e.maxy.bound cost gridBlockAmp ... k remains visible and is not replaced by an unsupported same-sample domination by the root hsep.

Scope of the payoff interface #

ConclusionRoot.abs_blockVecDot_coarseBlockMatrix_originCube_le_payload_ae is almost-everywhere and retains, as antecedents, nonemptiness of hsepSet, the wave envelope, and the potential/solenoidal competitor clauses. The final theorem here therefore only converts an already supplied a.e. conditional local Step-3 payoff into the constant-plus-lane form, preserving an explicit gate unchanged on both sides. It does not assert that the gate or payoff is satisfied, and it does not turn an a.e. conclusion into a pointwise one.

A producer from ConclusionRoot still requires the analytic competitor clauses, a uniform envelope, the quadratic-form-to-operator-norm bridge, and a simultaneous a.e. argument over the loadings (the cutoff indices are countable, but the unit sphere is not). None of those obligations is moved into a hypothesis of an unconditional theorem here.

Source #

Source: ABK26, p.bfA.multiscalebound; the translated-grid maximum in the proof of p.cg.ellipticity.bounds.
No theorem in this file closes p.bfA.multiscalebound.

The local lane and its deterministic hygiene #

source

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaLocalLane {d : ℕ} (M : ABKModel d) (R : HCPolySupport.TriadicCube d) (E b gam Cpre eps : ℝ) (omega : Cutoff.CutoffSample d) :

ℝ

The p.bfA.multiscalebound random lane at a triadic cube R: the origin lane at scale R.scale, evaluated on the sample translated by the base point of R.

Equations

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

Instances For

source

theorem Algsuperdiff.Section3.Provider.Multiscale.bfaLocalLane_nonneg {d : ℕ} (M : ABKModel d) (R : HCPolySupport.TriadicCube d) {E b gam Cpre eps : ℝ} (hCpre : 0 ≤ Cpre) (heps : 0 ≤ eps) (omega : Cutoff.CutoffSample d) :

0 ≤ bfaLocalLane M R E b gam Cpre eps omega

source

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_bfaLocalLane {d : ℕ} (M : ABKModel d) (R : HCPolySupport.TriadicCube d) (E b gam Cpre eps : ℝ) :

Measurable (bfaLocalLane M R E b gam Cpre eps)

Stationarity transport of the proved local `BfaPerCube` bound #

source

theorem Algsuperdiff.Section3.Provider.Multiscale.inductionState_restrict {d : ℕ} {M : ABKModel d} {m0 m1 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hm : m1 ≤ m0) (hS : Frozen.Section3.inductionState M m0 E) :

Frozen.Section3.inductionState M m1 E

Restrict the induction state to an earlier terminal scale. This is only the monotonicity already present in the frozen definition's two forall m <= m0 clauses.

source