Spatial derivative tests for the synchronized Galerkin limit

The Galerkin gradients are weak derivatives on the torus. This module begins the corresponding closedness argument in the synchronized product-space limit.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.productWeakGradientMeasureSpace : 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.productWeakGradientOneLeTwo : Fact (1 ≤ 2)

def AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialVector (i : Fin 2) : ℝ →L[ℝ] SpatialVector

The spatial vector containing a scalar in coordinate i and zero in the other coordinate.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialVector i = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 2) => ℝ).symm ∘SL ContinuousLinearMap.single ℝ (fun (x : Fin 2) => ℝ) i

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialGradientL2 (i : Fin 2) : ↥ScalarTorusL2 →L[ℝ] ↥SpatialGradientL2

Embed a scalar torus L² function into one coordinate of the vector torus L² space.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialGradientL2 i = ContinuousLinearMap.compLpL 2 MeasureTheory.volume (AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialVector i)

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialVector_apply (i : Fin 2) (r : ℝ) : (scalarToSpatialVector i) r = WithLp.toLp 2 (Pi.single i r)

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarToSpatialGradientL2_apply (i : Fin 2) (f : ↥ScalarTorusL2) : (scalarToSpatialGradientL2 i) f = (scalarToSpatialVector i).compLp f

def AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradientClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradientClosedCell_compact : IsCompact productWeakGradientClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradient_cube_subset_closedCell : unitCube ⊆ productWeakGradientClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradient_unitCell_subset_closedCell : Torus.unitCell 2 ⊆ productWeakGradientClosedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradient_continuous_unitCell_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradient_realToComplex_periodic {f : Homogenization.Vec 2 → ℝ} (hperiodic : IsZ2Periodic f) : Torus.IsZdPeriodic (Torus.realToComplex f)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradient_integral_unitCube_coord_ibp {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hpf : IsZ2Periodic f) (hpg : IsZ2Periodic g) (i : Fin 2) : ∫ (x : Homogenization.Vec 2) in unitCube, f x * spaceGrad g x i = -∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad f x i * g x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.productWeakGradient_smooth_memL2On {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : Homogenization.MemL2On unitCube f

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productWeakGradient_coord_contDiff {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceGrad ψ x i

theorem AVenhance.Infra.Parabolic.FourierGalerkin.productWeakGradient_coord_periodic {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) (i : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => spaceGrad ψ x i

theorem AVenhance.Infra.Parabolic.FourierGalerkin.ProductWeakGradient.realFourierModeGradL2_coordinate_pairing (N : ℕ) (j : Fin (RealFourierDimension N)) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : inner ℝ (realFourierModeGradL2 N j) ((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) = -inner ℝ (realFourierModeL2 N j) (smoothPeriodicTestL2 ⋯ ⋯)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierGradientMap_coordinate_pairing (N : ℕ) (c : Coefficients (RealFourierDimension N)) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : inner ℝ ((realFourierGradientMap N) c) ((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) = -inner ℝ ((realFourierScalarMap N) c) (smoothPeriodicTestL2 ⋯ ⋯)

Finite real Fourier sums satisfy the coordinate distributional-gradient identity against any smooth periodic spatial test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.finite_gradient_coordinate_pairing (P : FrozenDriftProblem) (N : ℕ) (t : ℝ) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : inner ℝ (P.gradientTimeFunction N t) ((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) = -inner ℝ (P.scalarTimeFunction N t) (smoothPeriodicTestL2 ⋯ ⋯)

Every concrete finite Galerkin gradient is the spatial weak gradient of its scalar path when paired against a smooth periodic test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.finite_product_spatial_derivative_identity (P : FrozenDriftProblem) (N : ℕ) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : inner ℝ (P.gradientProductLp N) (gradientProductTestLp η ((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) hη) = -inner ℝ (P.scalarProductLp N) (scalarProductTestLp η (smoothPeriodicTestL2 ⋯ ⋯) hη)

The finite product-space Galerkin scalar and gradient representatives satisfy the spatial integration-by-parts identity for every separated bounded time test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_spatial_derivative_identity (P : FrozenDriftProblem) (σ : ℕ → ℕ) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (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))) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : inner ℝ Gprod (gradientProductTestLp η ((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) hη) = -inner ℝ Uprod (scalarProductTestLp η (smoothPeriodicTestL2 ⋯ ⋯) hη)

The synchronized product-space weak limits inherit the spatial distributional-gradient identity against every smooth periodic test and bounded time weight.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_path_spatial_derivative_identity (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))) (η : ℝ → ℝ) (hηMem : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (i : Fin 2) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hperiodic : IsZ2Periodic ψ) : inner ℝ Gprod (gradientProductTestLp η ((scalarToSpatialGradientL2 i) (smoothPeriodicTestL2 hψ hperiodic)) hηMem) = -∫ (t : ℝ), if ht : t ∈ Set.Icc 0 1 then η t * inner ℝ (u ⟨t, ht⟩) (smoothPeriodicTestL2 ⋯ ⋯) else 0 ∂GalerkinTimeMeasure

The synchronized gradient limit has the spatial distributional derivative pairing of the weakly continuous scalar path after the product scalar limit is identified.