Auxiliary facts for concatenating Leray–Hopf solutions

Time splitting of almost-everywhere statements and slab integrals, and the continuity of the weak pairing of a strongly L²-continuous field (lem:lps-continuation).

theorem ESS.lps_Ioo_ae_eq_union {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : Set.Ioo a c =ᵐ[MeasureTheory.volume] Set.Ioo a b ∪ Set.Ioo b c

The open interval (a, c) is the union of (a, b) and (b, c) up to a null set.

theorem ESS.lps_ae_restrict_Ioo_union {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) {P : ℝ → Prop} (h1 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), P t) (h2 : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo b c), P t) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a c), P t

An almost-everywhere statement on two adjacent time intervals holds almost everywhere on their union.

theorem ESS.lps_slab_restrict_eq_add {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a c)) = MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)) + MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c))

The restrictions to the slabs (a, b) and (b, c) add up to the restriction to (a, c).

theorem ESS.lps_lintegral_slab_split {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) (f : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), f z = (∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), f z) + ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), f z

Lower integrals over adjacent slabs add.

theorem ESS.lps_memLp_two_of_lintegral_lt_top {E : Type} [NormedAddCommGroup E] {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.ParabolicPoint} {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint), ‖f z‖ₑ ^ 2 ∂μ < ⊤) : MeasureTheory.MemLp f 2 μ

A field with finite integral of the square of its norm and a.e. strongly measurable is square integrable.

theorem ESS.lps_pairing_continuousOn_of_l2 {α β : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hmem : ∀ t ∈ Set.Icc α β, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc α β, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) - u (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc α β)) (nhds 0)) {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) : ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i) (Set.Icc α β)

The weak pairing of a family that is strongly L²-continuous on an interval is continuous on it.

theorem ESS.lps_strong_energy_ennreal {s s' : ℝ} {W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DW : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pW : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hW : IsLpsStrongSolution s s' W DW pW) {t : ℝ} (ht : t ∈ Set.Icc s s') : (ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (W (x, t))) ^ 2) + ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ENNReal.ofReal (CKN.spatialGradientSq W DW z) = ENNReal.ofReal (1 / 2) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (W (x, s))) ^ 2

The energy equality of a strong solution between its initial time and any later time, in the extended-real form of the Leray–Hopf energy inequality (prop:lps-local-strong).

theorem ESS.lps_weak_pairing_test_hG {α s M : ℝ} (hαs : α ≤ s) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hweak : ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i) (Set.Icc α s)) (hM : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo α s), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume).toReal ≤ M) (δ : ℝ) : δ > 0 → ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo α s), s - η < t → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * φ (x, t) i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i * φ (x, s) i| < δ

Approximate continuity of the pairing with a test field at the right end of an interval, for a weakly continuous family with a uniform almost-everywhere L² bound.