Documentation

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

ZerothOrderSchauder #

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

Interior Schauder estimate with a bounded scalar source #

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

Dimension coefficient for the Hölder row with scalar forcing.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothHolderOutputConstant_nonneg (d : ℕ) :
    0 ≤ smallContrastZerothHolderOutputConstant d
    source
    noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothSchauderConstant (d : ℕ) :
    ℝ

    The single dimension coefficient in the zeroth-order estimate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothSchauderConstant_nonneg (d : ℕ) :
      0 ≤ smallContrastZerothSchauderConstant d
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastSchauder_zerothOrder {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} {g : HCPolySupport.Vec d → ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} {delta alpha : ℝ} (hd : 2 ≤ d) (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ smallContrastThreshold d alpha) (hmeas : Measurable a) (ha : CoefficientIdentityDistanceLE (smallContrastUnitBall d) a delta) (hu : IsMatrixDivFormWeakSolutionZerothOrderOn a (smallContrastUnitBall d) u g f) (hg : MemScalarLInfOn (smallContrastUnitBall d) g) (hf : MemVectorLpOn (smallContrastUnitBall d) (schauderSourceExponent d alpha) f) :
      SmallContrastSchauderConclusion alpha (smallContrastZerothSchauderConstant d * smallContrastZerothOrderDataSize d alpha u f g) u

      Full representative and gradient conclusion for a bounded scalar source.

      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.schauder_interior_holder_zerothOrder {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} {g : HCPolySupport.Vec d → ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} {delta alpha : ℝ} (hd : 2 ≤ d) (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ smallContrastThreshold d alpha) (hmeas : Measurable a) (ha : CoefficientIdentityDistanceLE (smallContrastUnitBall d) a delta) (hu : IsMatrixDivFormWeakSolutionZerothOrderOn a (smallContrastUnitBall d) u g f) (hg : MemScalarLInfOn (smallContrastUnitBall d) g) (hf : MemVectorLpOn (smallContrastUnitBall d) (schauderSourceExponent d alpha) f) :
      SmallContrastSchauderConclusion alpha (smallContrastZerothSchauderConstant d * smallContrastZerothOrderDataSize d alpha u f g) u

      Interior Schauder estimate with g in L^infinity; the scalar term has no factor (1-alpha)⁻¹.