Harmonic Part Bounds

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

theorem CKN.exists_harmonicPressurePart_Ck_constant (k : ℕ) : ∃ (C₁₆ : ℝ), 0 ≤ C₁₆ ∧ ∀ {η : 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), ‖iteratedFDeriv ℝ k (harmonicPressurePart η u c p s) x‖ ≤ C₁₆ * ρ ^ (-(2 + ↑k)) * (A + B)