Equation-derived weak time moduli

Testing each larger-cutoff ODE by an embedded lower-cutoff Fourier vector yields a common one-half-Hölder modulus, with the uniform spatial gradient energy supplying the time Cauchy bound.

@[instance_reducible]

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

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.equationModulusTwoNeTop : Fact (2 ≠ ⊤)

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientEnergyBound (P : FrozenDriftProblem) : ℝ

The cutoff-uniform spacetime gradient energy bound for the Galerkin solutions.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.fourierPairing_modulus_of_cutoff_le (P : FrozenDriftProblem) {M N : ℕ} (hMN : M ≤ N) (c : Coefficients (RealFourierDimension M)) (t s : ↑(Set.Icc 0 1)) : |inner ℝ ((P.scalarPath N) t) ((realFourierScalarMap M) c) - inner ℝ ((P.scalarPath N) s) ((realFourierScalarMap M) c)| ≤ (positiveCutoffDriftConstant P.b ⋯ * ‖c‖ + P.κ * ‖(realFourierGradientMap M) c‖) * √(dist t s) * √P.gradientEnergyBound

Pairing with a fixed real Fourier vector has a uniform half-Hölder modulus for every Galerkin cutoff containing its support.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarPath_pairing_lipschitz (P : FrozenDriftProblem) (N : ℕ) (w : ↥ScalarTorusL2) (t s : ↑(Set.Icc 0 1)) : |inner ℝ ((P.scalarPath N) t) w - inner ℝ ((P.scalarPath N) s) w| ≤ (P.galerkinData N).coefficientBound * P.scalarBound * ‖w‖ * dist t s

Every fixed finite Galerkin scalar path is Lipschitz in time, with a constant determined by the finite ODE operator bound and the common scalar L² bound. This controls the finite initial cutoff exceptions for each fixed Fourier test.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.fourierPairing_modulus (P : FrozenDriftProblem) {w : ↥ScalarTorusL2} (hw : w ∈ realFourierSpan) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (t s : ↑(Set.Icc 0 1)), |inner ℝ ((P.scalarPath N) t) w - inner ℝ ((P.scalarPath N) s) w| ≤ C * √(dist t s)

Equation-derived half-Hölder moduli for every dense Fourier test, including the finitely many cutoffs below that test's support.