Physical weak equation for smooth Fourier cutoffs

The synchronized product-space identity is transferred to the Euclidean cell using the physical time-torus measure-preserving map and the selected scalar and gradient representatives.

@[instance_reducible]

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

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.limitWeakEquationProbabilityTime : MeasureTheory.IsProbabilityMeasure GalerkinTimeMeasure

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.limitWeakEquationCellMeasure : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)

Lebesgue measure restricted to the physical time-space unit cell.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.limitWeakEquationCellMeasure = MeasureTheory.volume.restrict AVenhance.timeCube

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.limitWeakEquationProductMeasure : MeasureTheory.Measure (ℝ × Torus)

Product of the Galerkin time measure and the normalized torus measure.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.limitWeakEquationProductMeasure = AVenhance.Infra.Parabolic.FourierGalerkin.GalerkinTimeMeasure.prod MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.integral_product_eq_physical_pullback {f : ℝ × Torus → ℝ} (hf : MeasureTheory.Integrable f limitWeakEquationProductMeasure) : ∫ (q : ℝ × Torus), f q ∂limitWeakEquationProductMeasure = ∫ (p : ℝ × Homogenization.Vec 2), f (physicalTimeTorusMap p) ∂limitWeakEquationCellMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.scalarFourierModeL2_eq_fin_ae_product (N : ℕ) (j : Fin (RealFourierDimension N)) : (fun (p : ℝ × Torus) => ↑↑(realFourierModeL2 N j) p.2) =ᵐ[limitWeakEquationProductMeasure] fun (p : ℝ × Torus) => realFourierModeFin N j p.2

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.gradientFourierModeL2_eq_fin_ae_product (N : ℕ) (j : Fin (RealFourierDimension N)) : (fun (p : ℝ × Torus) => ↑↑(realFourierModeGradL2 N j) p.2) =ᵐ[limitWeakEquationProductMeasure] fun (p : ℝ × Torus) => WithLp.toLp 2 (realFourierModeGradFin N j p.2)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.realFourierModeFin_at_cell (N : ℕ) (j : Fin (RealFourierDimension N)) {x : Homogenization.Vec 2} (hx : x ∈ unitCube) : realFourierModeFin N j (Torus.toUnitTorus 2 x) = realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.realFourierModeGradFin_at_cell (N : ℕ) (j : Fin (RealFourierDimension N)) {x : Homogenization.Vec 2} (hx : x ∈ unitCube) : realFourierModeGradFin N j (Torus.toUnitTorus 2 x) = realFourierModeAmbientGrad N ((realFourierIndexEquivFin N).symm j) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.LimitWeakEquation.spacetimeCutoff_spaceGrad_expansion {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (N : ℕ) (t : ℝ) : spaceGrad (Section5.testFourierCutoff (φ t) N) = fun (x : Homogenization.Vec 2) => ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j t • realFourierModeAmbientGrad N ((realFourierIndexEquivFin N).symm j) x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_fourierCutoff_cell_identity (P : FrozenDriftProblem) (σ : ℕ → ℕ) (hσ : StrictMono σ) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (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))) (S : Set ℝ) (hSmeas : MeasurableSet S) (hSae : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, t ∈ S) (_hS : ∀ t ∈ S, synchronizedScalarSliceGood Uprod u t) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (hterminal : ∀ (t : ℝ), 1 ≤ t → ∀ (x : Homogenization.Vec 2), φ t x = 0) (N : ℕ) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, -synchronizedScalarRepresentative Uprod u S p.1 p.2 * deriv (fun (s : ℝ) => Section5.testFourierCutoff (φ s) N p.2) p.1 + Homogenization.vecDot (P.b p.1 p.2) (synchronizedGradientRepresentative Gprod p.1 p.2) * Section5.testFourierCutoff (φ p.1) N p.2 + P.κ * Homogenization.vecDot (synchronizedGradientRepresentative Gprod p.1 p.2) (spaceGrad (Section5.testFourierCutoff (φ p.1) N) p.2) = ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j 0 * inner ℝ P.initialTorusL2 (realFourierModeL2 N j)

The product-limit equation gives the physical weak equation for every smooth spatial Fourier cutoff of a spacetime test.