Raw I2 Bound

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

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

Raw transport contribution after subtracting the chosen scalar energy center.

Equations

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

theorem CKN.caccioppoli_I2_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) {c : Foundation.Parabolic.ParabolicPoint → ℝ} {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r C_PS : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hC_PS : 0 ≤ C_PS) (hr : 0 < r) (hscale : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I) (hA : AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w|) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ))) (hcenter : (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w| ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal (C_PS * ρ ^ (4 / 3) * alpha u (x₀, t₀) ρ * beta u Du (x₀, t₀) ρ)) (hvelocity : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) : caccioppoliI2HeatCutoffRaw hρ hε ≤ C_PS * (1500 * cutoffGradientConstant + 900000) * (ρ ^ 2 / r ^ 2) * alpha u (x₀, t₀) ρ * beta u Du (x₀, t₀) ρ * gamma u (x₀, t₀) ρ

theorem CKN.caccioppoli_I2_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) {c : Foundation.Parabolic.ParabolicPoint → ℝ} {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r C₂₅ C_PS : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hC_PS : 0 ≤ C_PS) (hr : 0 < r) (hscale : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I) (hA : AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w|) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ))) (hcenter : (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w| ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal (C_PS * ρ ^ (4 / 3) * alpha u (x₀, t₀) ρ * beta u Du (x₀, t₀) ρ)) (hvelocity : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤) (hKbound : C_PS * (1500 * cutoffGradientConstant + 900000) ≤ C₂₅ ^ 2) : caccioppoliI2HeatCutoffRaw hρ hε ≤ (C₂₅ * (r / ρ)⁻¹ * alpha u (x₀, t₀) ρ ^ (1 / 2) * beta u Du (x₀, t₀) ρ ^ (1 / 2) * gamma u (x₀, t₀) ρ ^ (1 / 2)) ^ 2