Pointwise weak-limit bounds and traces for Galerkin paths

These lemmas are the limit-identification half of the compactness step. They preserve the uniform-in-time energy bound, the initial trace, and scalar weak continuity once a pointwise weak subsequence has been extracted. They do not perform the extraction; the required uniform equicontinuity estimates still have to be supplied by the Galerkin equation.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.norm_le_of_inner_tendsto {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {xSeq : ℕ → E} {x : E} {M : ℝ} (hlim : ∀ (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (xSeq n) v) Filter.atTop (nhds (inner ℝ x v))) (hbound : ∀ (n : ℕ), ‖xSeq n‖ ≤ M) : ‖x‖ ≤ M

Weak convergence preserves a uniform norm bound in a real Hilbert space.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.pointwiseWeakLimit_preserves_weak_initial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {T : Type u_2} (t₀ : T) {uSeq : ℕ → T → E} {u : T → E} {u₀ : E} (hinit : ∀ (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (uSeq n t₀) v) Filter.atTop (nhds (inner ℝ u₀ v))) (hweak : ∀ (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (uSeq n t₀) v) Filter.atTop (nhds (inner ℝ (u t₀) v))) : u t₀ = u₀

A pointwise weak path limit inherits a weakly convergent sequence of initial traces.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.exists_subseq_inner_tendsto_of_norm_bounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] {xSeq : ℕ → E} {M : ℝ} (hbound : ∀ (n : ℕ), ‖xSeq n‖ ≤ M) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (x : E), (∀ (v : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (xSeq (φ n)) v) Filter.atTop (nhds (inner ℝ x v))) ∧ ‖x‖ ≤ M

A bounded sequence in a separable real Hilbert space has a weakly convergent subsequence.

This is the one-space extraction primitive for the parabolic compactness argument. The energy bound on the limit is included; applying it to a space-time graph carrier still requires that carrier's separability and completeness to be established.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.exists_subseq_inner_tendsto_pair_of_norm_bounded {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] [TopologicalSpace.SeparableSpace F] {uSeq : ℕ → E} {vSeq : ℕ → F} {M : ℝ} (hbound : ∀ (n : ℕ), ‖WithLp.toLp 2 (uSeq n, vSeq n)‖ ≤ M) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (u : E) (v : F), (∀ (w : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (uSeq (φ n)) w) Filter.atTop (nhds (inner ℝ u w))) ∧ (∀ (w : F), Filter.Tendsto (fun (n : ℕ) => inner ℝ (vSeq (φ n)) w) Filter.atTop (nhds (inner ℝ v w))) ∧ ‖WithLp.toLp 2 (u, v)‖ ≤ M

A single subsequence makes both components of a bounded product-Hilbert sequence converge weakly. This packages simultaneous extraction for the space-time solution and its gradient.