The strong Galerkin limit retains the prescribed initial trace.

@[instance_reducible]

noncomputable def classicalSmoothInitialMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• classicalSmoothInitialMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem classicalSmoothInitialMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalSmoothInitialProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.GalerkinSmoothInitial.classicalGalerkinCoefficientPath_initial (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (N : ℕ) : (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) ⟨0, ⋯⟩ = (classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).initial

theorem AVenhance.Infra.Classical.classicalGalerkinWordScalarPathLimit_initial (φ : ℝ → 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 θ₀) : (classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per []) ⟨0, ⋯⟩ = MeasureTheory.MemLp.toLp (Torus.periodicToTorus θ₀) ⋯

At time zero, the Cauchy limit of the smooth Galerkin paths is the torus L² class of the initial datum.