Integrability estimates used by the local energy lower bound.
theorem
CKN.caccioppoli_gradient_integrable_on_cylinder
{Ω : 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₀ ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
:
MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du z)
(Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) MeasureTheory.volume
theorem
CKN.caccioppoli_u_sq_integrable_of_memLp
{B : Set Foundation.Parabolic.Vec3}
{v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict B))
:
MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (v x) ^ 2) B
MeasureTheory.volume
theorem
CKN.caccioppoli_gradient_sq_integrable_of_memLp
{B : Set Foundation.Parabolic.Vec3}
{v : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3}
(hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict B))
:
MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, v x i j ^ 2) B
MeasureTheory.volume