The spatial L² gradient space for real Fourier cutoffs

This module places the explicitly differentiated real modes in the vector-valued torus L² space and packages their finite synthesis as a continuous linear map. The Euclidean norm on the two gradient coordinates is the PiLp 2 norm, matching the gradient energy.

@[instance_reducible]

noncomputable def gradientSpaceMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem gradientSpaceMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem gradientSpaceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.SpatialVector : Type

Euclidean two-vectors with their usual squared-sum norm.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.SpatialVector = PiLp 2 fun (x : Fin 2) => ℝ

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.SpatialGradientL2 : AddSubgroup (Torus →ₘ[MeasureTheory.volume] SpatialVector)

The Hilbert space of square-integrable spatial vector fields on the unit torus.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.SpatialGradientL2 = MeasureTheory.Lp AVenhance.Infra.Parabolic.FourierGalerkin.SpatialVector 2 MeasureTheory.volume

def AVenhance.Infra.Parabolic.FourierGalerkin.GradientSpace.closedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.GradientSpace.closedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.GradientSpace.isCompact_closedCell : IsCompact closedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.GradientSpace.unitTorusRepresentative_mem_closedCell (x : Torus) : Torus.unitTorusRepresentative 2 x ∈ closedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradFin_memLp (N : ℕ) (i : Fin (RealFourierDimension N)) : MeasureTheory.MemLp (fun (x : Torus) => WithLp.toLp 2 (realFourierModeGradFin N i x)) 2 MeasureTheory.volume

Every real Fourier gradient mode is an element of vector-valued spatial L².

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierModeGradL2 (N : ℕ) (i : Fin (RealFourierDimension N)) : ↥SpatialGradientL2

A real Fourier gradient mode, represented as an L² equivalence class.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap (N : ℕ) : Coefficients (RealFourierDimension N) →L[ℝ] ↥SpatialGradientL2

Finite synthesis of the vector-valued gradient modes.

Equations

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

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_apply (N : ℕ) (c : Coefficients (RealFourierDimension N)) : (realFourierGradientMap N) c = ∑ i : Fin (RealFourierDimension N), c.ofLp i • realFourierModeGradL2 N i