Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.ConstantBesov

ConstantBesov #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The negative Besov seminorm of a constant vector field #

Source: ABK26, the third summand of the three-way split of ∇u = ∇w + ∇w* + ℓ_p inside e.split.besov.stuff.begin: the affine piece ℓ_p contributes the constant gradient p, whose concrete negative Besov seminorm is a pure geometric series.

Every descendant average of a constant field is that constant, so

[c]_{B^{-s}_{2,2}(Q), N} = |c| ( ∑_{j ≤ N} 3^{-2 s j} )^{1/2}
                         ≤ |c| (1 - 3^{-2s})^{-1/2}          (0 < s).

The bound is uniform in the depth N, so it also bounds the infinite-depth sSup seminorm, and it exhibits the required BddAbove witness.

The depth-level quantities of a constant field #

source
theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorDepthAverage_const {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : HCPolySupport.Vec d) (j : ℕ) :
HCPolySupport.cubeBesovNegativeVectorDepthAverage Q (fun (x : HCPolySupport.Vec d) => c) j = HCPolySupport.vecNormSq c
source
theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sqrt_vecNormSq_eq_vecNorm {d : ℕ} (c : HCPolySupport.Vec d) :
√(HCPolySupport.vecNormSq c) = HCPolySupport.Book.Ch02.vecNorm c
source
theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorDepthSeminorm_const {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (c : HCPolySupport.Vec d) (j : ℕ) :
HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s (fun (x : HCPolySupport.Vec d) => c) j = Real.rpow 3 (-s * ↑j) * HCPolySupport.Book.Ch02.vecNorm c

The geometric constant #

source
noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.constantFieldBesovConst (s : ℝ) :
ℝ

The geometric constant of the constant-field negative Besov bound.

Equations
Instances For
    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.constantFieldBesovConst_nonneg (s : ℝ) :
    0 ≤ constantFieldBesovConst s

    The finite-depth bound #

    source
    theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovNegativeVectorPartialSeminormTwo_const_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (N : ℕ) (c : HCPolySupport.Vec d) :
    (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => c) ≤ constantFieldBesovConst s * HCPolySupport.Book.Ch02.vecNorm c