Raw I3 Bound

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

noncomputable def CKN.caccioppoliI3HeatCutoffRaw {p : Foundation.Parabolic.ParabolicPoint → ℝ} {v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) : ℝ

Raw pressure contribution paired with velocity and the spatial gradient of the heat cutoff.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.caccioppoli_I3_heat_cutoff_raw_bound {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) (hscale : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I) (hvelocity : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) : caccioppoliI3HeatCutoffRaw hρ hε ≤ (3000 * cutoffGradientConstant + 1800000) * (ρ ^ 2 / r ^ 2) * delta p (x₀, t₀) ρ ^ 2 * gamma u (x₀, t₀) ρ

theorem CKN.caccioppoli_I3_heat_cutoff_raw_normalized {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r C₂₅ : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) (hscale : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I) (hvelocity : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) (hKbound : 3000 * cutoffGradientConstant + 1800000 ≤ C₂₅ ^ 2) : caccioppoliI3HeatCutoffRaw hρ hε ≤ (C₂₅ * (r / ρ)⁻¹ * delta p (x₀, t₀) ρ * gamma u (x₀, t₀) ρ ^ (1 / 2)) ^ 2