Caccioppoli Assembly #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_centered_bound_of_slice_data
{B : Set Foundation.Parabolic.Vec3}
{T : Set ℝ}
{g e d : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{F E D : ℝ → ENNReal}
{E₀ D₀ V : ENNReal}
{cC : ℝ}
(hFdef : ∀ (s : ℝ), F s = ∫⁻ (x : Foundation.Parabolic.Vec3) in B, ENNReal.ofReal (g (x, s)))
(hEdef : ∀ (s : ℝ), E s = ∫⁻ (x : Foundation.Parabolic.Vec3) in B, ENNReal.ofReal (e (x, s)))
(hDdef : ∀ (s : ℝ), D s = ∫⁻ (x : Foundation.Parabolic.Vec3) in B, ENNReal.ofReal (d (x, s)))
(hDmeas : AEMeasurable D (MeasureTheory.volume.restrict T))
(hgInt :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => g (x, s)) B MeasureTheory.volume)
(heInt :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => e (x, s)) B MeasureTheory.volume)
(hdInt :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => d (x, s)) B MeasureTheory.volume)
(hgn :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, 0 ≤ᵐ[MeasureTheory.volume.restrict B] fun (x : Foundation.Parabolic.Vec3) => g (x, s))
(hen :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, 0 ≤ᵐ[MeasureTheory.volume.restrict B] fun (x : Foundation.Parabolic.Vec3) => e (x, s))
(hdn :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, 0 ≤ᵐ[MeasureTheory.volume.restrict B] fun (x : Foundation.Parabolic.Vec3) => d (x, s))
(hpoint :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, (∫ (x : Foundation.Parabolic.Vec3) in B, g (x, s)) ^ (2 / 3) ≤ cC * (∫ (x : Foundation.Parabolic.Vec3) in B, e (x, s)) ^ (1 / 2) * (∫ (x : Foundation.Parabolic.Vec3) in B, d (x, s)) ^ (1 / 2))
(hC : 0 ≤ cC)
(hCtop : ENNReal.ofReal cC ≠ ⊤)
(hEbound : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, E s ≤ E₀)
(hDint : ∫⁻ (s : ℝ) in T, D s ≤ D₀)
(hTvol : MeasureTheory.volume T ≤ V)
(hE₀ : E₀ ≠ ⊤)
:
theorem
CKN.caccioppoli_assemble_four_terms
{αr βr A B G D L κ C₂₅ C₂₆ I₁ I₂ I₃ I₄ : ℝ}
(hαr : 0 ≤ αr)
(hβr : 0 ≤ βr)
(hA : 0 ≤ A)
(hB : 0 ≤ B)
(hG : 0 ≤ G)
(hD : 0 ≤ D)
(hL : 0 ≤ L)
(hκ : 0 < κ)
(hC₂₅ : 0 ≤ C₂₅)
(hC₂₆ : 0 ≤ C₂₆)
(hlower : (αr + βr) ^ 2 ≤ I₁ + I₂ + I₃ + I₄)
(hI₁_bound : I₁ ≤ (C₂₅ * κ * A) ^ 2)
(hI₂_bound : I₂ ≤ (C₂₅ * κ⁻¹ * A ^ (1 / 2) * B ^ (1 / 2) * G ^ (1 / 2)) ^ 2)
(hI₃_bound : I₃ ≤ (C₂₅ * κ⁻¹ * D * G ^ (1 / 2)) ^ 2)
(hI₄_bound : I₄ ≤ (C₂₆ * κ ^ (-1 / 2) * G ^ (1 / 2) * L ^ (1 / 2)) ^ 2)
:
The four Caccioppoli contributions assemble into the squared paper bound.
The four inequalities in hI are the interfaces for the four analytic
integral estimates, and hlower is the lower-bound step on the left side.
theorem
CKN.caccioppoli_raw_term_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₂₆ C_PS : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(hr : 0 < r)
(hscale : r ≤ ρ / 2)
(hεr : ε < r ^ 2)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hfuture : Set.Icc t₀ (t₀ + ε) ⊆ I)
(hC_PS : 0 ≤ C_PS)
(hC₁ : (32 + 3 * cutoffSecondDerivativeConstant) * 8000000 + 6 * cutoffGradientConstant * 5000000 ≤ C₂₅ ^ 2)
(hC₂ : C_PS * (1500 * cutoffGradientConstant + 900000) ≤ C₂₅ ^ 2)
(hC₃ : 3000 * cutoffGradientConstant + 1800000 ≤ C₂₅ ^ 2)
(hC₄ : 2000 * (4 * Real.pi / 3) ^ (1 / (q / (q - 1)) - 1 / 3) ≤ C₂₆ ^ 2)
{c : Foundation.Parabolic.ParabolicPoint → ℝ}
(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₀) ρ))
:
caccioppoliI1HeatCutoffRaw hρ hε ≤ (C₂₅ * (r / ρ) * alpha u (x₀, t₀) ρ) ^ 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 ∧ caccioppoliI3HeatCutoffRaw hρ hε ≤ (C₂₅ * (r / ρ)⁻¹ * delta p (x₀, t₀) ρ * gamma u (x₀, t₀) ρ ^ (1 / 2)) ^ 2 ∧ caccioppoliI4HeatCutoffRaw hρ hε ≤ (C₂₆ * (r / ρ) ^ (-1 / 2) * gamma u (x₀, t₀) ρ ^ (1 / 2) * lambda q f (x₀, t₀) ρ ^ (1 / 2)) ^ 2
theorem
CKN.caccioppoli_setIntegral_le_toReal_lintegral_abs
{S Q : Set Foundation.Parabolic.ParabolicPoint}
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hSQ : S ⊆ Q)
(hg : MeasureTheory.IntegrableOn g Q MeasureTheory.volume)
:
∫ (z : Foundation.Parabolic.ParabolicPoint) in S, g z ≤ (∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Q, ENNReal.ofReal |g z|).toReal