Documentation

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

CampanatoHolder #

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

Campanato-to-Hölder conversion on [1/2,1) #

The exponent restriction bounds the order-alpha⁻¹ Campanato constant by a numerical constant.

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

The common constant in the local small-contrast Hölder estimate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastLocalHolderConstant_nonneg (d : ℕ) :
    0 ≤ smallContrastLocalHolderConstant d
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.local_holder_smallContrastCampanatoRepresentative {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) {x y : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) (hy : y ∈ smallContrastBall d (1 / 2)) (hxy : ‖x - y‖ ≤ smallContrastCampanatoRadius d) :
    |smallContrastCampanatoRepresentative u.toFun x - smallContrastCampanatoRepresentative u.toFun y| ≤ smallContrastLocalHolderConstant d * K * ‖x - y‖ ^ alpha

    The representative is Hölder for separations at most the fixed telescope radius.

    Finite convex chaining #

    source
    def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastHolderChainLength (d : ℕ) :
    ℕ

    The number of links used to compare points in the small-contrast Hölder estimate.

    Equations
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastHolderChainLength_pos (d : ℕ) :
      0 < smallContrastHolderChainLength d
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.holder_on_halfBall_of_local {d : ℕ} [NeZero d] {alpha L : ℝ} {G : HCPolySupport.Vec d → ℝ} (halpha0 : 0 ≤ alpha) (hL : 0 ≤ L) (hloc : ∀ x ∈ smallContrastBall d (1 / 2), ∀ y ∈ smallContrastBall d (1 / 2), ‖x - y‖ ≤ smallContrastCampanatoRadius d → |G x - G y| ≤ L * ‖x - y‖ ^ alpha) (x : HCPolySupport.Vec d) :
      x ∈ smallContrastBall d (1 / 2) → ∀ y ∈ smallContrastBall d (1 / 2), |G x - G y| ≤ ↑(smallContrastHolderChainLength d) * L * ‖x - y‖ ^ alpha

      A local scalar Hölder estimate on B_{1/2} globalizes with the fixed dimension-only chain length 12d+1.

      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.holder_smallContrastCampanatoRepresentative {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) (x : HCPolySupport.Vec d) :
      x ∈ smallContrastBall d (1 / 2) → ∀ y ∈ smallContrastBall d (1 / 2), |smallContrastCampanatoRepresentative u.toFun x - smallContrastCampanatoRepresentative u.toFun y| ≤ ↑(smallContrastHolderChainLength d) * smallContrastLocalHolderConstant d * K * ‖x - y‖ ^ alpha

      Global sup-metric Hölder bound of the Campanato representative.

      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.continuousOn_of_supHolderBoundOn_Ico_half {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha L : ℝ} {G : HCPolySupport.Vec d → ℝ} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hL : 0 ≤ L) (hholder : ∀ x ∈ W, ∀ y ∈ W, |G x - G y| ≤ L * ‖x - y‖ ^ alpha) :
      ContinuousOn G W

      A positive sup-metric Hölder modulus gives continuity on its window. On the range alpha >= 1/2, a squared epsilon radius is a uniform modulus, so no exponent-dependent constant is introduced.

      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.continuousOn_smallContrastCampanatoRepresentative {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 (smallContrastCampanatoRepresentative u.toFun) (smallContrastBall d (1 / 2))

      Continuity of the canonical Campanato representative on the interior half-ball.