Upper semicontinuity of the time-slice energy

The product-cutoff argument below uses the almost-every-time local energy inequality and the compactly supported smooth cutoffs from the setting layer.

theorem CKN.alpha_usc_of_sws {Ω : 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} {r R t₁ t₂ : ℝ} (hr : 0 < r) (hrr : r < R) (ht : t₁ < t₂) (hrect : euclideanClosedBall x₀ R ×ˢ Set.Icc t₁ t₂ ⊆ spaceTimeSet Ω I) : Filter.limsup (fun (h : ℝ) => (essSup (fun (s : ℝ) => ENNReal.ofReal (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 2)) (MeasureTheory.volume.restrict (Set.Ioc t₁ (t₂ + h)))).toReal) (nhdsWithin 0 (Set.Ioi 0)) ≤ (essSup (fun (x : ℝ) => Foundation.Parabolic.Integration.timeSliceBallEnergy x₀ R x fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) (MeasureTheory.volume.restrict (Set.Ioc t₁ t₂))).toReal

The right-sided essential-supremum bound for a suitable weak solution.

The spatial cutoff is one on the inner ball and supported in the outer ball; the time cutoff is one through the enlarged time interval. The two pieces of the time interval are then joined before taking the essential supremum.

theorem CKN.alpha_usc_of_local_energy_inequality {F ω : ℝ → ℝ} {S : ℝ} (hF_nonneg : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 ≤ F h) (hF_bounded : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin 0 (Set.Ioi 0)) F) (henergy : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), F h ≤ S + ω h) (hω : Filter.Tendsto ω (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : Filter.limsup F (nhdsWithin 0 (Set.Ioi 0)) ≤ S

Conditional form of lem:alpha-usc.

F h is the inner-ball time-slice essential supremum on the enlarged time interval, S is the outer-ball essential supremum before the endpoint, and henergy is the estimate obtained from the a.e.-time local energy inequality and a product cutoff. The conclusion is the paper's right-sided limsup bound.