Continuous L² tests for the transport part of the limiting Fourier ODE.

theorem classicalEquationLimitOneLeTwo : Fact (1 ≤ 2)

@[instance_reducible]

noncomputable def classicalEquationLimitMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalEquationLimitAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalEquationLimitProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.GalerkinSmoothEquationLimit.classicalEquationLimitDriftSlice_contDiff (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (t : ℝ) : ContDiff ℝ (↑⊤) (streamVel φ t)

noncomputable def AVenhance.Infra.Classical.classicalGalerkinTransportFourierTest (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (j : Fin 2) (t : ℝ) : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2

The complex L² test against which one component of the Galerkin gradient is paired in a Fourier coefficient of the transport term.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinTransportFourierTest_eq_periodicL2 (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (j : Fin 2) (t : ℝ) : classicalGalerkinTransportFourierTest φ hφ k j t = Torus.periodicToTorusL2 (fun (x : Homogenization.Vec 2) => Torus.torusCharacter k x * ↑(streamVel φ t x j)) ⋯

The transport test is the torus L² class of its explicit periodic representative.

theorem AVenhance.Infra.Classical.classicalGalerkinTransportFourierTest_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (j : Fin 2) (t B : ℝ) (hB : 0 ≤ B) (hb : ∀ (s : ℝ) (x : Homogenization.Vec 2), ‖streamVel φ s x‖ ≤ B) : ‖classicalGalerkinTransportFourierTest φ hφ k j t‖ ≤ B

A uniform bound for the transport test follows from the global velocity bound and unit modulus of the torus character.

theorem AVenhance.Infra.Classical.classicalGalerkinTransportFourierPairing_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (k : Fin 2 → ℤ) (j : Fin 2) (t B : ℝ) (hB : 0 ≤ B) (hb : ∀ (s : ℝ) (x : Homogenization.Vec 2), ‖streamVel φ s x‖ ≤ B) (u : ↥Parabolic.FourierGalerkin.ScalarTorusL2) : ‖inner ℂ (classicalRealToComplexTorusCLM u) (classicalGalerkinTransportFourierTest φ hφ k j t)‖ ≤ B * ‖u‖

Pairing a real L² path with the smooth transport test is bounded by the velocity bound.