Smooth periodic spatial tests from the real Fourier identities

The synchronized limit has a common full-measure set of times on which its weak spatial derivative identity holds for every real Fourier mode. This module begins the density bridge from those modes to the smooth periodic tests used by the solution predicate.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.testDensityBridgeMeasureSpaceUnitAddCircle : 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.testDensityBridgeMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.avInfraParabolicFourierGalerkinTestDensityBridgeIsFiniteMeasure1 : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.bridge_continuous_memL2 {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.bridge_pairing_error_bound {g v : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) (hv : Continuous v) : |∫ (x : Homogenization.Vec 2) in unitCube, g x * v x| ≤ √(l2NormSq g) * √(l2NormSq v)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.bridge_gradientCoord_continuous {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Parabolic.FourierGalerkin.bridge_continuous_integrable_cube {g : Homogenization.Vec 2 → ℝ} (hg : Continuous g) : MeasureTheory.IntegrableOn g unitCube MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.testFourierCutoff_l2_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (N : ℕ) : l2NormSq (Section5.testFourierCutoff f N) ≤ l2NormSq f

The real Fourier cutoff is an L² contraction on the cell. This bound supplies a time-uniform integrable majorant when the cutoff is applied slice by slice to a smooth spacetime test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.bridge_unitCube_measurable : MeasurableSet unitCube

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.bridge_gradientCoord_energy_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) : (l2NormSq fun (x : Homogenization.Vec 2) => spaceGrad f x i) ≤ gradNormSq (spaceGrad f)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.testFourierCutoff_gradient_pairing_tendsto {g ψ : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) (i : Fin 2) : Filter.Tendsto (fun (N : ℕ) => ∫ (x : Homogenization.Vec 2) in unitCube, g x * spaceGrad (Section5.testFourierCutoff ψ N) x i) Filter.atTop (nhds (∫ (x : Homogenization.Vec 2) in unitCube, g x * spaceGrad ψ x i))

The derivative part of the Fourier cutoff converges in every cell pairing against an arbitrary L² function.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.frequencyBall_pairFrequency_iff (N : ℕ) (k : Fin 2 → ℤ) : k ∈ Ergodic.frequencyBall N ↔ frequencyPair k ∈ symmetricFrequencyBox N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.frequencyPair_pairFrequency (p : ℤ × ℤ) : frequencyPair (pairFrequency p) = p

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.frequencyPair_injective {p q : Fin 2 → ℤ} (h : frequencyPair p = frequencyPair q) : p = q

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.testFourierCutoff_eq_realFourierProjection_ambient {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ 1 ψ) (hperiodic : IsZ2Periodic ψ) (N : ℕ) (x : Homogenization.Vec 2) : Section5.testFourierCutoff ψ N x = realFourierProjection N (Torus.periodicToTorus ψ) (Torus.toUnitTorus 2 x)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TestDensityBridge.realFourierModeFin_ambient_at (N : ℕ) (i : Fin (RealFourierDimension N)) (x : Homogenization.Vec 2) : realFourierModeFin N i (Torus.toUnitTorus 2 x) = realFourierModeAmbient N ((realFourierIndexEquivFin N).symm i) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.testFourierCutoff_ambientExpansion {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) (N : ℕ) : ∃ (c : Coefficients (RealFourierDimension N)), ∀ (x : Homogenization.Vec 2), Section5.testFourierCutoff ψ N x = ∑ i : Fin (RealFourierDimension N), c.ofLp i * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm i) x

The spatial Fourier cutoff is exactly a finite real Fourier expansion, including its ambient periodic representative.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.testFourierCutoff_ambientExpansion_coeff {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) (N : ℕ) (x : Homogenization.Vec 2) : Section5.testFourierCutoff ψ N x = ∑ i : Fin (RealFourierDimension N), (modeProjectionCoefficients (RealFourierDimension N) (realFourierModeFin N) (Torus.periodicToTorus ψ)).ofLp i * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm i) x

The ambient finite expansion uses the canonical torus projection coefficients. This makes its time-dependent coefficients explicit when the cutoff is applied to a spacetime test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.cellWeakDerivative_of_realFourierModes {u Du : Homogenization.Vec 2 → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict unitCube)) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict unitCube)) (i : Fin 2) (hmode : ∀ (N : ℕ) (j : Fin (RealFourierDimension N)), ∫ (x : Homogenization.Vec 2) in unitCube, u x * spaceGrad (realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j)) x i = -∫ (x : Homogenization.Vec 2) in unitCube, Du x * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : ∫ (x : Homogenization.Vec 2) in unitCube, u x * spaceGrad ψ x i = -∫ (x : Homogenization.Vec 2) in unitCube, Du x * ψ x

A common Fourier-mode weak-derivative identity extends to every smooth periodic spatial test. The cutoff is the actual finite Fourier polynomial, and convergence is in the exact value and derivative cell pairings needed for integration by parts.