Pk Bounds Cylinder

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

theorem CKN.pressure_cutoff_spatialDeriv_bound (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (y : Foundation.Parabolic.Vec3) (i : Fin 3) : |spatialDeriv (mollifiedBallCutoff x₀ hρ) i y| ≤ cutoffGradientConstant / ρ

theorem CKN.pressure_cutoff_mixedSecond_bound (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (y : Foundation.Parabolic.Vec3) (i j : Fin 3) : |mixedSecond (mollifiedBallCutoff x₀ hρ) i j y| ≤ cutoffSecondDerivativeConstant / ρ ^ 2

theorem CKN.pressure_cutoff_derivatives_vanish (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) {y : Foundation.Parabolic.Vec3} (hy : y ∉ euclideanBall x₀ (3 * ρ / 4) \ euclideanClosedBall x₀ (13 * ρ / 20)) : (∀ (i : Fin 3), spatialDeriv (mollifiedBallCutoff x₀ hρ) i y = 0) ∧ ∀ (i j : Fin 3), mixedSecond (mollifiedBallCutoff x₀ hρ) i j y = 0

theorem CKN.pressure_cutoff_support_subset_ball (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) : tsupport (mollifiedBallCutoff x₀ hρ) ⊆ Foundation.Parabolic.vec3Ball x₀ ρ

theorem CKN.pressure_kernel_meas_shift (x : Foundation.Parabolic.Vec3) : Measurable fun (y : Foundation.Parabolic.Vec3) => -Foundation.Heat.newtonianKernel (x - y)

theorem CKN.pressure_kernel_deriv_meas_shift (x : Foundation.Parabolic.Vec3) (i : Fin 3) : Measurable fun (y : Foundation.Parabolic.Vec3) => spatialDeriv Foundation.Heat.newtonianKernel i (x - y)

theorem CKN.pressure_potential_source_integrable {g : Foundation.Parabolic.Vec3 → ℝ} {x₀ x : Foundation.Parabolic.Vec3} {ρ ρ' : ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hA : ∀ (y : Foundation.Parabolic.Vec3), g y ≠ 0 → y ∈ pressureAnnulus x₀ ρ') (hρ : 0 < ρ') (hr : 0 < ρ) (hhalf : ρ ≤ ρ' / 2) (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ ρ) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => -Foundation.Heat.newtonianKernel (x - y) * g y) MeasureTheory.volume

theorem CKN.pressure_derivative_source_integrable {g : Foundation.Parabolic.Vec3 → ℝ} {x₀ x : Foundation.Parabolic.Vec3} {ρ ρ' : ℝ} (i : Fin 3) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hA : ∀ (y : Foundation.Parabolic.Vec3), g y ≠ 0 → y ∈ pressureAnnulus x₀ ρ') (hρ : 0 < ρ') (hr : 0 < ρ) (hhalf : ρ ≤ ρ' / 2) (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ ρ) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * g y) MeasureTheory.volume

theorem CKN.pressure_utensor_integrable_on_ball {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ s : ℝ} : 0 < ρ → ∀ (humeas : AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hu : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))), MeasureTheory.Integrable (pressureUTensorNorm u c s) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))

theorem CKN.pressure_spatialGradientSq_le (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (w : Foundation.Parabolic.ParabolicPoint) : spatialGradientSq u Du w ≤ 9 * ‖Du w‖ ^ 2

theorem CKN.pressureP234_fixed_bound {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ r s : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hC₁ : 0 ≤ cutoffGradientConstant) (hC₂ : 0 ≤ cutoffSecondDerivativeConstant) (hηeq : η = mollifiedBallCutoff x₀ hρ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ ρ) : Foundation.Parabolic.vec3Ball x₀ ρ ⊆ Foundation.Parabolic.vec3Ball x₀ ρ → ∀ (hu : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))), AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)) → ∀ (hU : MeasureTheory.Integrable (pressureUTensorNorm u c s) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))), ∀ x ∈ Foundation.Parabolic.vec3Ball x₀ r, |pressureP2 η u c s x| + |pressureP3 η u c s x| + |pressureP4 η u c s x| ≤ (18 * cutoffSecondDerivativeConstant + 720 * cutoffGradientConstant) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, pressureUTensorNorm u c s y

