Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Euclidean.CZUnconditional

CZUnconditional #

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

Unconditional endpoint adapters #

The weak endpoint and the indexed L² input are now concrete. This file only retains the distributional identification data which are not consequences of the endpoint estimate.

source
noncomputable def CKN.Foundation.Euclidean.czGradientOperatorConstant :
ℝ

The explicit constant for the selected vector-valued gradient operator.

Equations
Instances For
    source
    noncomputable def CKN.Foundation.Euclidean.czP1OperatorConstant :
    ℝ

    The explicit component constant at exponent 3 / 2.

    Equations
    Instances For
      source
      theorem CKN.Foundation.Euclidean.hasCZGradientOperatorBound_unconditional :
      HasCZGradientOperatorBound (fun (i j : Fin 3) (G : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) => -rieszSecondGradientExtensionOperator (rieszSecondL2Input i j) ⋯ G x) czGradientOperatorConstant

      The selected signed gradient extension obeys its CZ operator bound.

      source
      theorem CKN.Foundation.Euclidean.rieszSecondP1_extension_operator_bound_unconditional (i j : Fin 3) {G : Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGc : HasCompactSupport G) :
      MeasureTheory.lpNorm (rieszSecondP1ExtensionOperator (rieszSecondL2Input i j) ⋯ G) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ czP1OperatorConstant * MeasureTheory.lpNorm G (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

      The scalar indexed extension has the exact hT norm-bound shape.

      source
      theorem CKN.Foundation.Euclidean.pressureSecondExtension_operator_bound_unconditional {G : Fin 3 → Fin 3 → Parabolic.Vec3 → ℝ} {E : ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGc : ∀ (i j : Fin 3), HasCompactSupport (G i j)) (hsource : ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.lpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hE : 0 ≤ E) :
      MeasureTheory.lpNorm (pressureSecondExtensionOperator rieszSecondL2Input rieszSecondL2_weak_type G) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ czP1OperatorConstant * E ^ (2 / 3)

      The tensor extension has the nine-index pressure norm bound.

      source
      theorem CKN.hCZ_p1_unconditional (C_CZ C₁₁ E C : ℝ) :
      0 ≤ C_CZ → ∀ (hoperator : Foundation.Euclidean.czP1OperatorConstant ≤ C_CZ) (hconst : C_CZ ≤ C₁₁) (hE : 0 ≤ E) (hC : 0 ≤ C) {p₁ : Foundation.Parabolic.Vec3 → ℝ} {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGc : ∀ (i j : Fin 3), HasCompactSupport (G i j)) (hsource : ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.lpNorm (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hP1 : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), p₁ x * spatialLaplacian ψ x = pressureSecondPairing G ψ) (hP1Int : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume) (hmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p₁ x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type G x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hgrowth : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p₁ x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type G x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)), MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E ^ (2 / 3)

      The pressure CZ estimate after the exact remaining identification data are supplied. The numerical constants precede the pressure and source data.