weak-solution existence from the synchronized Galerkin limit

The synchronized scalar path and product-space limits assemble into the exact IsWeakSolutionGrad predicate. The slice derivative identities are upgraded to global Euclidean weak gradients by the periodization bridge, and the Fourier-cutoff weak equation is passed to all smooth spacetime tests.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.limitExistenceMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.limitExistenceMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.limitExistenceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.limitExistenceProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.exists_isWeakSolutionGrad (P : FrozenDriftProblem) : ∃ (θ : ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), IsWeakSolutionGrad P.b P.κ P.θ₀ θ Dθ

Every bounded measurable periodic drift and every L² datum have a weak solution in the exact author-IsWeakSolutionGrad class.