Euclidean representatives of the synchronized gradient limit

The product gradient determines a spatial torus L² section for almost every time. Pulling its coordinate representatives back to the Euclidean cover gives periodic gradients with the cellwise L² bounds.

@[instance_reducible]

noncomputable def gradientRepresentativeMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem gradientRepresentativeMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem gradientRepresentativeProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductGradientRepresentative.realFourierModeAmbient_contDiff_withTop (N : ℕ) (j : Fin (RealFourierDimension N)) : ContDiff ℝ (↑⊤) (realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductGradientRepresentative.measurable_toUnitTorus_frozen : Measurable (Torus.toUnitTorus 2)

def AVenhance.Infra.Parabolic.FourierGalerkin.physicalTimeTorusMap : ℝ × Homogenization.Vec 2 → ℝ × Torus

Pass from physical time-space to time times the torus, preserving time.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.physicalTimeTorusMap p = (p.1, AVenhance.Infra.Torus.toUnitTorus 2 p.2)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.measurePreserving_toUnitTorus_unitCube : MeasureTheory.MeasurePreserving (Torus.toUnitTorus 2) (MeasureTheory.volume.restrict unitCube) MeasureTheory.volume

The Euclidean-to-torus map preserves measure on the spatial cell.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.measurePreserving_physicalTimeTorusMap : MeasureTheory.MeasurePreserving physicalTimeTorusMap (MeasureTheory.volume.restrict timeCube) (GalerkinTimeMeasure.prod MeasureTheory.volume)

Pulling back a product-torus L² class to the spacetime cell preserves its coordinatewise L² bounds.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative (G : ↥GradientProductTimeL2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

The selected product-gradient representative, pulled back periodically to Euclidean space.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative G t x = (↑↑G (t, AVenhance.Infra.Torus.toUnitTorus 2 x)).ofLp

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative_periodic (G : ↥GradientProductTimeL2) (t : ℝ) : IsZ2Periodic (synchronizedGradientRepresentative G t)

The selected Euclidean gradient representative is periodic at every time.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative_coordinate_memL2On (G : ↥GradientProductTimeL2) (t : ℝ) (hsection : MeasureTheory.MemLp (fun (y : Torus) => ↑↑G (t, y)) 2 MeasureTheory.volume) (i : Fin 2) : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => synchronizedGradientRepresentative G t x i

A coordinate of the selected gradient representative is square-integrable on the open unit cell whenever the product section is an L² slice.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative_gradMemL2On_ae (G : ↥GradientProductTimeL2) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, Homogenization.GradMemL2On unitCube (synchronizedGradientRepresentative G t)

For almost every time, the synchronized Euclidean gradient has the coordinatewise L² bound on the cell.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative_memLp_timeCube (G : ↥GradientProductTimeL2) (i : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => synchronizedGradientRepresentative G p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)

Every coordinate of the Euclidean representative belongs to the exact space-time L² carrier.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_realFourier_derivative_ae (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (hPathWeak : ∀ (t : ↑(Set.Icc 0 1)) (v : ↥ScalarTorusL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ ((P.scalarPath (σ n)) t) v) Filter.atTop (nhds (inner ℝ (u t) v))) (hUweak : ∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) (hGweak : ∀ (v : ↥GradientProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.gradientProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Gprod v))) (hUcont : ∀ (v : ↥ScalarTorusL2), Continuous fun (t : ↑(Set.Icc 0 1)) => inner ℝ (u t) v) (hUbound : ∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ P.scalarBound) : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, ∀ (i : Fin 2) (N : ℕ) (j : Fin (RealFourierDimension N)), ∫ (x : Torus), inner ℝ (↑↑Gprod (t, x)) (↑↑((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 ⋯ ⋯)) x) = -inner ℝ (u (clampTimeToUnit t)) (smoothPeriodicTestL2 ⋯ ⋯)

The synchronized weak spatial derivative identities hold on one common full-measure set for every real Fourier mode and both coordinates. This is the countable Fourier criterion needed for the later periodic H¹ closure argument.