Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedSmoothLaplacianBridge

Smooth L² representatives and distributional derivatives #

Integration by parts against Schwartz functions identifies classical square-integrable derivatives with derivatives of their tempered L² distributions.

source
noncomputable def CKN.Leray.regularisedL2CoordinateBasis :
OrthonormalBasis (Fin 3) ℝ Foundation.Parabolic.L2Vec3

The coordinate orthonormal basis of the Euclidean spatial L² carrier.

Equations
Instances For
    source
    @[simp]
    theorem CKN.Leray.regularisedL2CoordinateBasis_apply (i : Fin 3) :
    regularisedL2CoordinateBasis i = WithLp.toLp 2 (basisVec i)

    Its basis vectors are the canonical spatial coordinate directions.

    source
    theorem CKN.Leray.regularised_smooth_L2_lineDerivative (f : Foundation.Parabolic.L2Vec3 → ComplexVec3) (hf : ContDiff ℝ (↑⊤) f) (v : Foundation.Parabolic.L2Vec3) (hfL2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hDfL2 : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.L2Vec3) => (fderiv ℝ f x) v) 2 MeasureTheory.volume) :
    LineDeriv.lineDerivOp v (MeasureTheory.Lp.toTemperedDistribution (MeasureTheory.MemLp.toLp f hfL2)) = MeasureTheory.Lp.toTemperedDistribution (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.L2Vec3) => (fderiv ℝ f x) v) hDfL2)

    A smooth L² vector field with an L² directional derivative has that classical derivative as its tempered-distribution derivative.

    source
    noncomputable def CKN.Leray.regularisedL2ClassicalLaplacian (f : Foundation.Parabolic.L2Vec3 → ComplexVec3) :
    Foundation.Parabolic.L2Vec3 → ComplexVec3

    The pointwise classical spatial Laplacian on the Hilbert carrier.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CKN.Leray.regularised_smooth_L2_laplacian (f : Foundation.Parabolic.L2Vec3 → ComplexVec3) (hf : ContDiff ℝ (↑⊤) f) (hfL2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hD1 : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.L2Vec3) => (fderiv ℝ f x) (regularisedL2CoordinateBasis i)) 2 MeasureTheory.volume) (hD2 : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.L2Vec3) => (fderiv ℝ (fun (y : Foundation.Parabolic.L2Vec3) => (fderiv ℝ f y) (regularisedL2CoordinateBasis i)) x) (regularisedL2CoordinateBasis i)) 2 MeasureTheory.volume) :
      Laplacian.laplacian (MeasureTheory.Lp.toTemperedDistribution (MeasureTheory.MemLp.toLp f hfL2)) = MeasureTheory.Lp.toTemperedDistribution (MeasureTheory.MemLp.toLp (regularisedL2ClassicalLaplacian f) ⋯)

      The distributional Laplacian of a smooth L² field agrees with the L² class of its classical Laplacian when its first and diagonal second derivatives are square-integrable.

      source
      theorem CKN.Leray.regularised_smooth_L2_even_lift_of_classical_iterates (k : ℕ) (f : Foundation.Parabolic.L2Vec3 → ComplexVec3) (hf : ContDiff ℝ (↑⊤) f) (hLp : ∀ (j : ℕ), MeasureTheory.MemLp (regularisedL2ClassicalLaplacian^[j] f) 2 MeasureTheory.volume) (hD1 : ∀ (j : ℕ) (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.L2Vec3) => (fderiv ℝ (regularisedL2ClassicalLaplacian^[j] f) x) (regularisedL2CoordinateBasis i)) 2 MeasureTheory.volume) (hD2 : ∀ (j : ℕ) (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.L2Vec3) => (fderiv ℝ (fun (y : Foundation.Parabolic.L2Vec3) => (fderiv ℝ (regularisedL2ClassicalLaplacian^[j] f) y) (regularisedL2CoordinateBasis i)) x) (regularisedL2CoordinateBasis i)) 2 MeasureTheory.volume) :
      ∃ (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2), regularisedBesselSobolevToL2 ↑(2 * k) ⋯ b = MeasureTheory.MemLp.toLp f ⋯

      Smooth fields with all classical Laplacian iterates and their first two coordinate derivatives in L² have the matching even-order Bessel lift.