Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RieszPressureDualityPotentialCompact

Compact potential tests for pressure duality #

The spatial distribution identity is transported through the space-time operator for smooth, compactly supported tests.

source
noncomputable def CKN.Leray.rieszPressureJointDirection (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) :
Foundation.Parabolic.Vec3 × ℝ → ℝ

The spatial coordinate derivative written on the space-time carrier, used by lem:riesz-duality.

Equations
Instances For
    source
    noncomputable def CKN.Leray.rieszPressureJointHessian (f : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i j : Fin 3) :
    Foundation.Parabolic.Vec3 × ℝ → ℝ

    The spatial Hessian component written on the space-time carrier, used by lem:riesz-duality.

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

      The spatial Laplacian written on the space-time carrier, used by lem:riesz-duality.

      Equations
      Instances For
        source
        theorem CKN.Leray.rieszPressure_sliceSpatialDeriv_eq_joint {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
        spatialDeriv (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) i z.1 = rieszPressureJointDirection f i z

        A spatial slice derivative agrees with the joint directional derivative, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressure_sliceMixedSecond_eq_joint {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) :
        mixedSecond (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) i j z.1 = rieszPressureJointHessian f i j z

        A spatial slice Hessian agrees with the joint spatial Hessian, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressure_sliceLaplacian_eq_joint {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (z : Foundation.Parabolic.Vec3 × ℝ) :
        spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) z.1 = rieszPressureJointLaplacian f z

        A spatial slice Laplacian agrees with the joint spatial Laplacian, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressureJointDirection_contDiff {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) :
        ContDiff ℝ (↑⊤) (rieszPressureJointDirection f i)

        Spatial directional derivatives preserve smoothness, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressureJointHessian_contDiff {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) :
        ContDiff ℝ (↑⊤) (rieszPressureJointHessian f i j)

        Spatial Hessian components preserve smoothness, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressureJointHessian_hasCompactSupport {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hfc : HasCompactSupport f) (i j : Fin 3) :
        HasCompactSupport (rieszPressureJointHessian f i j)

        Spatial Hessians of compactly supported functions have compact support, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressureJointLaplacian_hasCompactSupport {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hfc : HasCompactSupport f) :
        HasCompactSupport (rieszPressureJointLaplacian f)

        Spatial Laplacians of compactly supported functions have compact support, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressureJointLaplacian_contDiff {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) :
        ContDiff ℝ (↑⊤) (rieszPressureJointLaplacian f)

        The spatial Laplacian preserves smoothness, used by lem:riesz-duality.

        source
        theorem CKN.Leray.rieszPressureComponentCompactClass_laplacian_pairing (r : ℝ) (hr : 1 < r) (q : ℝ) (hHolder : r.HolderConjugate q) (i j : Fin 3) {F ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) :
        ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑(rieszPressureComponentCompactClass r hr i j hF hFc) z * rieszPressureJointLaplacian ψ z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * rieszPressureJointHessian ψ i j z

        A compact smooth potential test satisfies the component distributional identity, used by lem:riesz-duality.