Perturbation

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

Constants and unit-cube normalizations for the perturbation Besov bound

Source: ABK26, the second inequality of e.sensitivity.basic.split1:

‖ h ‖_{B^{3/8}_{2,2}(□₀)}  ≤  C ( | (h)_{□₀} | + ‖ ∇h ‖_{L^∞(□₀)} ) .

What remains here is the arithmetic surface that the surviving Section 2.4 cone consumes: the constant besovPerturbConst s, which is the ℓ² geometric sum ∑ 3^{2(s-1)j} (convergent because s < 1), and the two unit-cube normalizations of the cube scale factor and the Besov scale weight.

The ℓ² depth constant

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovPerturbConst (s : ℝ) : ℝ

The constant of the perturbation bound: the ℓ² geometric sum ∑ 3^{2(s-1)j}.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovPerturbConst s = √(1 - Real.rpow 3 (2 * (s - 1)))⁻¹

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.besovPerturbConst_pos {s : ℝ} (hs : s < 1) : 0 < besovPerturbConst s

The unit-cube statement

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeScaleFactor_originCube_zero (d : ℕ) : HCPolySupport.cubeScaleFactor (HCPolySupport.originCube d 0) = 1

@[simp]

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.cubeBesovScaleWeight_originCube_zero (d : ℕ) (s : ℝ) : HCPolySupport.cubeBesovScaleWeight s (HCPolySupport.originCube d 0) = 1