Product-space identities for time-dependent Fourier cutoffs

The modewise weak identities are first regrouped as product-space integrals. This keeps the bounded drift and the vector gradient in their natural Hilbert spaces before the physical-cell representatives are substituted.

@[instance_reducible]

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

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

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

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.cutoffProductMeasure : MeasureTheory.Measure (ℝ × Torus)

Product time-torus measure used for the time-dependent cutoff pairing.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.cutoffProductMeasure = AVenhance.Infra.Parabolic.FourierGalerkin.GalerkinTimeMeasure.prod MeasureTheory.volume

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.cutoffProductUnitCoefficient (N : ℕ) (j : Fin (RealFourierDimension N)) : Coefficients (RealFourierDimension N)

Single unit coefficient selecting a real Fourier mode.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.cutoffProductUnitCoefficient N j = WithLp.toLp 2 (Pi.single j 1)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.cutoffProductModeExpansion_unit (N : ℕ) (j : Fin (RealFourierDimension N)) (x : Torus) : modeExpansion (RealFourierDimension N) (realFourierModeFin N) (cutoffProductUnitCoefficient N j) x = realFourierModeFin N j x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.scalarProductTestLp_inner_integral_mode (U : ↥ScalarProductTimeL2) (N : ℕ) (j : Fin (RealFourierDimension N)) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) : MeasureTheory.Integrable (fun (p : ℝ × Torus) => ↑↑U p * (η p.1 * ↑↑(realFourierModeL2 N j) p.2)) cutoffProductMeasure ∧ inner ℝ U (scalarProductTestLp η (realFourierModeL2 N j) hη) = ∫ (p : ℝ × Torus), ↑↑U p * (η p.1 * ↑↑(realFourierModeL2 N j) p.2) ∂cutoffProductMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.gradientProductTestLp_inner_integral_mode (G : ↥GradientProductTimeL2) (N : ℕ) (j : Fin (RealFourierDimension N)) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) : MeasureTheory.Integrable (fun (p : ℝ × Torus) => inner ℝ (↑↑G p) (η p.1 • ↑↑(realFourierModeGradL2 N j) p.2)) cutoffProductMeasure ∧ inner ℝ G (gradientProductTestLp η (realFourierModeGradL2 N j) hη) = ∫ (p : ℝ × Torus), inner ℝ (↑↑G p) (η p.1 • ↑↑(realFourierModeGradL2 N j) p.2) ∂cutoffProductMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentCutoffProduct.weightedDriftProductTestLp_inner_integral_mode (P : FrozenDriftProblem) (G : ↥GradientProductTimeL2) (N : ℕ) (j : Fin (RealFourierDimension N)) (η : ℝ → ℝ) (hη : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) : MeasureTheory.Integrable (fun (p : ℝ × Torus) => inner ℝ (↑↑G p) (P.weightedDriftProductTestFunction η N (cutoffProductUnitCoefficient N j) p)) cutoffProductMeasure ∧ inner ℝ G (P.weightedDriftProductTestLp η N (cutoffProductUnitCoefficient N j) hη) = ∫ (p : ℝ × Torus), inner ℝ (↑↑G p) (P.weightedDriftProductTestFunction η N (cutoffProductUnitCoefficient N j) p) ∂cutoffProductMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_spacetimeFourierCutoff_product_identity (P : FrozenDriftProblem) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (N : ℕ) (hidentity : -∑ j : Fin (RealFourierDimension N), inner ℝ Uprod (scalarProductTestLp (deriv (spacetimeRealFourierCoefficient φ N j)) (realFourierModeL2 N j) ⋯) + ∑ j : Fin (RealFourierDimension N), inner ℝ Gprod (P.weightedDriftProductTestLp (spacetimeRealFourierCoefficient φ N j) N (realFourierUnitCoefficient N j) ⋯) + P.κ * ∑ j : Fin (RealFourierDimension N), inner ℝ Gprod (gradientProductTestLp (spacetimeRealFourierCoefficient φ N j) (realFourierModeGradL2 N j) ⋯) = ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j 0 * inner ℝ P.initialTorusL2 (realFourierModeL2 N j)) : -∫ (p : ℝ × Torus), ↑↑Uprod p * ∑ j : Fin (RealFourierDimension N), deriv (spacetimeRealFourierCoefficient φ N j) p.1 * ↑↑(realFourierModeL2 N j) p.2 ∂TimeDependentCutoffProduct.cutoffProductMeasure + ∫ (p : ℝ × Torus), ∑ j : Fin (RealFourierDimension N), inner ℝ (↑↑Gprod p) ((spacetimeRealFourierCoefficient φ N j p.1 * modeExpansion (RealFourierDimension N) (realFourierModeFin N) (realFourierUnitCoefficient N j) p.2) • WithLp.toLp 2 (Torus.periodicToTorus (P.b p.1) p.2)) ∂TimeDependentCutoffProduct.cutoffProductMeasure + P.κ * ∫ (p : ℝ × Torus), ∑ j : Fin (RealFourierDimension N), inner ℝ (↑↑Gprod p) (spacetimeRealFourierCoefficient φ N j p.1 • ↑↑(realFourierModeGradL2 N j) p.2) ∂TimeDependentCutoffProduct.cutoffProductMeasure = ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j 0 * inner ℝ P.initialTorusL2 (realFourierModeL2 N j)

The three finite sums in the time-dependent mode identity are the product-space pairings against the value, drift-weighted value, and gradient of one finite Fourier cutoff.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.spacetimeFourierCutoff_product_integrable (P : FrozenDriftProblem) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (N : ℕ) : MeasureTheory.Integrable (fun (p : ℝ × Torus) => ↑↑Uprod p * ∑ j : Fin (RealFourierDimension N), deriv (spacetimeRealFourierCoefficient φ N j) p.1 * ↑↑(realFourierModeL2 N j) p.2) TimeDependentCutoffProduct.cutoffProductMeasure ∧ MeasureTheory.Integrable (fun (p : ℝ × Torus) => ∑ j : Fin (RealFourierDimension N), inner ℝ (↑↑Gprod p) ((spacetimeRealFourierCoefficient φ N j p.1 * realFourierModeFin N j p.2) • WithLp.toLp 2 (Torus.periodicToTorus (P.b p.1) p.2))) TimeDependentCutoffProduct.cutoffProductMeasure ∧ MeasureTheory.Integrable (fun (p : ℝ × Torus) => ∑ j : Fin (RealFourierDimension N), inner ℝ (↑↑Gprod p) (spacetimeRealFourierCoefficient φ N j p.1 • ↑↑(realFourierModeGradL2 N j) p.2)) TimeDependentCutoffProduct.cutoffProductMeasure

The three finite Fourier cutoff integrands are integrable on time times the torus.