Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.RootClauseBWellPlacedFloor

RootClauseBWellPlacedFloor #

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

fine-scale dichotomy executed #

Nothing here imports any of them, nothing here claims an anchor, and nothing here is a frozen statement.

References #

1. Prefactor monotonicity #

source
theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBWellPlacedPrefactor_mono (d : ℕ) {Cch Cg Cg' CB Ctr CWG CWG' CWH CWH' CdM CdM' : ℝ} (hCch : 0 ≤ Cch) (hCg : 0 ≤ Cg) (hCB : 0 ≤ CB) (hCtr : 0 ≤ Ctr) (hCWG : 0 ≤ CWG) (hCWH : 0 ≤ CWH) (hCdM : 0 ≤ CdM) (hg : Cg ≤ Cg') (hwg : CWG ≤ CWG') (hwh : CWH ≤ CWH') (hdm : CdM ≤ CdM') :
rootClauseBWellPlacedPrefactor d Cch Cg CB Ctr CWG CWH CdM ≤ rootClauseBWellPlacedPrefactor d Cch Cg' CB Ctr CWG' CWH' CdM'

The well-placed prefactor is monotone in its four data slots.

source
theorem Algsuperdiff.Section4.Provider.Regularity.gateBranchCg_le_uniform (d : ℕ) [NeZero d] {Cc sigma CBraw CBu Cosc : ℝ} {np : ℤ} {a : HCPolySupport.Book.Ch03.CoeffFamily d} (hCc : 0 < Cc) (hsigma : 0 < sigma) (hCosc : 0 ≤ Cosc) (hCBraw : 0 ≤ CBraw) (hle : CBraw ≤ CBu) (hcaps : StepSevenLambdaCaps (HCPolySupport.originCube d (np + 1)) a sigma CBraw) :
Real.rpow 3 (3 * ↑d + 1 / 4) * stepSevenCaccConst Cc (HCPolySupport.originCube d np) a * (Cosc * √(256 / 63 * CBraw) + 1) ≤ rootClauseBCg d (rootClauseBCaccUniform Cc CBu) Cosc CBu

The gate branch's chain constant against its ω-free cap.

2. The floor #

source
theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_display_wellPlaced_final_floor (d : ℕ) [NeZero d] (hd : d ≠ 0) (cstar Crg : ℝ) (hcstar : 0 < cstar) (hCrg : 0 < Crg) :
∃ (Cfl : ℝ) (Citer : ℝ) (Cest : ℝ) (k : ℕ), 1 ≤ Cfl ∧ 0 ≤ Cest ∧ 11 ≤ k ∧ ∀ (Cedos : ℝ), Cfl ≤ Cedos → ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - Crg * √M.gamma → ∀ (m : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (n L : ℤ), n ≤ m → m ≤ L → RootWindowPayload M (stepOneC1 d Cedos 1 Citer k) alpha n m omega → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), (√M.nu * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m (n + 1)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) ≤ Cest * Real.rpow 3 ((1 - alpha) * (↑m - ↑n)) * ((√M.nu * Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) + √(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg + √↑(Section3.Annealed.sigmaBar M m) * Real.rpow 3 (↑m / 2) * Kh)

The boundary three-leg display centre, almost surely — the fine-scale dichotomy executed; no gate, no shell, no region hypothesis. See the module docstring.