Support bounds for centred cutoff corrections

The pressure-gradient construction uses a centred cutoff and its spatial derivatives. This file records the pointwise support and correction estimates needed when the cutoff and its derivatives are contained in the source ball. The displayed bounds keep the centred velocity tensor and the velocity-gradient centring term explicit, so they can be consumed by the source estimates.

Main results

• centredRawSourceCorrection_abs_le_of_support: a pointwise triangle bound for the centred raw-source correction under support hypotheses.
• mollifiedBallCutoff_eq_zero_outside_source_ball: the centred cutoff vanishes outside the source ball under the gap condition.
• spatialDeriv_mollifiedBallCutoff_eq_zero_outside_source_ball: every spatial derivative of that cutoff vanishes there under the same condition.

Pressure Gradient Origin KPHarmonic Small Cells

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

noncomputable def CKN.Core.Step4.originHarmonicCellRadius (r : ℝ) : ℝ

The source collar is never smaller than one quarter, while its half-ball contains the tested small cell.

Equations

• CKN.Core.Step4.originHarmonicCellRadius r = max (1 / 4) (2 * r)

theorem CKN.Core.Step4.centredRawSourceCorrection_abs_le_of_support {R₀ Kη : ℝ} {η : Foundation.Parabolic.Vec3 → ℝ} {dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hη0 : ∀ (x : Foundation.Parabolic.Vec3), 0 ≤ η x) (hη1 : ∀ (x : Foundation.Parabolic.Vec3), η x ≤ 1) (hsupp : ∀ x ∉ Foundation.Parabolic.vec3Ball 0 R₀, η x = 0) (hdη : ∀ (k : Fin 3) (x : Foundation.Parabolic.Vec3), |dη k x| ≤ Kη) (hdsupp : ∀ (k : Fin 3), ∀ x ∉ Foundation.Parabolic.vec3Ball 0 R₀, dη k x = 0) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (c : Foundation.Parabolic.Vec3) (j : Fin 3) (x : Foundation.Parabolic.Vec3) : |centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η dη u f Du c j x| ≤ |(Foundation.Parabolic.vec3Ball 0 R₀).indicator (fun (y : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du y j k * u y k - f y j) x| + Kη * ∑ k : Fin 3, |(Foundation.Parabolic.vec3Ball 0 R₀).indicator (fun (y : Foundation.Parabolic.Vec3) => u y j * (u y k - c k)) x| + ∑ k : Fin 3, |(Foundation.Parabolic.vec3Ball 0 R₀).indicator (fun (y : Foundation.Parabolic.Vec3) => Du y j k * c k) x|

The correction under the support containment. If the cutoff and its spatial derivatives vanish outside vec3Ball 0 R₀ and the cutoff takes values in [0,1], then the raw-source correction is dominated pointwise by the raw divergence source, the centred velocity tensor and the velocity-gradient centring term, each restricted to vec3Ball 0 R₀, with the cutoff-gradient size as the only coefficient. Every majorant on the right is supported where the A binder's Morrey bounds KU, KD apply.

theorem CKN.Core.Step4.mollifiedBallCutoff_eq_zero_outside_source_ball {ρ R₁ R₀ : ℝ} (hρ : 0 < ρ) (hR₁ : 0 < R₁) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁)) (hgap : R₁ + 3 * ρ / 4 ≤ R₀) (x : Foundation.Parabolic.Vec3) : x ∉ Foundation.Parabolic.vec3Ball 0 R₀ → mollifiedBallCutoff z.1 hρ x = 0

The gap condition that makes the containment true. If the collar radius satisfies R₁ + 3ρ/4 ≤ R₀ then, for every centre in the closure of the carrier of radius R₁, the centred cutoff vanishes outside the source ball.

theorem CKN.Core.Step4.spatialDeriv_mollifiedBallCutoff_eq_zero_outside_source_ball {ρ R₁ R₀ : ℝ} (hρ : 0 < ρ) (hR₁ : 0 < R₁) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁)) (hgap : R₁ + 3 * ρ / 4 ≤ R₀) (k : Fin 3) (x : Foundation.Parabolic.Vec3) : x ∉ Foundation.Parabolic.vec3Ball 0 R₀ → spatialDeriv (mollifiedBallCutoff z.1 hρ) k x = 0

Under the same gap condition every first spatial derivative of the centred cutoff vanishes outside the source ball.