Identification Extension Unconditional

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

noncomputable def CKN.pressureExponent : ENNReal

Three-halves integrability exponent for pressure.

Equations

• CKN.pressureExponent = ENNReal.ofReal (3 / 2)

theorem CKN.pressureSecondExtension_residual_local_growth {p₁ Tg : Foundation.Parabolic.Vec3 → ℝ} (hp₁ : MeasureTheory.MemLp p₁ pressureExponent MeasureTheory.volume) (hTg : MeasureTheory.MemLp Tg pressureExponent MeasureTheory.volume) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => p₁ x - Tg x) pressureExponent (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p₁ x - Tg x) pressureExponent (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (MeasureTheory.lpNorm p₁ pressureExponent MeasureTheory.volume + MeasureTheory.lpNorm Tg pressureExponent MeasureTheory.volume) * (1 + ρ)

theorem CKN.pressureSecondExtension_residual_local_growth_of_source_bound {p₁ : Foundation.Parabolic.Vec3 → ℝ} {G : Fin 3 → Fin 3 → Foundation.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) (hp₁ : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) : (∀ (ρ : ℝ), 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 ρ))) ∧ ∀ (ρ : ℝ), 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 ρ)) ≤ (MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume + Foundation.Euclidean.czP1OperatorConstant * E ^ (2 / 3)) * (1 + ρ)

The endpoint weak-type certificate is now unconditional. This adapter fixes the extension to the canonical L² inputs and removes the operator-bound function from the pressure identification interface.

theorem CKN.pressureP1_hident_of_pressureSecondExtension_unconditional {p₁ : Foundation.Parabolic.Vec3 → ℝ} {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {C : ℝ} (hC : 0 ≤ C) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (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 + ρ)) : p₁ =ᵐ[MeasureTheory.volume] pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type G

theorem CKN.pressureP1_hCZ_slice_of_unconditional_extension (C_CZ : ℝ) (hC_CZ : 0 ≤ C_CZ) (hoperator : Foundation.Euclidean.czP1OperatorConstant ≤ C_CZ) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Ω) {c : ℝ → Foundation.Parabolic.Vec3} (hG : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i j : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ (∫ (x : Foundation.Parabolic.Vec3), pressureUTensorNorm u c s x ^ (3 / 2)) ^ (2 / 3)) (hresidual : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∃ (C : ℝ), 0 ≤ C ∧ (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureP1 η u c p f s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type (fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureP1 η u c p f s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type (fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.MemLp (pressureP1 η u c p f s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (pressureP1 η u c p f s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * (∫ (x : Foundation.Parabolic.Vec3), pressureUTensorNorm u c s x ^ (3 / 2)) ^ (2 / 3)