Identification Whole Space

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

theorem CKN.pressureP1_eq_of_wholeSpace_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 ψ → 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 ψ → 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 ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => p₁ x * spatialLaplacian ψ x) MeasureTheory.volume) (hTInt : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → 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

A whole-space distributional identity is the form consumed by the Liouville identification. Unlike the local slice export, this identity quantifies over every compactly supported smooth test.