Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.Regularity.UnitCubeDirichletPoincare

UnitCubeDirichletPoincare #

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

An explicit Dirichlet Poincaré constant on the unit cube #

The upstream general-domain theorem selects an unspecified constant. On the unit axis cube, integration by parts in one coordinate gives the closed constant 1.

source
def Algsuperdiff.StochasticProcess.Common.Regularity.unitCubeDirichletPoincareExplicit (_d : ℕ) :
ℝ

Closed Dirichlet Poincaré constant used by the small-contrast chain.

Equations
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.unitCubeDirichletPoincareExplicit_nonneg (d : ℕ) :
    0 ≤ unitCubeDirichletPoincareExplicit d
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.unitCubeDirichletPoincareExplicit_bound {d : ℕ} [NeZero d] (w : HCPolySupport.H10Function (HCPolySupport.axisCube 0 1)) :
    ‖w.toScalarL2‖ ≤ unitCubeDirichletPoincareExplicit d * w.gradientCoordL2NormSum

    The unit axis cube has the explicit zero-trace Poincaré constant 1.

    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.scaled_dirichlet_poincare_explicit_norm {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (w : HCPolySupport.H10Function (HCPolySupport.axisCube z L)) :
    ‖w.toScalarL2‖ ≤ unitCubeDirichletPoincareExplicit d * L * w.gradientCoordL2NormSum

    Scaled zero-trace Poincaré inequality on an axis cube, with explicit constant 1.

    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.scaled_dirichlet_poincare_explicit {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) (w : HCPolySupport.H10Function (HCPolySupport.axisCube z L)) :
    (MeasureTheory.eLpNorm w.toFun 2 (HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L))).toReal ≤ unitCubeDirichletPoincareExplicit d * L * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => w.grad x i) 2 (HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L))).toReal

    Scaled zero-trace Poincaré inequality in eLpNorm form, with explicit constant 1.