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.product_test_function {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Ω) (hθ : ContDiff ℝ (↑⊤) θ) (hθc : HasCompactSupport θ) (hθI : tsupport θ ⊆ I) : (fun (z : Foundation.Parabolic.Vec3 × ℝ) => η z.1 * θ z.2) ∈ spaceTimeTestFunction Ω I

theorem CKN.smooth_time_envelope {a b : ℝ} (hab : a < b) {I : Set ℝ} (ha : a ∈ I) (hb : b ∈ I) (hI : IsOpen I) (hconn : I.OrdConnected) : ∃ (θ : ℝ → ℝ), ContDiff ℝ (↑⊤) θ ∧ HasCompactSupport θ ∧ tsupport θ ⊆ I ∧ (∀ (t : ℝ), 0 ≤ θ t) ∧ ∀ t ∈ Set.Icc a b, θ t = 1

theorem CKN.vec3Ball_subset_euclideanBall {x : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : Foundation.Parabolic.vec3Ball x r ⊆ euclideanBall x r

theorem CKN.weighted_kernel_le {A : ℝ → ℝ} {b h S : ℝ} (hh : 0 < h) (hA : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (b - h) b), A s ≤ S) (hAint : MeasureTheory.Integrable A MeasureTheory.volume) : 0 ≤ S → ∫ (s : ℝ), A s * -deriv (backwardTimeCutoff b h) s ≤ S

theorem CKN.strip_error_tendsto {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {K : Set Foundation.Parabolic.Vec3} {b : ℝ} (hK : IsCompact K) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : Filter.Tendsto (fun (h : ℝ) => ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in K ×ˢ Set.Icc (b - h) (b + h), |g z|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem CKN.setIntegral_univ_Iio_probe {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {t : ℝ} (hg : MeasureTheory.IntegrableOn g (Set.univ ×ˢ Set.Iio t) MeasureTheory.volume) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Iio t, g z = ∫ (s : ℝ) in Set.Iio t, ∫ (x : Foundation.Parabolic.Vec3), g (x, s)

theorem CKN.cutoff_slice_le {Ω : Set Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {η : Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} {x₀ : Foundation.Parabolic.Vec3} {r R a b : ℝ} (hr : 0 < r) (hrr : r < R) (hη_nonneg : ∀ (x : Foundation.Parabolic.Vec3), 0 ≤ η x) (hη_le : ∀ (x : Foundation.Parabolic.Vec3), η x ≤ 1) : (∀ x ∈ Foundation.Parabolic.vec3Ball x₀ r, η x = 1) → ∀ (hη_support : tsupport η ⊆ euclideanBall x₀ R) (hηΩ : tsupport η ⊆ Ω) (hθ_one : ∀ s ∈ Set.Icc a b, θ s = 1) {S : ENNReal} (hSdef : S = 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 a b))) (hS : S ≠ ⊤) (hE : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.Vec3 × ℝ) => Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (η z.1 * θ z.2)) MeasureTheory.volume), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), ∫ (x : Foundation.Parabolic.Vec3) in Ω, Foundation.Parabolic.vec3EuclideanNorm (u (x, s)) ^ 2 * η x ≤ S.toReal