Harmonic Part Bounds AE

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

theorem CKN.vec3EuclideanNorm_le_sqrt_three (v : Foundation.Parabolic.Vec3) : Foundation.Parabolic.vec3EuclideanNorm v ≤ √3 * ‖v‖

theorem CKN.exists_harmonicPressurePart_Ck_ae_of_sws (k : ℕ) : ∃ (C₁₆ : ℝ), 0 ≤ C₁₆ ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ), closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖iteratedFDeriv ℝ k (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p s) x‖ ≤ C₁₆ * ρ ^ (-(2 + ↑k)) * (alpha u z ρ ^ 2 + MeasureTheory.lpNorm (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))