Strong convergence on a slab in prop:leray-limit

Local strong L² convergence on compact subsets of positive time, a uniform slice energy bound and uniform spatial tails give strong L² convergence on the whole slab ℝ³ × (0,T). The sequence is only assumed continuous at positive times; its measurable extension by zero agrees with it on the slab. The file also records the transfer of a slice energy bound to a local weak limit and the interpolation of Lᵖ membership between two exponents.

theorem CKN.Leray.lerayLimit_memLp_of_exponent_between {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p q r : ℝ} (hp : 0 < p) (hpq : p ≤ q) (hqr : q ≤ r) (hfp : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) (hfr : MeasureTheory.MemLp f (ENNReal.ofReal r) μ) : MeasureTheory.MemLp f (ENNReal.ofReal q) μ

Membership in Lᵖ and in Lʳ gives membership in L^q for every p ≤ q ≤ r.

theorem CKN.Leray.lerayLimit_limit_slice_le_of_compact_transfer (G : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : Measurable v) (M : ENNReal) (hM : M < ⊤) (t : ℝ) (ht : 0 < t) (hGslice : ∀ (n : ℕ), ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (G n (x, t))‖ₑ ^ 2 ≤ M) (hSliceBound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∀ (b₁ b₂ : ℝ), Set.Icc b₁ b₂ ⊆ Set.Ioi 0 → ∀ M < ⊤, (∀ (n : ℕ), ∀ s ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (G n (x, s))) ^ 2 ≤ M) → ∀ s ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (v (x, s))) ^ 2 ≤ M) : ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (v (x, t))‖ₑ ^ 2 ≤ M

A slice bound for a sequence at a positive time passes to its local weak limit, given the transfer of slice bounds on compact sets from the compactness step.

theorem CKN.Leray.lerayLimit_slab_strongL2_of_local_and_tails (T : ℝ) (hT : 0 < T) (F : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (G : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hFcont : ∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => F n z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hGF : ∀ (n : ℕ) (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → G n (x, t) = F n (x, t)) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : Measurable v) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (huv : ∀ (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → u (x, t) = v (x, t)) (hstrong : ∀ (Q : Set (Foundation.Parabolic.Vec3 × ℝ)), IsCompact Q → Q ⊆ Set.univ ×ˢ Set.Ioi 0 → Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm ((fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (G k z)) - fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (v z)) 2 (MeasureTheory.volume.restrict Q)) Filter.atTop (nhds 0)) (A : ENNReal) (hA : A < ⊤) (hFslice : ∀ (n : ℕ), ∀ t ∈ Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (F n (x, t))‖ₑ ^ 2 ≤ A ^ 2) (hvslice : ∀ t ∈ Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (v (x, t))‖ₑ ^ 2 ≤ A ^ 2) (htails : ∃ (S : ℕ → ENNReal), Filter.Tendsto S Filter.atTop (nhds 0) ∧ (∀ (m n : ℕ), ∀ t ∈ Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | 2 * (↑m + 1) < Foundation.Parabolic.vec3EuclideanNorm x}, ‖WithLp.toLp 2 (F n (x, t))‖ₑ ^ 2 ≤ S m) ∧ ∀ (m : ℕ), ∀ t ∈ Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | 2 * (↑m + 1) < Foundation.Parabolic.vec3EuclideanNorm x}, ‖WithLp.toLp 2 (v (x, t))‖ₑ ^ 2 ≤ S m) : have μ := MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)); (∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ) ∧ MeasureTheory.MemLp u 2 μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - u) 2 μ) Filter.atTop (nhds 0)

Strong L² convergence on the slab ℝ³ × (0,T) in prop:leray-limit. The sequence F n is continuous at positive times and agrees there with the sequence G n of the compactness step; G n → v strongly in L² on compact subsets of positive time; u = v at positive times; the slices of F n and of v are bounded by A² on (0,T); and their exterior slice energies beyond the radius 2(m+1) are bounded on (0,T) by one sequence S m → 0. Then F n and u are square integrable on the slab and F n → u in L².