Positive-cutoff Galerkin paths for drift data

This module chooses the finite-dimensional ODE solution at every positive real Fourier cutoff and records the cutoff-independent scalar energy bound. The next compactness module consumes these paths together with the uniform gradient estimate.

@[instance_reducible]

noncomputable def sequenceMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem sequenceMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem sequenceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTorusMeasureSeparable : MeasureTheory.IsSeparable MeasureTheory.volume

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.scalarTorusL2SecondCountable : SecondCountableTopology ↥ScalarTorusL2

structure AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem : Type

The hypotheses needed to instantiate every positive real Fourier Galerkin system.

• b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

  Bounded measurable periodic drift of the frozen parabolic problem.

• drift_measurable : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => self.b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))
• drift_bounded : ∃ (B : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖self.b t x‖ ≤ B
• drift_periodic (t : ℝ) : t ∈ Set.Icc 0 1 → IsZ2Periodic (self.b t)
• κ : ℝ

  Positive diffusivity of the frozen parabolic problem.

• κ_pos : 0 < self.κ
• θ₀ : Homogenization.Vec 2 → ℝ

  Square-integrable periodic initial datum of the frozen parabolic problem.

• initial_memL2 : Homogenization.MemL2On unitCube self.θ₀

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.galerkinData (P : FrozenDriftProblem) (N : ℕ) : WeakFormGalerkinData (RealFourierDimension N) ↥SpatialGradientL2

The concrete finite weak-form ODE at cutoff N.

Equations

• P.galerkinData N = AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffGalerkinData N P.b ⋯ ⋯ ⋯ P.κ ⋯ P.θ₀ ⋯

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.coefficientPath (P : FrozenDriftProblem) (N : ℕ) : C(↑(Set.Icc 0 1), Coefficients (RealFourierDimension N))

A selected continuous coefficient path solving the finite Galerkin system.

Equations

• P.coefficientPath N = Classical.choose ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.coefficientPath_isSolution (P : FrozenDriftProblem) (N : ℕ) : (P.galerkinData N).ode.IsSolution (P.coefficientPath N)

The selected coefficient path is the unique finite ODE solution.

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarPath (P : FrozenDriftProblem) (N : ℕ) : C(↑(Set.Icc 0 1), ↥ScalarTorusL2)

The continuous scalar L² path represented by the finite real Fourier expansion.

Equations

• P.scalarPath N = { toFun := fun (t : ↑(Set.Icc 0 1)) => (AVenhance.Infra.Parabolic.FourierGalerkin.realFourierScalarMap N) ((P.coefficientPath N) t), continuous_toFun := ⋯ }

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initialTorusL2 (P : FrozenDriftProblem) : ↥ScalarTorusL2

The fixed torus L² representative of the initial datum.

Equations

• P.initialTorusL2 = MeasureTheory.MemLp.toLp (AVenhance.Infra.Torus.periodicToTorus P.θ₀) ⋯

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

A cutoff-independent upper bound for all scalar path norms.

Equations

• P.scalarBound = ‖P.initialTorusL2‖ * Real.exp (AVenhance.Infra.Parabolic.FourierGalerkin.positiveCutoffDriftConstant P.b ⋯ ^ 2 / P.κ)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarBound_nonneg (P : FrozenDriftProblem) : 0 ≤ P.scalarBound

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initialProjection_norm_le (P : FrozenDriftProblem) (N : ℕ) : ‖(P.galerkinData N).initial‖ ≤ ‖P.initialTorusL2‖

Fourier projection does not increase the L² norm of the datum.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.scalarPath_norm_le (P : FrozenDriftProblem) (N : ℕ) (t : ↑(Set.Icc 0 1)) : ‖(P.scalarPath N) t‖ ≤ P.scalarBound

Every positive-cutoff path obeys one common-in-time L² bound independent of its cutoff.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.gradientEnergy_le (P : FrozenDriftProblem) (N : ℕ) : ∫ (t : ℝ) in 0..1, ‖(P.galerkinData N).gradient (ODE.extendCurve gradientEnergy_le._proof_1 (P.coefficientPath N) t)‖ ^ 2 ≤ ‖P.initialTorusL2‖ ^ 2 * (1 + positiveCutoffDriftConstant P.b ⋯ ^ 2 / P.κ * Real.exp (positiveCutoffDriftConstant P.b ⋯ ^ 2 / P.κ)) / P.κ

Uniform space-time gradient energy for the positive-cutoff Galerkin paths.