Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.Regularity.Ported.BallCampanato

BallCampanato #

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

Campanato oscillation from the small-contrast gradient row #

source
noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRadius (d : ℕ) :
ℝ

A fixed dimension-only top radius for the sup-ball Campanato telescope.

Equations
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRadius_pos {d : ℕ} [NeZero d] :
    0 < smallContrastCampanatoRadius d
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.three_mul_dimension_mul_campanatoRadius {d : ℕ} [NeZero d] :
    3 * ↑d * smallContrastCampanatoRadius d = 1 / 4
    source
    noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoConstant (d : ℕ) :
    ℝ

    The dimension-only Poincare/ball-comparison price.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoConstant_nonneg (d : ℕ) :
      0 ≤ smallContrastCampanatoConstant d
      source
      def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.HasSmallContrastBallCampanatoBound {d : ℕ} (alpha K : ℝ) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) :
      Prop

      Campanato oscillation on every sufficiently small sup-ball.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballCampanatoBound_of_interiorGradient {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hgrad : HasInteriorSmallContrastGradientScaleBound alpha K u) :
        HasSmallContrastBallCampanatoBound alpha K u

        Poincare converts the local Morrey-gradient row into the literal Campanato mean-oscillation row.