Common Fourier weak-derivative identities for the physical limit representative

The synchronized product limit gives a single full-measure set on which the scalar and gradient representatives satisfy the distributional derivative relation for every real Fourier mode.

@[instance_reducible]

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

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

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

def AVenhance.Infra.Parabolic.FourierGalerkin.ScalarFourierDerivative.scalarFourierDerivativeClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarFourierDerivative.scalarFourierDerivativeClosedCell_compact : IsCompact scalarFourierDerivativeClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarFourierDerivative.scalarFourierDerivative_cube_subset_closedCell : unitCube ⊆ scalarFourierDerivativeClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarFourierDerivative.scalarFourierDerivative_smooth_memL2On {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : Homogenization.MemL2On unitCube ψ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarFourierDerivative.smoothPeriodicTestL2_ae_periodicToTorus {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : (fun (y : Torus) => ↑↑(smoothPeriodicTestL2 hψ hperiodic) y) =ᵐ[MeasureTheory.volume] Torus.periodicToTorus ψ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronizedGradientRepresentative_pairing_eq_cell_integral (G : ↥GradientProductTimeL2) (t : ℝ) (hsection : MeasureTheory.MemLp (fun (y : Torus) => ↑↑G (t, y)) 2 MeasureTheory.volume) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : ∫ (y : Torus), inner ℝ (↑↑G (t, y)) (↑↑((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) y) = ∫ (x : Homogenization.Vec 2) in unitCube, synchronizedGradientRepresentative G t x i * ψ x

The torus gradient pairing against a smooth periodic scalar test is the cell pairing with the synchronized Euclidean representative.

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ScalarFourierDerivative.scalarFourierDerivative_clamp_eq {t : ℝ} (ht : t ∈ Set.Icc 0 1) : clampTimeToUnit t = ⟨t, ht⟩

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_cell_realFourier_derivative_ae (P : FrozenDriftProblem) (σ : ℕ → ℕ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (S : Set ℝ) (hS : ∀ t ∈ S, synchronizedScalarSliceGood Uprod u t) (hSae : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, t ∈ S) (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 : Homogenization.Vec 2) in unitCube, synchronizedScalarRepresentative Uprod u S t x * spaceGrad (realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j)) x i = -∫ (x : Homogenization.Vec 2) in unitCube, synchronizedGradientRepresentative Gprod t x i * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x

The physical scalar and gradient representatives obey all real Fourier weak-derivative tests on one common full-measure set of times.