Continuity of the finite smooth Galerkin operators on the physical time slab.

@[instance_reducible]

noncomputable def classicalSmoothCoefficientsMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalSmoothCoefficientsMeasureIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalSmoothCoefficientsProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalSmoothCoefficientsTorusProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficientClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficientClosedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficientCell_ae_eq_closedCell : Torus.unitCell 2 =ᵐ[MeasureTheory.volume] classicalCoefficientClosedCell

theorem AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficient_driftIntegral_eq_closedCell (φ : ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (t : ℝ) (i j : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : ∫ (x : Parabolic.FourierGalerkin.Torus), Parabolic.FourierGalerkin.vecDot (Torus.periodicToTorus (streamVel φ t) x) (Parabolic.FourierGalerkin.realFourierModeGradFin N j x) * Parabolic.FourierGalerkin.realFourierModeFin N i x = ∫ (x : Homogenization.Vec 2) in classicalCoefficientClosedCell, Homogenization.vecDot (streamVel φ t x) (Parabolic.FourierGalerkin.realFourierModeAmbientGrad N ((Parabolic.FourierGalerkin.realFourierIndexEquivFin N).symm j) x) * Parabolic.FourierGalerkin.realFourierModeAmbient N ((Parabolic.FourierGalerkin.realFourierIndexEquivFin N).symm i) x

theorem AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficient_drift_extension (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) : Continuous (Function.uncurry (streamVel φ))

theorem AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficient_entry_continuous (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (N : ℕ) (i j : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : Continuous fun (t : ℝ) => Parabolic.FourierGalerkin.weakFormMatrixEntry (fun (s : ℝ) (x : Parabolic.FourierGalerkin.Torus) => Torus.periodicToTorus (streamVel φ s) x) κ (Parabolic.FourierGalerkin.realFourierModeFin N) (Parabolic.FourierGalerkin.realFourierModeGradFin N) t i j

theorem AVenhance.Infra.Classical.GalerkinSmoothCoefficients.classicalCoefficient_matrix_continuous (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (N : ℕ) : Continuous fun (t : ℝ) => Parabolic.FourierGalerkin.matrixCoefficientCLM fun (i j : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) => Parabolic.FourierGalerkin.weakFormMatrixEntry (fun (s : ℝ) (x : Parabolic.FourierGalerkin.Torus) => Torus.periodicToTorus (streamVel φ s) x) κ (Parabolic.FourierGalerkin.realFourierModeFin N) (Parabolic.FourierGalerkin.realFourierModeGradFin N) t i j

theorem AVenhance.Infra.Classical.classicalForcedGalerkinCoefficient_continuousOn (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) : ContinuousOn (classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).weak.coefficient (Set.Icc 0 1)

The finite Galerkin operator in classicalForcedGalerkinData is continuous on [0,1]. This makes its integral ODE classically differentiable at interior times.

theorem AVenhance.Infra.Classical.classicalGalerkinCoefficientPath_hasDerivAt (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (ODE.extendCurve classicalGalerkinCoefficientPath_hasDerivAt._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N)) (((classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).weak.coefficient t) (ODE.extendCurve classicalGalerkinCoefficientPath_hasDerivAt._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t) + classicalForcingCoefficients N F t) t

Interior classical derivative of each forced Galerkin coefficient path.