The identification data for the leading pressure term

The Calderón--Zygmund bound for the leading local pressure p₁ consumes two facts about a fixed time slice: the whole-space distributional identity pairing p₁(·, s) with Δψ against the tensor source η U(·, s), and the integrability of that pairing, both for every compactly supported smooth spatial test function ψ. The identity produced by the pressure decomposition holds, for each fixed ψ, only for almost every time, with an exceptional set depending on ψ. Testing against the countable family of mollifier bumps removes that dependence, and the two facts below hold, for almost every time, simultaneously for every test function.

noncomputable def CKN.pressureP1Residual (η : Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) (i j : Fin 3) : Foundation.Parabolic.Vec3 → ℝ

The residual matrix field whose second-order pairing measures the failure of the whole-space identity: the diagonal carries p₁(·, s) and the full matrix carries the tensor source η U(·, s).

Equations

• CKN.pressureP1Residual η u c p f s i j x = (if i = j then CKN.pressureP1 η u c p f s x else 0) - η x * CKN.pressureUTensor u c (x, s) i j

theorem CKN.pressureP1_cz_identification_data_ae_of_sws {Ω : 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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, (∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP1 η u c p f s x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), pressureP1 η u c p f s x * spatialLaplacian ψ x = pressureSecondPairing (fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) ψ) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP1 η u c p f s x * spatialLaplacian ψ x) MeasureTheory.volume

The Calderón--Zygmund identification data for the leading local pressure. For almost every time the whole-space distributional identity and the integrability of the pairing hold simultaneously for every compactly supported smooth spatial test function; the tensor source is η U(·, s).

theorem CKN.pressureP1_cz_hP1_ae_of_sws {Ω : 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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP1 η u c p f s x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), pressureP1 η u c p f s x * spatialLaplacian ψ x = pressureSecondPairing (fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) => η x * pressureUTensor u c (x, s) i j) ψ

The whole-space pairing identity in the exact binder shape consumed by the pressure Calderón--Zygmund estimate.

theorem CKN.pressureP1_cz_hP1Int_ae_of_sws {Ω : 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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP1 η u c p f s x * spatialLaplacian ψ x) MeasureTheory.volume

The test-pairing integrability in the exact binder shape consumed by the pressure Calderón--Zygmund estimate.