Cylinder assembly for the pressure terms whose fixed-time estimates use the annular part of the cutoff.

theorem CKN.pressureP234_cylinder_bound {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {t₀ r ρ K C₁₂ α β : ℝ} : 0 < ρ → ∀ (hr : 0 < r), r ≤ ρ / 2 → ∀ (hK : 0 ≤ K) {G : ℝ → ℝ} (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (Set.Ioc (t₀ - r ^ 2) t₀))) (hP₂ : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r), ‖pressureP2 η u c z.2 z.1‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ) (hP₃ : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r), ‖pressureP3 η u c z.2 z.1‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ) (hP₄ : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r), ‖pressureP4 η u c z.2 z.1‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ) (hscale : ENNReal.ofReal (r ^ (-4 / 3)) * (3 * (ENNReal.ofReal K ^ (3 / 2) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x₀ r) * ∫⁻ (s : ℝ) in Set.Ioc (t₀ - r ^ 2) t₀, ‖G s‖ₑ ^ (3 / 2)) ^ (2 / 3)) ≤ ENNReal.ofReal (C₁₂ * (r / ρ) * α * β)), ENNReal.ofReal (r ^ (-4 / 3)) * (MeasureTheory.eLpNorm' (fun (z : Foundation.Parabolic.ParabolicPoint) => pressureP2 η u c z.2 z.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r)) + MeasureTheory.eLpNorm' (fun (z : Foundation.Parabolic.ParabolicPoint) => pressureP3 η u c z.2 z.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r)) + MeasureTheory.eLpNorm' (fun (z : Foundation.Parabolic.ParabolicPoint) => pressureP4 η u c z.2 z.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r))) ≤ ENNReal.ofReal (C₁₂ * (r / ρ) * α * β)

theorem CKN.pressureP56_cylinder_bound {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {x₀ : Foundation.Parabolic.Vec3} {t₀ r ρ K C₁₂ δ : ℝ} : 0 < ρ → ∀ (hr : 0 < r), r ≤ ρ / 2 → ∀ (hK : 0 ≤ K) {G : ℝ → ℝ} (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (Set.Ioc (t₀ - r ^ 2) t₀))) (hP₅ : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r), ‖pressureP5 η p z.2 z.1‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ) (hP₆ : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r), ‖pressureP6 η p z.2 z.1‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ) (hscale : ENNReal.ofReal (r ^ (-4 / 3)) * (2 * (ENNReal.ofReal K ^ (3 / 2) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x₀ r) * ∫⁻ (s : ℝ) in Set.Ioc (t₀ - r ^ 2) t₀, ‖G s‖ₑ ^ (3 / 2)) ^ (2 / 3)) ≤ ENNReal.ofReal (C₁₂ * (r / ρ) ^ (2 / 3) * δ ^ 2)), ENNReal.ofReal (r ^ (-4 / 3)) * (MeasureTheory.eLpNorm' (fun (z : Foundation.Parabolic.ParabolicPoint) => pressureP5 η p z.2 z.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r)) + MeasureTheory.eLpNorm' (fun (z : Foundation.Parabolic.ParabolicPoint) => pressureP6 η p z.2 z.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r))) ≤ ENNReal.ofReal (C₁₂ * (r / ρ) ^ (2 / 3) * δ ^ 2)

theorem CKN.pressureP8_cylinder_bound {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {t₀ r ρ K C₁₃ lam : ℝ} : 0 < ρ → ∀ (hr : 0 < r), r ≤ ρ / 2 → ∀ (hK : 0 ≤ K) {G : ℝ → ℝ} (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (Set.Ioc (t₀ - r ^ 2) t₀))) (hP₈ : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r), ‖pressureP8 η f z.2 z.1‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ) (hscale : ENNReal.ofReal (r ^ (-4 / 3)) * (ENNReal.ofReal K ^ (3 / 2) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x₀ r) * ∫⁻ (s : ℝ) in Set.Ioc (t₀ - r ^ 2) t₀, ‖G s‖ₑ ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal (C₁₃ * (r / ρ) * lam)), ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (z : Foundation.Parabolic.ParabolicPoint) => pressureP8 η f z.2 z.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ r)) ≤ ENNReal.ofReal (C₁₃ * (r / ρ) * lam)