Caccioppoli

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

noncomputable def CKN.caccioppoliC₂₅BaseSquared : ℝ

Squared common coefficient collecting the velocity and pressure terms in the Caccioppoli estimate.

Equations

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

noncomputable def CKN.caccioppoliC₂₅Base : ℝ

Square root of the common Caccioppoli coefficient, used before the final energy normalization.

Equations

• CKN.caccioppoliC₂₅Base = √CKN.caccioppoliC₂₅BaseSquared

noncomputable def CKN.caccioppoliC₂₅ : ℝ

Velocity and pressure coefficient after normalizing the Caccioppoli energy bound.

Equations

• CKN.caccioppoliC₂₅ = √(6000 * CKN.caccioppoliC₂₅BaseSquared)

noncomputable def CKN.caccioppoliC₂₆ (q : ℝ) : ℝ

Force coefficient in the Caccioppoli estimate for local integrability exponent q.

Equations

• CKN.caccioppoliC₂₆ q = √(6000 * (2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3)))

theorem CKN.caccioppoli {Ω : 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) {z₀ : Foundation.Parabolic.ParabolicPoint} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hrr : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 ρ) ⊆ spaceTimeSet Ω I) : alpha u z₀ r + beta u Du z₀ r ≤ caccioppoliC₂₅ * (r / ρ) * alpha u z₀ ρ + caccioppoliC₂₅ * (r / ρ)⁻¹ * alpha u z₀ ρ ^ (1 / 2) * beta u Du z₀ ρ ^ (1 / 2) * gamma u z₀ ρ ^ (1 / 2) + caccioppoliC₂₅ * (r / ρ)⁻¹ * delta p z₀ ρ * gamma u z₀ ρ ^ (1 / 2) + caccioppoliC₂₆ q * (r / ρ) ^ (-1 / 2) * gamma u z₀ ρ ^ (1 / 2) * lambda q f z₀ ρ ^ (1 / 2)