Identifying product and weak-path scalar limits

The pointwise weakly continuous Galerkin limit and the product-space limit have the same pairings against separated time/spatial tests. The proof uses dominated convergence and the uniform scalar energy bound.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.productScalar_pairing_eq_path_integral (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (hPathWeak : ∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) (hUprodWeak : ∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) {η : ℝ → ℝ} (hηMem : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (ψ : ↥ScalarTorusL2) : inner ℝ Uprod (scalarProductTestLp η ψ hηMem) = ∫ (t : ℝ), if ht : t ∈ Set.Icc 0 1 then η t * inner ℝ (u ⟨t, ht⟩) ψ else 0 ∂GalerkinTimeMeasure

The synchronized product scalar limit pairs with a separated test as the time integral of the weakly continuous path pairing.