Uniform Cauchy convergence of the scalar torus Galerkin paths.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinScalarPathError (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (E_F E_T : ℝ) (M : ℕ) : ℝ

The explicit cutoff error supplied by the nested-path energy estimate.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinScalarPathError_tendsto_zero (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (E_F E_T : ℝ) : Filter.Tendsto (fun (M : ℕ) => classicalGalerkinScalarPathError φ hφ κ hκ θ₀ hθ₀ E_F E_T M) Filter.atTop (nhds 0)

The explicit nested-path error tends to zero as the lower cutoff grows.

theorem AVenhance.Infra.Classical.classicalGalerkinScalarPath_cauchy (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) : CauchySeq fun (N : ℕ) => classicalGalerkinScalarPath φ hφ κ hκ F hF θ₀ hθ₀ N

The smooth Galerkin scalar paths are Cauchy uniformly in time in torus L².