Documentation

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

ZerothOrderGradient #

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

Gradient Morrey rows with a bounded scalar source #

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

The additional dimension coefficient paid by the scalar source.

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

    A dimension-only coefficient controlling all three data rows.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothGradientConstant_nonneg (d : ℕ) :
      0 ≤ smallContrastZerothGradientConstant d
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.interiorGradientScaleBound_of_smallContrast_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) :
      HasInteriorSmallContrastGradientScaleBound alpha (smallContrastZerothGradientConstant d * smallContrastZerothOrderDataSize d alpha u f g) u

      Uniform interior Morrey-gradient bound with a bounded scalar source.

      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.gradientScaleBound_of_smallContrast_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) :
      HasSmallContrastGradientScaleBound alpha (smallContrastZerothGradientConstant d * smallContrastZerothOrderDataSize d alpha u f g) u

      Concentric gradient row for the zeroth-order equation.