Transfer of initial data to the unit torus

The datum is only assumed square-integrable on the open unit cube and need not be periodic. This module transports that representative to the quotient torus through its canonical Ioc representative, using the fact that the open and half-open cells agree almost everywhere.

@[instance_reducible]

noncomputable def frozenInitialMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem frozenInitialMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem frozenInitialProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.frozenInitialData_memLp_torus {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : Homogenization.MemL2On unitCube θ₀) : MeasureTheory.MemLp (Torus.periodicToTorus θ₀) 2 MeasureTheory.volume

A L² datum on the open unit square induces an L² datum on the quotient torus.