Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedBesselDistributionEmbedding

Continuous distribution embedding of Sobolev fields #

The complete Bessel potential carrier maps continuously to tempered distributions. This embedding lets distributional derivatives be compared under strong Sobolev limits.

source
noncomputable def CKN.Leray.regularisedBesselToDistrCLM (s : ℝ) :
BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2 →L[ℂ] TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3

The underlying tempered distribution depends continuously and complex linearly on a Bessel-potential field.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CKN.Leray.regularisedBesselToDistrCLM_apply (s : ℝ) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) :
    (regularisedBesselToDistrCLM s) v = ↑v
    source
    noncomputable def CKN.Leray.regularisedOrderedDistributionDerivativeCLM (α : List Foundation.Parabolic.L2Vec3) :
    TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3 →L[ℂ] TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3

    The continuous linear map taking an ordered list of distributional directional derivatives.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CKN.Leray.regularisedOrderedDistributionDerivativeCLM_apply (α : List Foundation.Parabolic.L2Vec3) (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) :
      (regularisedOrderedDistributionDerivativeCLM α) D = List.foldl (fun (F : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (m : Foundation.Parabolic.L2Vec3) => LineDeriv.lineDerivOp m F) D α