RootClauseBCloseChain #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
Algsuperdiff.Section4.Provider.Regularity.rootClauseB_display_interior_freeCoarse
(d : ℕ)
[NeZero d]
:
∃ (Cch : ℝ) (Cc : ℝ),
0 < Cch ∧ 0 < Cc ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }),
Frozen.Section3.inductionState M m0 Ecap →
M.gamma < 1 / 2 →
∀ (L : ℤ) {alpha : ℝ} {n m kc n' : ℤ} {z : HCPolySupport.Vec d} (omega : Section3.Cutoff.CutoffSample d)
(uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
{gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {Khol Kd CB CBc Cdel Cosc CdM C1 delta Cest : ℝ}
{B : ℕ},
z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) →
m ≤ m0 →
n' ≤ m - 1 →
n + 1 ≤ n' - 2 →
n ≤ m →
n' ≤ kc →
kc ≤ m - 1 →
m - (kc + 1) ≤ ↑B + 1 →
Support.IsDirichletSolutionOn
(Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField
(HCPolySupport.originCube d m) uglob hdat gsrc →
MeasureTheory.MemLp gsrc 2
(Support.normalizedVolumeMeasureOn
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) →
MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2
(Support.normalizedGagliardoMeasureOn
(HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) →
0 ≤ Khol →
0 ≤ Kd →
0 ≤ CB →
0 ≤ CBc →
0 ≤ Cdel →
0 ≤ Cosc →
0 ≤ CdM →
2 * ↑d + 2 ≤ C1 →
0 ≤ alpha →
alpha ≤ 1 →
delta ≤ C1⁻¹ * (1 - alpha) →
n' - n ≤ ↑B + 6 →
↑B ≤ delta * (↑(m - n).toNat + 1) →
StepSevenLambdaCaps (HCPolySupport.originCube d (kc + 1))
(Support.fluxCorrectedCoeffFamily M L (kc + 1)
(HCPolySupport.originCube d (kc + 1))
(Section3.Cutoff.translateCutoffSample z omega))
(↑(Section3.Annealed.sigmaBar M (kc + 1))) CB →
StepSevenLambdaCaps
(HCPolySupport.originCube d (n' + 1))
(Support.fluxCorrectedCoeffFamily M L (n' + 1)
(HCPolySupport.originCube d (n' + 1))
(Section3.Cutoff.translateCutoffSample z omega))
(↑(Section3.Annealed.sigmaBar M (n' + 1))) CBc →
(HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo
(HCPolySupport.originCube d kc) stepSevenCgS
fun (x : HCPolySupport.Vec d) =>
-gsrc (x + z)) ≤ Kd * edFinalDataOscG Khol m →
(stepSevenCaccDataM (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L (n' + 1)
(HCPolySupport.originCube d (n' + 1))
(Section3.Cutoff.translateCutoffSample z
omega))
fun (x : HCPolySupport.Vec d) =>
-gsrc (x + z)) ≤ CdM * (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * edFinalDataOscG Khol m) →
(3 ^ (-n') * Support.normalizedL2On
(ExcessDecay.truncatedWindow z m n')
fun (x : HCPolySupport.Vec d) =>
uglob.toFun x - HCPolySupport.volumeAverage
(ExcessDecay.truncatedWindow z m n')
uglob.toFun) ≤ Cosc * Real.rpow 3
(1 / 2 * stepSixExponent alpha n m) * (3 ^ (-kc) * Support.normalizedL2On
(ExcessDecay.truncatedWindow z m kc)
fun (x : HCPolySupport.Vec d) =>
uglob.toFun x - HCPolySupport.volumeAverage
(ExcessDecay.truncatedWindow z m
kc)
uglob.toFun) + Cosc * Real.rpow 3
(1 / 2 * stepSixExponent alpha n m) * (edFinalDataG M Cdel
(Khol * stepFourGagliardoConst d stepOneS)
m + 0) →
rootClauseBPrefactor d Cch
(stepSevenCaccConst Cc
(HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L
(n' + 1)
(HCPolySupport.originCube d (n' + 1))
(Section3.Cutoff.translateCutoffSample
z omega)))
Cosc CBc CB (rootClauseBTopCtr d Kd)
(edFinalDataOscW M Cdel * stepFourGagliardoConst d stepOneS)
CdM ≤ Cest →
(√M.nu * Support.normalizedL2On
(ExcessDecay.truncatedWindow z m
(n + 1))
fun (y : HCPolySupport.Vec d) =>
√(HCPolySupport.vecNormSq
(uglob.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
(uglob.grad y))) + ⋯)
The interior clause-(B) display with k = m-1 replaced by a
free k_c ≤ m-1; the coarse clause-(B) record accordingly sits at □_{k_c+1}
against its own σ_{k_c+1}, which is what lets the record come from the
Step-3 good event instead of the uncontrolled top scale.