Harmonic Part Bounds Terms #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.harmonicPressurePart_term_bounds
(k : ℕ)
:
∃ (cN : ℝ) (cD : ℝ) (κ : ℝ),
0 ≤ cN ∧ 0 ≤ cD ∧ 0 ≤ κ ∧ ∀ {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ}
{x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ),
PressureHarmonicPotentialData (Foundation.Parabolic.vec3Ball x₀ (13 * ρ / 20)) η u c p s →
η = mollifiedBallCutoff x₀ hρ →
(∀ y ∉ pressureAnnulus x₀ ρ,
(∀ (i : Fin 3), spatialDeriv η i y = 0) ∧ (∀ (i j : Fin 3), mixedSecond η i j y = 0) ∧ spatialLaplacian η y = 0) →
MeasureTheory.Integrable (pressureUTensorNorm u c s)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)) →
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)) →
∀ (A B : ℝ),
0 ≤ A →
0 ≤ B →
∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, pressureUTensorNorm u c s y ≤ 2 * ρ * A →
∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)| ≤ (Real.pi * 4 / 3) ^ (1 / 3) * ρ * B →
∀ x ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2),
ContDiffOn ℝ (↑k) (pressureP2 η u c s) (Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) ∧ ContDiffOn ℝ (↑k) (pressureP3 η u c s) (Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) ∧ ContDiffOn ℝ (↑k) (pressureP4 η u c s) (Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) ∧ ContDiffOn ℝ (↑k) (pressureP5 η p s) (Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) ∧ ContDiffOn ℝ (↑k) (pressureP6 η p s)
(Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) ∧ ‖iteratedFDeriv ℝ k (pressureP2 η u c s) x‖ ≤ 18 * cN * cutoffSecondDerivativeConstant * (3 / 20) ^ (-(1 + ↑k)) * ρ ^ (-(2 + ↑k)) * A ∧ ‖iteratedFDeriv ℝ k (pressureP3 η u c s) x‖ ≤ 18 * cD * cutoffGradientConstant * (3 / 20) ^ (-(2 + ↑k)) * ρ ^ (-(2 + ↑k)) * A ∧ ‖iteratedFDeriv ℝ k (pressureP4 η u c s) x‖ ≤ 18 * cD * cutoffGradientConstant * (3 / 20) ^ (-(2 + ↑k)) * ρ ^ (-(2 + ↑k)) * A ∧ ‖iteratedFDeriv ℝ k (pressureP5 η p s) x‖ ≤ 3 * κ * cN * cutoffSecondDerivativeConstant * (3 / 20) ^ (-(1 + ↑k)) * ρ ^ (-(2 + ↑k)) * B ∧ ‖iteratedFDeriv ℝ k (pressureP6 η p s) x‖ ≤ 6 * κ * cD * cutoffGradientConstant * (3 / 20) ^ (-(2 + ↑k)) * ρ ^ (-(2 + ↑k)) * B