Mixed Fourier weak forms

The finite ODE is tested by a potentially different Fourier vector from its evolving trial vector. These identities retain that bilinear structure and give bounds with constants that do not depend on the cutoff.

@[instance_reducible]

noncomputable def bilinearFormsMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• bilinearFormsMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem bilinearFormsMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem bilinearFormsProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierDriftBilinearForm (N : ℕ) (drift : ℝ → Torus → Homogenization.Vec 2) (t : ℝ) (c d : Coefficients (RealFourierDimension N)) : ℝ

Spatial drift form with independent trial and test Fourier coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.BilinearForms.realFourierDriftBilinearForm_pointwise (N : ℕ) (b : Torus → Homogenization.Vec 2) (c d : Coefficients (RealFourierDimension N)) : (fun (x : Torus) => Homogenization.vecDot (b x) (∑ j : Fin (RealFourierDimension N), c.ofLp j • realFourierModeGradFin N j x) * modeExpansion (RealFourierDimension N) (realFourierModeFin N) d x) = fun (x : Torus) => ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), d.ofLp i * c.ofLp j * (Homogenization.vecDot (b x) (realFourierModeGradFin N j x) * realFourierModeFin N i x)

Pointwise expansion of the mixed drift integrand.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.BilinearForms.realFourierDriftBilinearForm_matrix (N : ℕ) (b : ℝ → Torus → Homogenization.Vec 2) (t : ℝ) (c d : Coefficients (RealFourierDimension N)) (hentries : ∀ (i j : Fin (RealFourierDimension N)), MeasureTheory.Integrable (fun (x : Torus) => Homogenization.vecDot (b t x) (realFourierModeGradFin N j x) * realFourierModeFin N i x) MeasureTheory.volume) : realFourierDriftBilinearForm N b t c d = ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), d.ofLp i * c.ofLp j * ∫ (x : Torus), Homogenization.vecDot (b t x) (realFourierModeGradFin N j x) * realFourierModeFin N i x

The mixed drift integral is the corresponding rectangular matrix sum.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.BilinearForms.realFourierGradientMap_inner_mixed (N : ℕ) (c d : Coefficients (RealFourierDimension N)) : inner ℝ ((realFourierGradientMap N) c) ((realFourierGradientMap N) d) = ∑ i : Fin (RealFourierDimension N), ∑ j : Fin (RealFourierDimension N), d.ofLp i * c.ofLp j * ∫ (x : Torus), vecDot (realFourierModeGradFin N j x) (realFourierModeGradFin N i x)

The gradient pairing of two finite real Fourier sums is their mixed gradient matrix sum.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.BilinearForms.matrixCoefficientCLM_inner_bilinear {n : ℕ} (A : Fin n → Fin n → ℝ) (c d : Coefficients n) : inner ℝ d ((matrixCoefficientCLM A) c) = ∑ i : Fin n, ∑ j : Fin n, d.ofLp i * c.ofLp j * A i j

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffWeakForm_bilinear_identity (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ t : ℝ) (c d : Coefficients (RealFourierDimension N)) (hentries : ∀ (i j : Fin (RealFourierDimension N)), MeasureTheory.Integrable (fun (x : Torus) => Homogenization.vecDot (Torus.periodicToTorus (b t) x) (realFourierModeGradFin N j x) * realFourierModeFin N i x) MeasureTheory.volume) : inner ℝ d ((matrixCoefficientCLM fun (i j : Fin (RealFourierDimension N)) => weakFormMatrixEntry (fun (s : ℝ) (x : Torus) => Torus.periodicToTorus (b s) x) κ (realFourierModeFin N) (realFourierModeGradFin N) t i j) c) = -realFourierDriftBilinearForm N (fun (s : ℝ) => Torus.periodicToTorus (b s)) t c d - κ * inner ℝ ((realFourierGradientMap N) c) ((realFourierGradientMap N) d)

The finite weak-form matrix tested against d equals the spatial mixed weak form.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffDriftBilinear_bound (N : ℕ) (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (c d : Coefficients (RealFourierDimension N)) : |realFourierDriftBilinearForm N (fun (s : ℝ) => Torus.periodicToTorus (b s)) t c d| ≤ positiveCutoffDriftConstant b hb_bdd * ‖(positiveCutoffGradientMap N) c‖ * ‖d‖

Mixed drift estimate, uniform in the real Fourier cutoff.