The weak limit of the time derivatives

If the time derivatives of an L²-convergent sequence are bounded in L², a subsequence of them converges weakly, and the limit is the weak time derivative of the limit of the sequence against every test pair for which the integration by parts identity holds along the sequence (prop:lps-local-strong).

theorem ESS.LPS.lps_weak_limit_time_derivative {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.ParabolicPoint} [MeasureTheory.SFinite μ] (Un Qn : ℕ → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (u : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hUn : ∀ (n : ℕ) (i : Fin 3), MeasureTheory.MemLp (Un n i) 2 μ) (hQn : ∀ (n : ℕ) (i : Fin 3), MeasureTheory.MemLp (Qn n i) 2 μ) (hu : ∀ (i : Fin 3), MeasureTheory.MemLp (u i) 2 μ) (hconv : ∀ (i : Fin 3), Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), (Un n i z - u i z) ^ 2 ∂μ) Filter.atTop (nhds 0)) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (n : ℕ) (i : Fin 3), ‖MeasureTheory.MemLp.toLp (Qn n i) ⋯‖ ≤ C) (P : (CKN.Foundation.Parabolic.ParabolicPoint → ℝ) → (CKN.Foundation.Parabolic.ParabolicPoint → ℝ) → Prop) (hP : ∀ (θ Dθ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), P θ Dθ → MeasureTheory.MemLp θ 2 μ ∧ MeasureTheory.MemLp Dθ 2 μ ∧ ∀ (n : ℕ) (i : Fin 3), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), Un n i z * Dθ z ∂μ = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), Qn n i z * θ z ∂μ) : ∃ (Dt : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (i : Fin 3), MeasureTheory.MemLp (Dt i) 2 μ) ∧ ∀ (i : Fin 3) (θ Dθ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), P θ Dθ → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), u i z * Dθ z ∂μ = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint), Dt i z * θ z ∂μ

A bounded sequence of triples of square integrable functions has a weakly convergent subsequence whose limit represents the time derivative of the limit of the sequence against every test pair for which the identity holds along the sequence.