All-order forced Galerkin estimates and classical-limit construction.

@[instance_reducible]

noncomputable def classicalExistenceMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalExistenceMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalExistenceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalExistenceProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Classical.classicalWordCommutatorCount (s : ℕ) : ℕ

The total number of component commutator terms across all derivative words of order at most s.

Equations

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

theorem AVenhance.Infra.Classical.classicalWordCommutatorCount_bounds_word (s : ℕ) (w : List (Fin 2)) (hw : w.length ≤ s) : 2 * (classicalWordCommutatorSplits w).length ≤ classicalWordCommutatorCount s

theorem AVenhance.Infra.Classical.GalerkinExistence.classicalListMapSum_mono {α : Type u_1} (L : List α) (f g : α → ℝ) (h : ∀ a ∈ L, f a ≤ g a) : (List.map f L).sum ≤ (List.map g L).sum

theorem AVenhance.Infra.Classical.GalerkinExistence.classicalWordDerivative_periodic_local (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.GalerkinExistence.classicalTransport_smooth_local (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.GalerkinExistence.classicalTransport_periodic_local (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.classicalWordResidualProjection_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (N s : ℕ) (w : List (Fin 2)) (hw : w.length ≤ s) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) {t BF BD Y : ℝ} (ht : t ∈ Set.Icc 0 1) (hBF : 0 ≤ BF) (hBD : 0 ≤ BD) (hY : 0 ≤ Y) (hFbound : ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (F t) x‖ ≤ BF) (hDbound : ∀ (v : List (Fin 2)), v.length ≤ s → ∀ (j : Fin 2) (x : Homogenization.Vec 2), ‖classicalWordDerivative v (fun (y : Homogenization.Vec 2) => streamVel φ t y j) x‖ ≤ BD) (hcoeff : ∀ (v : List (Fin 2)), v.length ≤ s → ‖(realFourierWordDerivativeMap N v) c‖ ≤ Y) : ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => classicalWordDerivative w (F t) x - classicalWordTransportCommutatorExpansion w (fun (x : Homogenization.Vec 2) => streamVel φ t x) (realFourierModeAmbientExpansion N c) x)‖ ≤ BF + ↑(classicalWordCommutatorCount s) * BD * Y

A single transformed forcing component is bounded by the physical source derivative plus the commutator multiplicity times the derivative-family state norm.

theorem AVenhance.Infra.Classical.classicalForcedGalerkinData_transformedForcing_eq_wordResidual (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (w : List (Fin 2)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : have D := classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N; D.transformedForcing (realFourierWordDerivativeMap N w) (ODE.extendCurve classicalForcedGalerkinData_transformedForcing_eq_wordResidual._proof_1 u) t = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => classicalWordDerivative w (F t) x - classicalWordTransportCommutatorExpansion w (fun (x : Homogenization.Vec 2) => streamVel φ t x) (realFourierModeAmbientExpansion N (ODE.extendCurve classicalForcedGalerkinData_transformedForcing_eq_wordResidual._proof_1 u t)) x)

The transformed source of a classical Galerkin path is the projected differentiated forcing minus the transport commutator.

theorem AVenhance.Infra.Classical.classicalForcedGalerkinDerivativeFamily_forcing_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 ℝ (↑⊤) θ₀) (N s : ℕ) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) {t : ℝ} (ht : t ∈ Set.Icc 0 1) {BF BD : ℝ} (hBF : 0 ≤ BF) (hBD : 0 ≤ BD) (hFbound : ∀ (w : List (Fin 2)), w.length ≤ s → ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (F t) x‖ ≤ BF) (hDbound : ∀ (w : List (Fin 2)), w.length ≤ s → ∀ (j : Fin 2) (x : Homogenization.Vec 2), ‖classicalWordDerivative w (fun (y : Homogenization.Vec 2) => streamVel φ t y j) x‖ ≤ BD) : have word := classicalDerivativeWordOfIndex; have V := energyFamilyPath fun (a : ClassicalDerivativeWordIndex s) => ForcedGalerkinData.mapPath (realFourierWordDerivativeMap N (word a)) u; have D := classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N; ‖(D.wordDerivativeFamilyData u word).forcing t‖ ≤ ↑(Fintype.card (ClassicalDerivativeWordIndex s)) * ↑(classicalWordCommutatorCount s) * BD * ‖ODE.extendCurve classicalForcedGalerkinData_transformedForcing_eq_wordResidual._proof_1 V t‖ + ↑(Fintype.card (ClassicalDerivativeWordIndex s)) * BF

The forcing in the finite product of all derivative equations has linear growth in the combined derivative state, with constants independent of the Fourier cutoff.

Initial bounds for derivative families.

theorem AVenhance.Infra.Classical.classicalForcedGalerkinDerivativeFamily_initial_norm_le (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (N s : ℕ) {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ (w : List (Fin 2)), w.length ≤ s → ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w θ₀ x‖ ≤ B) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) : ‖((classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).wordDerivativeFamilyData u fun (a : ClassicalDerivativeWordIndex s) => classicalDerivativeWordOfIndex a).initial‖ ≤ √↑(Fintype.card (ClassicalDerivativeWordIndex s)) * B

The initial state in a finite derivative family is uniformly bounded by the sup norms of the corresponding derivatives of the datum.

theorem AVenhance.Infra.Classical.classicalGalerkin_derivativeFamily_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, ‖ODE.extendCurve classicalForcedGalerkinData_transformedForcing_eq_wordResidual._proof_1 (energyFamilyPath fun (a : ClassicalDerivativeWordIndex s) => ForcedGalerkinData.mapPath (realFourierWordDerivativeMap N (classicalDerivativeWordOfIndex a)) (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N)) t‖ ≤ C

Every fixed finite order of the differentiated Galerkin solution is bounded uniformly over all frequency cutoffs and all times in [0,1].