RootClauseBBoundaryOscFloor #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
Algsuperdiff.Section4.Provider.Regularity.exists_rootClauseBOsc_boundary_floor
(d : ℕ)
[NeZero d]
(hd : d ≠ 0)
:
∃ (C : ℝ) (Ccap : ℝ) (Cann : ℝ) (Cb : ℝ) (Cfl : ℝ) (Citer : ℝ) (Cosc : ℝ) (k : ℕ),
0 < C ∧ 0 < Ccap ∧ 0 < Cann ∧ 0 ≤ Cb ∧ 1 ≤ Cfl ∧ 0 ≤ Cosc ∧ 10 ≤ k ∧ ∀ (Cedos : ℝ),
Cfl ≤ 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 ≤ Ccap⁻¹ * Section3.Disorder.cstar M ^ 10 →
M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 →
M.gamma ≤ 1 / 256 →
∀ (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 + 1)) 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 →
RootWindowPayload M (stepOneC1 d Cedos 1 Citer (k + 1)) 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 →
(∀
y ∈
HCPolySupport.openCubeSet
(HCPolySupport.originCube d m),
‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) →
Support.HasGradientOn
(HCPolySupport.openCubeSet
(HCPolySupport.originCube d m))
hdat.toFun hdat.grad →
∀ (n' kc : ℤ), n ≤ n' → ⋯
e.oscillation.Holder.bound on the boundary branch, at the root's frame, on
ONE null set, with C_edos free above this lane's own floor.
The boundary Step-6 endpoint with its entire parameter prefix discharged, its scale pair inside the a.e. block, and its windows written in the carrier the clause-(B) payload reads. No interiority guard.