RootPayloadDataM #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
noncomputable def
Algsuperdiff.Section4.Provider.Regularity.rootClauseBDataMConst
(d : ℕ)
(CBc : ℝ)
:
The dataM constant C_dM = √(4·F·(64/7)·C_Bc)·K_d(d).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section4.Provider.Regularity.rootClauseB_dataM_of_besov_bound
{d : ℕ}
[NeZero d]
{M : Section3.ABKModel d}
{m0 : ℤ}
{Ecap : { E : ℝ // 1 ≤ E }}
(hS : Frozen.Section3.inductionState M m0 Ecap)
(hgamma : M.gamma < 1 / 2)
{m n' : ℤ}
{a : HCPolySupport.Book.Ch03.CoeffFamily d}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
{Khol CBc : ℝ}
(hmm0 : m ≤ m0)
(hn' : n' ≤ m - 1)
(hKhol : 0 ≤ Khol)
(hCBc : 0 ≤ CBc)
(hcaps : StepSevenLambdaCaps (HCPolySupport.originCube d (n' + 1)) a (↑(Section3.Annealed.sigmaBar M (n' + 1))) CBc)
(hBes :
HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d n') stepOneS f ≤ rootClauseBDataBConst d * (Real.rpow 3 (↑n' / 2) * Khol))
(hforce : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d n') stepOneS f)
:
stepSevenCaccDataM (HCPolySupport.originCube d n') a f ≤ rootClauseBDataMConst d CBc * (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * edFinalDataOscG Khol m)
A Besov bound and forcing regularity supply the common Caccioppoli data estimate.
theorem
Algsuperdiff.Section4.Provider.Regularity.rootClauseB_dataM
{d : ℕ}
[NeZero d]
{M : Section3.ABKModel d}
{m0 : ℤ}
{Ecap : { E : ℝ // 1 ≤ E }}
(hS : Frozen.Section3.inductionState M m0 Ecap)
(hgamma : M.gamma < 1 / 2)
{m n' : ℤ}
{z : HCPolySupport.Vec d}
{a : HCPolySupport.Book.Ch03.CoeffFamily d}
{gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d}
{Khol CBc : ℝ}
(hmm0 : m ≤ m0)
(hn' : n' ≤ m - 1)
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)))
(hKhol : 0 ≤ Khol)
(hCBc : 0 ≤ CBc)
(hgHol : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Khol gsrc)
(hgL2 :
MeasureTheory.MemLp gsrc 2
(Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))))
(hgW :
MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2
(Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))))
(hcaps : StepSevenLambdaCaps (HCPolySupport.originCube d (n' + 1)) a (↑(Section3.Annealed.sigmaBar M (n' + 1))) CBc)
:
(stepSevenCaccDataM (HCPolySupport.originCube d n') a fun (y : HCPolySupport.Vec d) => -gsrc (y + z)) ≤ rootClauseBDataMConst d CBc * (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * edFinalDataOscG Khol m)
The clause-(B) dataM leg, produced: the Caccioppoli's own data leg
against the printed K_g-leg.