Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Euclidean.RieszSecondL2Input

Riesz Second L2 Input #

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

source
@[reducible, inline]
abbrev CKN.Foundation.Euclidean.testFunction :
Type

Smooth compactly supported real test functions on the whole spatial domain.

Equations
Instances For
    source
    noncomputable def CKN.Foundation.Euclidean.testSource :
    testFunction →ₗ[ℝ] ↥rieszSecondL2

    Linear inclusion of compactly supported smooth test functions into L².

    Equations
    Instances For
      source
      theorem CKN.Foundation.Euclidean.test_hessian_mem (i j : Fin 3) (f : testFunction) :
      MeasureTheory.MemLp (mixedSecond (pressureNewtonianPotential ⇑f) i j) 2 MeasureTheory.volume
      source
      noncomputable def CKN.Foundation.Euclidean.testHessian (i j : Fin 3) :
      testFunction →ₗ[ℝ] ↥rieszSecondL2

      L² class of a second derivative of the Newtonian potential of a test function.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def CKN.Foundation.Euclidean.testHessianExtension (i j : Fin 3) :
        ↥rieszSecondL2 →L[ℝ] ↥rieszSecondL2

        Continuous L² extension of the test-function Hessian operator.

        Equations
        Instances For
          source
          noncomputable def CKN.Foundation.Euclidean.rieszSecondSmoothMap (i j : Fin 3) :
          SchwartzMap Parabolic.Vec3 ℝ →L[ℝ] ↥rieszSecondL2

          Second-Riesz map on Schwartz functions obtained from the continuous L² extension.

          Equations
          Instances For
            source
            theorem CKN.Foundation.Euclidean.rieszSecondSmoothMap_bound (i j : Fin 3) (φ : SchwartzMap Parabolic.Vec3 ℝ) :
            ‖(rieszSecondSmoothMap i j) φ‖ ≤ ‖(SchwartzMap.toLpCLM ℝ ℝ 2 MeasureTheory.volume) φ‖
            source
            noncomputable def CKN.Foundation.Euclidean.rieszSecondL2Input (i j : Fin 3) :
            RieszSecondL2Input i j

            The indexed smooth Hessian map obtained from the global endpoint estimate.

            Equations
            Instances For
              source
              theorem CKN.Foundation.Euclidean.rieszSecondL2Input_extension_smooth_hessian (i j : Fin 3) {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) :
              ∃ (hmem : MeasureTheory.MemLp (mixedSecond (pressureNewtonianPotential F) i j) 2 MeasureTheory.volume), (rieszSecondL2Extension (rieszSecondL2Input i j)) (MeasureTheory.MemLp.toLp F ⋯) = MeasureTheory.MemLp.toLp (mixedSecond (pressureNewtonianPotential F) i j) hmem

              The completed endpoint extension agrees with the smooth Hessian on compact data.