RootClauseBFloorRecut #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. C₁ is monotone in C_edos #
theorem
Algsuperdiff.Section4.Provider.Regularity.le_stepOneC1_of_le_cedos
(d : ℕ)
{F Cedos : ℝ}
(h1 : 1 ≤ Cedos)
(hF : F ≤ Cedos)
(Citer : ℝ)
(k : ℕ)
:
Every floor is cleared by a large enough C_edos.
C₁ ≥ stepOne C_edos 1 k = 16 C_edos² 3^{k/2} ≥ C_edos for C_edos ≥ 1. This
is the shape a boundary producer needs: it may answer with a floor on C_edos
alone and never mention C₁.
2. hosc with C_edos free above the lane's own floor #
theorem
Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBOsc_floor
(d : ℕ)
[NeZero d]
(hd : d ≠ 0)
:
∃ (C : ℝ) (Cann : ℝ) (Citer : ℝ) (Cosc : ℝ) (Cdel : ℝ) (k : ℕ),
0 < C ∧ 0 < Cann ∧ 0 ≤ Cosc ∧ 0 ≤ Cdel ∧ 11 ≤ k ∧ ∀ (Cedos : ℝ),
rootClauseBFundCedos d C Cann k ≤ Cedos →
∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }),
Frozen.Section3.inductionState M m0 Ecap →
M.gamma < 1 / 2 →
M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 →
M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 →
M.gamma ≤ 1 / 256 →
M.gamma * |Real.log M.gamma| ^ 2 ≤ (stepOneS / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (C⁻¹ * stepOneS ^ 4) →
∀ (alpha : ℝ),
0 < alpha →
alpha < 1 →
M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos 1 Citer k) alpha) →
∀ m ≤ m0,
∀ᵐ (omega :
Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L n : ℤ) (v : Fin d → ℤ),
m ≤ L →
14 ≤ m - n →
v ∈ Support.latticeCubeSet d n m →
Support.triadicLatticePoint n v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) →
RootWindowPayload M (stepOneC1 d Cedos 1 Citer k) alpha n m omega →
∀
(uglob hdat :
HCPolySupport.H1Function
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d)
(Khol Kh : ℝ),
0 ≤ Khol →
0 ≤ Kh →
Support.IsDirichletSolutionOn
(Section3.Cutoff.coefficientCutoff M.nu L
omega).toCoeffField
(HCPolySupport.originCube d m) uglob hdat gsrc →
Support.HolderSeminormBoundOn
(HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))
(1 / 2) Khol gsrc →
Support.HolderSeminormBoundOn
(HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))
(1 / 2) Kh hdat.grad →
∀ (n' kc : ℤ),
n ≤ n' →
n' ≤ kc →
kc ≤ m →
(3 ^ (-n') * Support.normalizedL2On
(ExcessDecay.truncatedWindow
(Support.triadicLatticePoint n v) m
n')
fun (y : HCPolySupport.Vec d) =>
uglob.toFun y - HCPolySupport.volumeAverage
(ExcessDecay.truncatedWindow
(Support.triadicLatticePoint n v)
m n')
uglob.toFun) ≤ ⋯ * ⋯ + ⋯ * (edFinalDataG M Cdel
(Khol * stepFourGagliardoConst d stepOneS)
m + 0)
's exists_rootClauseBOsc, parametric above its C_edos floor.
Character for character RootClauseBFinalOsc.exists_rootClauseBOsc, with the
pinned letter rootClauseBFundCedos d k replaced by a C_edos above it. The
only proof change: the Step-6 funding gate is obtained from the pinned floor
and stepOneC1_mono_cedos.
3. Clause (B) with C_edos free above the lane's own floor #
theorem
Algsuperdiff.Section4.Provider.Regularity.rootClauseB_display_offGrid_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 →
∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m),
offGridCentre n x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) →
(√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)
's clause-(B) endpoint, parametric above its C_edos floor.