Lin34 Centred Pairing

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

The whole-space pairing identity for the centred first pressure potential

prop:pressure-decomposition of paper/ckn.tex produces, for a suitable weak solution, the distributional identity pairing the leading potential p₁ with Δψ against the singly centred nonlinearity U_ij = -u_i (u_j - c_j) of eq:Uij. The oscillation estimate prop:lin34 runs the same decomposition with the doubly centred nonlinearity Û_ij = -(u_i - c_i)(u_j - c_j) of eq:Uhat. The two identities differ by the pairing of the correction U_ij - Û_ij = -c_i (u_j - c_j), which vanishes because u is weakly divergence free and a constant vector field is divergence free. This file carries out that correction and produces the identification data consumed by the Calderón--Zygmund estimate for the centred potential.

noncomputable def CKN.lin34MeanVelocity (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) (ρ : ℝ) : ℝ → Foundation.Parabolic.Vec3

The spatial average ⨍_{B_ρ(x₀)} u(·, s) of eq:Chat, seen as a time-dependent constant vector.

Equations

• CKN.lin34MeanVelocity u x₀ ρ s j = ⨍ (z : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ ρ, u (z, s) j

theorem CKN.lin34_centredVelocity_apply (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) (ρ s : ℝ) (y : Foundation.Parabolic.Vec3) (j : Fin 3) : lin34CentredVelocity u x₀ ρ (y, s) j = u (y, s) j - lin34MeanVelocity u x₀ ρ s j

The mean-free velocity of eq:Uhat is the velocity minus its spatial average.

theorem CKN.lin34_pressureUTensor_sub_centred (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) (ρ s : ℝ) (y : Foundation.Parabolic.Vec3) (i j : Fin 3) : pressureUTensor u (lin34MeanVelocity u x₀ ρ) (y, s) i j - pressureUTensor (lin34CentredVelocity u x₀ ρ) 0 (y, s) i j = -(lin34MeanVelocity u x₀ ρ s i * (u (y, s) j - lin34MeanVelocity u x₀ ρ s j))

The singly and doubly centred nonlinearities of eq:Uij and eq:Uhat differ by the constant-vector correction -c_i (u_j - c_j).

theorem CKN.lin34_centredP1_sub_pressureP1 (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (s : ℝ) (x : Foundation.Parabolic.Vec3) : lin34CentredP1 u p f x₀ ρ hρ s x - pressureP1 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) p f s x = pressureP2 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) s x + pressureP3 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) s x + pressureP4 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) s x - (pressureP2 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP3 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP4 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x)

The centred and singly centred leading potentials differ only through the three tensor potentials p₂, p₃, p₄ of prop:pressure-decomposition.

Integrability bookkeeping on the support of the cut-off

theorem CKN.lin34_centredP1_pairing_of_slice_data {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {s : ℝ} {Ω' : Set Foundation.Parabolic.Vec3} (hηΩ' : tsupport (mollifiedBallCutoff x₀ hρ) ⊆ Ω') (hU : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u (lin34MeanVelocity u x₀ ρ) (y, s) i j) (tsupport (mollifiedBallCutoff x₀ hρ)) MeasureTheory.volume) (hUhat : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor (lin34CentredVelocity u x₀ ρ) 0 (y, s) i j) (tsupport (mollifiedBallCutoff x₀ hρ)) MeasureTheory.volume) (hum : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j) Ω' MeasureTheory.volume) (hdivΩ' : ∀ (φ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ Ω' → ∫ (x : Foundation.Parabolic.Vec3) in Ω', ∑ i : Fin 3, u (x, s) i * (fderiv ℝ φ x) (basisVec i) = 0) (hP1 : ∀ (χ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) χ → HasCompactSupport χ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) p f s x * spatialLaplacian χ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), pressureP1 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) p f s x * spatialLaplacian χ x = pressureSecondPairing (fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) => mollifiedBallCutoff x₀ hρ x * pressureUTensor u (lin34MeanVelocity u x₀ ρ) (x, s) i j) χ) (hP1Int : ∀ (χ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) χ → HasCompactSupport χ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureP1 (mollifiedBallCutoff x₀ hρ) u (lin34MeanVelocity u x₀ ρ) p f s x * spatialLaplacian χ x) MeasureTheory.volume) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f x₀ ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume ∧ ∫ (x : Foundation.Parabolic.Vec3), lin34CentredP1 u p f x₀ ρ hρ s x * spatialLaplacian ψ x = pressureSecondPairing (lin34CentredSource u x₀ hρ s) ψ

The whole-space pairing identity for the centred potential at one time slice. The singly centred identity of prop:pressure-decomposition is corrected by the constant-vector pairing, which vanishes by the weak divergence-free condition; what remains is the identity for the doubly centred nonlinearity eq:Uhat, which is the form ext:CZ consumes.