Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.FourierMollifierContraction

The L² contraction for the general regularizing profile #

Probability averaging by regMollifierKernel does not increase the spatial L² norm. This is the contraction estimate in lem:reg-mollifier-bounds.

source
def CKN.Leray.contractionScalarActionLinear :
ℝ →ₗ[ℝ] Foundation.Parabolic.L2Vec3 →ₗ[ℝ] Foundation.Parabolic.L2Vec3

The bilinear scalar multiplication map used in the mollifier contraction estimate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CKN.Leray.contractionScalarAction :
    ℝ →L[ℝ] Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

    The continuous scalar multiplication map used to bound the mollifier action.

    Equations
    Instances For
      source
      noncomputable def CKN.Leray.scalarProfileOnVec3 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) :
      Foundation.Parabolic.Vec3 → ℝ

      The dilated mollifier kernel expressed on the native coordinate space.

      Equations
      Instances For
        source
        noncomputable def CKN.Leray.scalarNormOnVec3 (f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) :
        Foundation.Parabolic.Vec3 → ℝ

        The pointwise norm of a Hilbert-valued map expressed on coordinate vectors.

        Equations
        Instances For
          source
          noncomputable def CKN.Leray.scalarConvolutionMajor (f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) :
          Foundation.Parabolic.L2Vec3 → ℝ

          The convolution of the mollifier kernel with the pointwise norm of a vector field.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem CKN.Leray.regMollifyVector_eLpNorm_two_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
            MeasureTheory.eLpNorm (regMollifyVector ρ ε hε f) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume

            Convolution by a normalized nonnegative regularizing kernel is a contraction on spatial L², as required by lem:reg-mollifier-bounds.