Uniform coefficient bounds for the residual-tail argument.

@[instance_reducible]

noncomputable def classicalResidualBoundsMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalResidualBoundsMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalResidualBoundsProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.classicalGalerkin_wordDerivative_coeff_uniform_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (s : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ), ∀ t ∈ Set.Icc 0 1, ∀ (w : List (Fin 2)), w.length ≤ s → ‖(realFourierWordDerivativeMap N w) (ODE.extendCurve classicalGalerkin_wordDerivative_coeff_uniform_bound._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)‖ ≤ C

The all-order derivative-family estimate bounds every fixed ordered derivative coefficient vector, uniformly in cutoff and time.

theorem AVenhance.Infra.Classical.GalerkinResidualBounds.classicalResidualTransport_smooth (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

theorem AVenhance.Infra.Classical.GalerkinResidualBounds.classicalResidualTransport_periodic (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : IsZ2Periodic b) (hu : IsZ2Periodic u) : IsZ2Periodic (classicalTransport b u)

theorem AVenhance.Infra.Classical.classicalGalerkinTransport_gradient_energy_uniform_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) : ∃ (E : ℝ), 0 ≤ E ∧ ∀ (N : ℕ), ∀ t ∈ Set.Icc 0 1, gradNormSq (spaceGrad (classicalTransport (streamVel φ t) (realFourierModeAmbientExpansion N (ODE.extendCurve classicalGalerkin_wordDerivative_coeff_uniform_bound._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)))) ≤ E

The transport term built from any forced Galerkin path has uniformly bounded spatial Dirichlet energy on [0,1].