VarianceCarrierSeam

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

The seam at the genuine coefficient cutoff law

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.cutoffComparatorNormalizer {d : ℕ} (M : ABKModel d) (L : ℤ) : HCPolySupport.FullBlockMat d

The isotropic comparator normalizer 𝐁(σ_L) carried by the transported finite-corridor bound: it is literally the B bound there, so a consumer can rewrite between the two forms by rfl.

Equations

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

theorem Algsuperdiff.Section3.Provider.Homogenization.annealedInverseDiffusivity_defect_bound {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) {n m : ℤ} (hLn : L ≤ n) (hnm : n ≤ m) {s : ℝ} (hs : 0 < s) {delta1 : ℝ} (hdelta1 : delta1 ∈ Set.Ioc 0 (1 / 2)) (hmoment : ∫⁻ (omega : Cutoff.CutoffSample d), ENNReal.ofReal (Observable.cutoffHomogenizationErrorRepresentative M L L s (Annealed.sigmaBar M L) omega ^ 4) ∂↑(Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (delta1 ^ 2)) {p q : HCPolySupport.Vec d} (hpq : q = ↑(Annealed.sigmaBar M L) • p) (hqnorm : HCPolySupport.vecNormSq q = ↑(Annealed.sigmaBar M L)) : (↑(Annealed.sigmaBar M L) * (annealedSigmaStarInvScalarAtScale M L m - annealedSigmaStarInvScalarAtScale M L n)) ^ 2 ≤ 4 * delta1 ^ 2

The Step-2 downscale display in the units of the Step-3 corridor bound. Multiplying e.means.downscale.by.defect by σ_L^2 removes the σ_L^{-2} gauge, leaving the pure amplitude 4 δ₁^2, which is the scale on which the transported corridor bound C δ (δ + 3^{-d(n-L)}) is stated. The premises are exactly those of the proved display.