Raw I4 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.caccioppoliI4HeatCutoffRaw
{u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ ε r : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
:
Raw forcing contribution to the local energy estimate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.caccioppoli_I4_heat_cutoff_raw_bound_of_finiteness
{Ω : 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)
:
ε < 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 ≠ ⊤),
caccioppoliI4HeatCutoffRaw hρ hε ≤ 2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3) * (r / ρ)⁻¹ * gamma u (x₀, t₀) ρ * lambda q f (x₀, t₀) ρ
theorem
CKN.caccioppoli_I4_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)
(hεr : ε < 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 : 2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3) ≤ C₂₆ ^ 2)
: