Fourier coefficient equations for the finite classical Galerkin paths.
@[instance_reducible]
Use normalized Haar measure on the unit circle for periodic integrals.
Equations
- classicalSmoothEquationMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }
Instances For
theorem
AVenhance.Infra.Classical.classicalGalerkinFourierCoefficient_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 : ℕ)
(k : Fin 2 → ℤ)
{t : ℝ}
(ht : t ∈ Set.Ioo 0 1)
:
HasDerivAt
(fun (s : ℝ) =>
(classicalComplexFourierCoeffCLM k)
((Parabolic.FourierGalerkin.realFourierScalarMap N)
(ODE.extendCurve classicalGalerkinFourierCoefficient_hasDerivAt._proof_1
(classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) s)))
((classicalComplexFourierCoeffCLM k)
((Parabolic.FourierGalerkin.realFourierScalarMap N)
(((classicalForcedGalerkinData φ hφ κ hκ F hF θ₀ hθ₀ N).weak.coefficient t)
(ODE.extendCurve classicalGalerkinFourierCoefficient_hasDerivAt._proof_1
(classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t) + classicalForcingCoefficients N F t)))
t
A finite Galerkin Fourier coefficient has the derivative obtained by applying its coefficient functional to the finite ODE right-hand side.
theorem
AVenhance.Infra.Classical.GalerkinSmoothEquation.classicalSmoothModeLaplacian_contDiff
(u : Homogenization.Vec 2 → ℝ)
(hu : ContDiff ℝ (↑⊤) u)
:
ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceLap u x
theorem
AVenhance.Infra.Classical.GalerkinSmoothEquation.classicalSmoothModeTransport_contDiff
(b : Homogenization.Vec 2 → Homogenization.Vec 2)
(u : Homogenization.Vec 2 → ℝ)
(hb : ContDiff ℝ (↑⊤) b)
(hu : ContDiff ℝ (↑⊤) u)
:
ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b x) (spaceGrad u x)