Synchronized path and product-space limits

The pointwise weakly continuous representative, Bochner time-space limits, and product-space limits are extracted along one common subsequence of the concrete Galerkin family.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.exists_synchronized_weak_product_limit (P : FrozenDriftProblem) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (U : ↥ScalarTimeL2) (G : ↥GradientTimeL2) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2), (∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) ∧ (∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) ∧ (∀ (v : ↥ScalarTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (scalarTimeLp P (σ n)) v) Filter.atTop (nhds (inner ℝ U v))) ∧ (∀ (v : ↥GradientTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (gradientTimeLp P (σ n)) v) Filter.atTop (nhds (inner ℝ G v))) ∧ (∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) ∧ (∀ (v : ↥GradientProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.gradientProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Gprod v))) ∧ (∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ P.scalarBound) ∧ u ⟨0, ⋯⟩ = P.initialTorusL2 ∧ ‖U‖ ≤ P.scalarBound ∧ ‖G‖ ^ 2 ≤ P.gradientEnergyBound ∧ ‖Uprod‖ ≤ P.scalarBound ∧ ‖Gprod‖ ^ 2 ≤ P.gradientEnergyBound

One subsequence carries the pointwise weak path, the Bochner time-space limits, and the product-space scalar and gradient limits. The path retains its trace and all-times scalar bound.