Weak convergence of every positive-time slice, with time-local energy bounds

In prop:forced-limit the forced regularized velocities converge weakly in L² on every positive-time slice, tested against every global L² field. As in prop:leray-limit, the local compactness step gives this on compact spatial sets and the energy bound extends it to global tests. The forced energy bound of lem:forced-energy-bounds is uniform only on bounded time intervals, and the forced regularized velocities are only measurable, so the energy and regularity inputs here are the time-local and measurable versions of those in CKN.Leray.lerayLimit_everyTime_pairing_tendsto.

theorem CKN.Leray.lerayLimit_everyTime_pairing_tendsto_of_local_energy (F : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (G : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hFmeas : ∀ (n : ℕ) (t : ℝ), 0 < t → Measurable fun (x : Foundation.Parabolic.Vec3) => F n (x, t)) (hv : Measurable v) (hGF : ∀ (n : ℕ) (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → G n (x, t) = F n (x, t)) (huv : ∀ (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → u (x, t) = v (x, t)) (hEnergy : ∀ (T : ℝ), 0 < T → ∃ A < ⊤, ∀ (n : ℕ) (t : ℝ), 0 < t → t ≤ T → ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (F n (x, t))‖ₑ ^ 2 ≤ A ^ 2) (hlocal : ∀ (t : ↑(Set.Ioi 0)) (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (G (σ k) (x, ↑t))) 2 (MeasureTheory.volume.restrict C)) (hl : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, ↑t))) 2 (MeasureTheory.volume.restrict C)), ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (G (σ k) (x, ↑t))) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, ↑t))) hl) w))) (hSliceBound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∀ (b₁ b₂ : ℝ), Set.Icc b₁ b₂ ⊆ Set.Ioi 0 → ∀ M < ⊤, (∀ (n : ℕ), ∀ t ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (G n (x, t))) ^ 2 ≤ M) → ∀ t ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (v (x, t))) ^ 2 ≤ M) (t : ℝ) : 0 < t → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, F (σ n) (x, t) i * w x i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))

Every-time weak convergence with time-local energy bounds, as used in prop:forced-limit: the local every-time weak convergence on compact spatial sets from the compactness step, the transfer of compact slice bounds to the limit, measurable positive-time slices, and a slice energy bound uniform on each bounded time interval give convergence of the coordinate pairings of every positive-time slice with every global L² field.

theorem CKN.Leray.forcedLerayLimit_slice_energy_local (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n) : (∀ (n : ℕ) (t : ℝ), Measurable fun (x : Foundation.Parabolic.Vec3) => forcedRegVelocity ρ a ha f hf (εseq n) (x, t)) ∧ ∀ (T : ℝ), 0 < T → ∃ A < ⊤, ∀ (n : ℕ) (t : ℝ), 0 < t → t ≤ T → ∫⁻ (x : Foundation.Parabolic.Vec3), ‖WithLp.toLp 2 (forcedRegVelocity ρ a ha f hf (εseq n) (x, t))‖ₑ ^ 2 ≤ A ^ 2

The forced regularized velocities have measurable positive-time slices and, on every bounded time interval, a slice energy bound uniform in ε, from lem:forced-energy-bounds.

theorem CKN.Leray.forcedLerayLimit_everyTimePairings (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (σ : ℕ → ℕ) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hv : Measurable v) (huv : ∀ (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → u (x, t) = v (x, t)) (hlocal : ∀ (t : ℝ), 0 < t → ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (forcedRegVelocity ρ a ha f hf (εseq (σ k)) (x, t))) 2 (MeasureTheory.volume.restrict C)) (hvC : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, t))) 2 (MeasureTheory.volume.restrict C)), ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (forcedRegVelocity ρ a ha f hf (εseq (σ k)) (x, t))) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, t))) hvC) w))) (hSliceBound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → ∀ (b₁ b₂ : ℝ), Set.Icc b₁ b₂ ⊆ Set.Ioi 0 → ∀ M < ⊤, (∀ (n : ℕ), ∀ t ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (forcedRegVelocity ρ a ha f hf (εseq n) (x, t))) ^ 2 ≤ M) → ∀ t ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (v (x, t))) ^ 2 ≤ M) (t : ℝ) : 0 < t → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedRegVelocity ρ a ha f hf (εseq (σ n)) (x, t) i * w x i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))

The every-time slice clause of prop:forced-limit: along the subsequence and limit of the forced local compactness theorem (forcedLerayLimit_local_compactness), the forced regularized velocities converge weakly in L² on every positive-time slice, tested against every global L² field.