Documentation

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

SchauderRepresentative #

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

Common representative for the unified Schauder chain #

source
noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastSchauderRepresentative {d : ℕ} (u : HCPolySupport.H1Function (smallContrastUnitBall d)) (x : HCPolySupport.Vec d) :
ℝ

A globally defined representative: the Campanato representative on the interior half-ball and the original Sobolev representative elsewhere.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastSchauderRepresentative_of_mem {d : ℕ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) :
    smallContrastSchauderRepresentative u x = smallContrastCampanatoRepresentative u.toFun x
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastSchauderRepresentative_ae_eq {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hcamp : HasSmallContrastBallCampanatoBound alpha K u) :
    smallContrastSchauderRepresentative u =ᵐ[MeasureTheory.volume.restrict (smallContrastUnitBall d)] u.toFun
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.continuousOn_smallContrastSchauderRepresentative {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hK : 0 ≤ K) (hcamp : HasSmallContrastBallCampanatoBound alpha K u) :
    ContinuousOn (smallContrastSchauderRepresentative u) (smallContrastBall d (1 / 2))