Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.ContinuousCoeffResolvent

ContinuousCoeffResolvent #

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

Ellipticity bounds for a continuous coefficient #

A coefficient with scalar symmetric part nu * I and continuous skew part is elliptic on every compact set, with an upper constant that compactness supplies. The closed axis cube and the closure of a bounded domain are compact, so on those two carriers the ellipticity certificate is a consequence of the continuity hypothesis and need not be assumed.

This file names the compact, cube, and bounded-domain ellipticity certificates supplied by continuity.

1. Two compact carriers #

source
theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isCompact_memAxisCubeClosure {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) :
IsCompact {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x}

The coordinatewise closure of an axis cube is compact.

source
theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isCompact_closure_of_isBoundedDomain {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsBoundedDomain U) :
IsCompact (closure U)

The closure of a bounded domain is compact.

2. The ellipticity witness supplied by continuity #

source
noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.compactEllipticUpper {d : ℕ} {W K : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (hK : IsCompact K) (hWK : W ⊆ K) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) K) :
ℝ

The upper ellipticity constant of a coefficient with scalar symmetric part and continuous skew part on a compact set.

Equations
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticFieldOn_compactEllipticUpper {d : ℕ} {W K : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (hK : IsCompact K) (hWK : W ⊆ K) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) K) :
    HCPolySupport.IsEllipticFieldOn nu (compactEllipticUpper hW hK hWK hnu hsymm hcont) W a

    The ellipticity certificate that the constant names.

    source
    noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.axisCubeEllipticUpper {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x}) :
    ℝ

    The upper ellipticity constant on an axis cube.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticFieldOn_axisCubeEllipticUpper {d : ℕ} (z : HCPolySupport.Vec d) (L : ℝ) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x}) :
      HCPolySupport.IsEllipticFieldOn nu (axisCubeEllipticUpper z L hnu hsymm hcont) (HCPolySupport.axisCube z L) a

      An axis-cube ellipticity certificate from continuity alone.

      source
      noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.domainEllipticUpper {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) (closure U)) :
      ℝ

      The upper ellipticity constant on a bounded domain.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isEllipticFieldOn_domainEllipticUpper {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) (closure U)) :
        HCPolySupport.IsEllipticFieldOn nu (domainEllipticUpper hU hnu hsymm hcont) U a

        A bounded-domain ellipticity certificate from continuity alone.