Theta Upper Semicontinuity Alpha #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.theta_usc_timeSliceEnergy_bounded
{Ω : 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 r h₁ : ℝ}
(hR : 0 < R)
(hrrR : r < R)
(hh₁ : 0 < h₁)
(hh₁R : h₁ < R ^ 2)
(hsubAt :
∀ {h : ℝ}, 0 ≤ h → h ≤ h₁ → closure (Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + h) R) ⊆ spaceTimeSet Ω I)
(hIntAt :
∀ {h : ℝ},
0 < h →
h ≤ h₁ →
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z₀.2 - R ^ 2) (z₀.2 + h)), MeasureTheory.IntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2)
(Foundation.Parabolic.vec3Ball z₀.1 r) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2)
(Foundation.Parabolic.vec3Ball z₀.1 R) MeasureTheory.volume)
(hS0 :
essSup
(fun (x : ℝ) =>
Foundation.Parabolic.Integration.timeSliceBallEnergy z₀.1 R x fun (w : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (u w))
(MeasureTheory.volume.restrict (Set.Ioc (z₀.2 - R ^ 2) z₀.2)) ≠ ⊤)
:
Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin 0 (Set.Ioi 0)) fun (h : ℝ) =>
(essSup
(fun (s : ℝ) =>
ENNReal.ofReal
(∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z₀.1 r, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2))
(MeasureTheory.volume.restrict (Set.Ioc (z₀.2 - R ^ 2) (z₀.2 + h)))).toReal
The time-slice energy restricted to the ball of radius r stays bounded
above near the base point, uniformly along the one-sided time parameter used in
the Step 2 transfer argument.