Integrability of the drift pairing at the synchronized limit

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.solutionIntegrabilityMeasureSpace : 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.solutionIntegrabilityProbabilityCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.SolutionIntegrability.torusFrozenDriftVector (P : FrozenDriftProblem) : ℝ × Torus → SpatialVector

Periodic drift represented as a Euclidean-normed spatial vector on time times the torus.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.SolutionIntegrability.torusFrozenDriftVector P p = WithLp.toLp 2 (AVenhance.Infra.Torus.periodicToTorus (P.b p.1) p.2)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.SolutionIntegrability.torusFrozenDriftGradientPairing (P : FrozenDriftProblem) (G : ↥GradientProductTimeL2) : ℝ × Torus → ℝ

Pointwise pairing of the frozen drift with a product-space L² gradient.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.torusFrozenDriftGradientPairing_integrable (P : FrozenDriftProblem) (G : ↥GradientProductTimeL2) : MeasureTheory.Integrable (SolutionIntegrability.torusFrozenDriftGradientPairing P G) (GalerkinTimeMeasure.prod MeasureTheory.volume)

The drift paired with an arbitrary product-space L² gradient is integrable on time times the torus.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronizedGradient_driftPairing_integrable (P : FrozenDriftProblem) (G : ↥GradientProductTimeL2) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (P.b p.1 p.2) (synchronizedGradientRepresentative G p.1 p.2)) (MeasureTheory.volume.restrict timeCube)

Pulling the drift pairing back to the Euclidean cell preserves its integrability.