Gamma Assembly #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
This adapter assembles the four raw terms in the gamma form of
lem:caccioppoli-gamma. The lower energy certificate remains explicit until
the unconditional Caccioppoli producer supplies it.
theorem
CKN.caccioppoli_gamma_of_raw_bounds
{Ω : 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₂₅ C₂₆ : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hC₂₅ : 0 ≤ C₂₅)
(hC₂₆ : 0 ≤ C₂₆)
(hK₁ :
6000 * ((Real.pi * 4 / 3) ^ (1 / 3) * ((32 + 3 * cutoffSecondDerivativeConstant) * 8000000 + 6 * cutoffGradientConstant * 5000000)) ≤ C₂₅ ^ 2)
(hK₂ : 6000 * (3 * (1500 * cutoffGradientConstant + 900000)) ≤ C₂₅ ^ 2)
(hK₃ : 6000 * (3000 * cutoffGradientConstant + 1800000) ≤ C₂₅ ^ 2)
(hK₄ : 6000 * (2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3)) ≤ C₂₆ ^ 2)
{c : Foundation.Parabolic.ParabolicPoint → ℝ}
(hc : ∀ (w : Foundation.Parabolic.ParabolicPoint), 0 ≤ c w)
(hcm : AEMeasurable c (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hA₁ :
AEMeasurable
(fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 2)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)))
(hmean :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (c w) ^ (3 / 2) ≤ ENNReal.ofReal (ρ ^ 2 * gamma u (x₀, t₀) ρ ^ 3))
(hvelocity :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≠ ⊤)
{I₁ I₂ I₃ I₄ : ℝ}
(hLower : (alpha u (x₀, t₀) r + beta u Du (x₀, t₀) r) ^ 2 ≤ 6000 * (I₁ + I₂ + I₃ + I₄))
(hI₁ : I₁ = caccioppoliI1HeatCutoffRaw hρ hε)
(hI₂ : I₂ = caccioppoliI2HeatCutoffRaw hρ hε)
(hI₃ : I₃ = caccioppoliI3HeatCutoffRaw hρ hε)
(hI₄ : I₄ = caccioppoliI4HeatCutoffRaw hρ hε)
:
Assemble the gamma form from the two gamma replacements and the raw pressure and force estimates.