Weak convergence of every positive-time slice

In prop:leray-limit the regularized velocities converge weakly in L² on every positive-time slice, tested against every global L² field. The local compactness step gives this on compact spatial sets; the uniform energy bound extends it to global tests, and the Hilbert pairing is then written as the coordinate dot-product integral.

theorem CKN.Leray.lerayLimit_everyTime_pairing_tendsto (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) (hFcont : ∀ (n : ℕ) (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => F n z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (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)) (A : ENNReal) (hA : A < ⊤) (hEnergy : ∀ (n : ℕ) (t : ℝ), 0 < 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 in prop:leray-limit: the local every-time weak convergence on compact spatial sets from the compactness step, the transfer of compact slice bounds to the limit, and the uniform slice energy bound give convergence of the coordinate pairings of every positive-time slice with every global L² field.