Identification

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

noncomputable def CKN.pressureSecondPairing (G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (ψ : Foundation.Parabolic.Vec3 → ℝ) : ℝ

Pairing of a tensor source with the Hessian of a scalar test function.

Equations

• CKN.pressureSecondPairing G ψ = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * CKN.mixedSecond ψ i j x

theorem CKN.pressureP1_residual_weaklyHarmonic {p₁ Tg : Foundation.Parabolic.Vec3 → ℝ} {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hP1 : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), p₁ x * spatialLaplacian ψ x = pressureSecondPairing G ψ) (hT : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => Tg x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), Tg x * spatialLaplacian ψ x = pressureSecondPairing G ψ) (hP1Int : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume) (hTInt : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => Tg x * spatialLaplacian ψ x) MeasureTheory.volume) : Foundation.Heat.WeaklyHarmonicOn Set.univ (p₁ - Tg)

The difference between a pressure term and a candidate second-order Newtonian operator is weakly harmonic when the two distributional identities have the same tensor source.

theorem CKN.pressureP1_eq_of_distributional_identity_and_linear_growth {p₁ Tg : Foundation.Parabolic.Vec3 → ℝ} {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {C : ℝ} (hC : 0 ≤ C) (hP1 : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), p₁ x * spatialLaplacian ψ x = pressureSecondPairing G ψ) (hT : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => Tg x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), Tg x * spatialLaplacian ψ x = pressureSecondPairing G ψ) (hP1Int : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume) (hTInt : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Set.univ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => Tg x * spatialLaplacian ψ x) MeasureTheory.volume) (hmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (p₁ - Tg) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hgrowth : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (p₁ - Tg) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)) : p₁ =ᵐ[MeasureTheory.volume] Tg

Identification of the leading pressure term from the residual growth and the distributional identities. The residual hypotheses are the analytic decay-at-infinity input for the compactly supported pressure data.

theorem CKN.pressure_lpNorm_le_of_operator_bound {T : (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ} {p₁ g : Foundation.Parabolic.Vec3 → ℝ} {C_CZ : ℝ} (hT : ∀ (f : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume → HasCompactSupport f → MeasureTheory.lpNorm (T f) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hgc : HasCompactSupport g) (hident : p₁ =ᵐ[MeasureTheory.volume] T g) : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

The operator-bound part of the pressure identification, isolated from the distributional argument so the eventual singular-integral theorem can be substituted without changing downstream consumers.

theorem CKN.hCZ_p1_of_operator_bound {T : (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ} {p₁ g : Foundation.Parabolic.Vec3 → ℝ} {C_CZ C₁₁ E : ℝ} (hT : ∀ (f : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume → HasCompactSupport f → MeasureTheory.lpNorm (T f) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C_CZ * MeasureTheory.lpNorm f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hg : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hgc : HasCompactSupport g) (hident : p₁ =ᵐ[MeasureTheory.volume] T g) (hsource : MeasureTheory.lpNorm g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ E ^ (2 / 3)) (hC_CZ : 0 ≤ C_CZ) (hconst : C_CZ ≤ C₁₁) (hE : 0 ≤ E) : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E ^ (2 / 3)

Discharge the exact global hCZ_p1 shape used by the lpNorm pressure consumers from the singular-integral estimate and a source norm bound.