RootPayloadDataB #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The dataB constant K_d = C_bg(d)·C_{§4.4}(d,1/4): the Besov--Gagliardo
bridge constant times the Hölder--Gagliardo constant at the §4.4 exponent. A
pure dimensional constant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section4.Provider.Regularity.besovTranslated_neg_le_holder_gate
{d : ℕ}
[NeZero d]
{m j : ℤ}
{z : HCPolySupport.Vec d}
{gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d}
{Khol : ℝ}
(hgate :
(fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j) ⊆
HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hKhol : 0 ≤ Khol)
(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))))
:
(HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d j) stepSevenCgS
fun (y : HCPolySupport.Vec d) => -gsrc (y + z)) ≤ rootClauseBDataBConst d * (Real.rpow 3 (↑j / 2) * Khol)
The translated Besov datum on every cube contained in the ambient domain.
theorem
Algsuperdiff.Section4.Provider.Regularity.besovTranslated_neg_le_holder
{d : ℕ}
[NeZero d]
{m j : ℤ}
{z : HCPolySupport.Vec d}
{gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d}
{Khol : ℝ}
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)))
(hj : j ≤ m - 1)
(hKhol : 0 ≤ Khol)
(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))))
:
(HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d j) stepSevenCgS
fun (y : HCPolySupport.Vec d) => -gsrc (y + z)) ≤ rootClauseBDataBConst d * (Real.rpow 3 (↑j / 2) * Khol)
The translated Besov datum at ANY interior scale.
For every interior centre z ∈ □_{m-1} and every scale j ≤ m-1, the
translated forcing's B^{1/4}_{2,∞}(□_j) seminorm is dominated by the root's
own Hölder-1/2 datum:
[ -𝐠(· + z) ]_{B^{1/4}_{2,∞}(□_j)} ≤ K_d(d) · 3^{j/2} K_g .
This is the shared engine of the payload's dataB field (at j = m-1) and of
its dataM field (at j = n').