Documentation

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

ZerothOrderCarrier #

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

Zeroth-order data for the small-contrast equation #

source
def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsMatrixDivFormWeakSolutionZerothOrderOn {d : ℕ} (a : HCPolySupport.CoeffField d) (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function W) (g : HCPolySupport.Vec d → ℝ) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) :
Prop

Weak -div(a grad u) = g + div f on a window.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.scalarLInfSizeOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (g : HCPolySupport.Vec d → ℝ) :
    ℝ

    Essential-supremum size of a scalar datum.

    Equations
    Instances For
      source
      def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.MemScalarLInfOn {d : ℕ} (W : Set (HCPolySupport.Vec d)) (g : HCPolySupport.Vec d → ℝ) :
      Prop

      Scalar L^infinity membership on a window.

      Equations
      Instances For
        source
        noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothOrderDataSize (d : ℕ) (alpha : ℝ) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (g : HCPolySupport.Vec d → ℝ) :
        ℝ

        Data size for the equation with a bounded zeroth-order source.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothOrderDataSize_nonneg {d : ℕ} {alpha : ℝ} (halpha : alpha < 1) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (g : HCPolySupport.Vec d → ℝ) :
          0 ≤ smallContrastZerothOrderDataSize d alpha u f g