Weak limit passage on fixed Fourier tests #
A fixed real Fourier test is embedded in every sufficiently large cutoff. The finite product-space identities therefore pass to the synchronized weak product limits without changing their tests.
theorem
AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakLimitPassage.scalarProductTestLp_congr
{η : ℝ → ℝ}
{ψ χ : ↥ScalarTorusL2}
(hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure)
(hψ : ψ = χ)
:
theorem
AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakLimitPassage.gradientProductTestLp_congr
{η : ℝ → ℝ}
{g h : ↥SpatialGradientL2}
(hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure)
(hg : g = h)
:
theorem
AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakLimitPassage.strictMono_nat_id_le
{σ : ℕ → ℕ}
(hσ : StrictMono σ)
(n : ℕ)
:
theorem
AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_fourier_test_weak_identity
(P : FrozenDriftProblem)
(M : ℕ)
(d : Coefficients (RealFourierDimension M))
(η : ℝ → ℝ)
(hη : ContDiff ℝ 1 η)
(hη₁ : η 1 = 0)
(hηMem : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure)
(hηDerivMem : MeasureTheory.MemLp (deriv η) ⊤ GalerkinTimeMeasure)
(σ : ℕ → ℕ)
(hσ : StrictMono σ)
(Uprod : ↥ScalarProductTimeL2)
(Gprod : ↥GradientProductTimeL2)
(hUweak :
∀ (v : ↥ScalarProductTimeL2),
Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v)))
(hGweak :
∀ (v : ↥GradientProductTimeL2),
Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.gradientProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Gprod v)))
:
-inner ℝ Uprod (scalarProductTestLp (deriv η) ((realFourierScalarMap M) d) hηDerivMem) + inner ℝ Gprod (P.weightedDriftProductTestLp η M d hηMem) + P.κ * inner ℝ Gprod (gradientProductTestLp η ((realFourierGradientMap M) d) hηMem) = η 0 * inner ℝ P.initialTorusL2 ((realFourierScalarMap M) d)
The synchronized weak product limits satisfy the weak equation against every separated smooth time test and fixed finite real Fourier test.