Fourier coefficients of the smooth Galerkin representative and its time derivative.
@[instance_reducible]
Use normalized Haar measure on the unit circle for periodic integrals.
Equations
- classicalTimeEquationMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }
Instances For
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquation_smoothFourierCoeff_eq_torus
{f : Homogenization.Vec 2 → ℂ}
(hper : Torus.IsZdPeriodic f)
(hf : Continuous f)
(k : Fin 2 → ℤ)
:
UnitAddTorus.mFourierCoeff (⇑{ toFun := Torus.periodicToTorus f, continuous_toFun := ⋯ }) k = Torus.smoothFourierCoeff f k
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquation_realL2_smoothCoeff
(f : Homogenization.Vec 2 → ℝ)
(hf : Continuous f)
(hper : IsZ2Periodic f)
(k : Fin 2 → ℤ)
:
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquationWord_periodic
(w : List (Fin 2))
(f : Homogenization.Vec 2 → ℝ)
(hper : IsZ2Periodic f)
:
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquationSpaceLap_periodic
(u : Homogenization.Vec 2 → ℝ)
(hper : IsZ2Periodic u)
:
IsZ2Periodic (spaceLap u)
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquationTransport_contDiff
(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.GalerkinSmoothTimeEquation.classicalTimeEquationTransport_periodic
(b : Homogenization.Vec 2 → Homogenization.Vec 2)
(u : Homogenization.Vec 2 → ℝ)
(hb : IsZ2Periodic b)
(hu : IsZ2Periodic u)
:
theorem
AVenhance.Infra.Classical.classicalGalerkinFourierContinuousLimit_fourierCoeff
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
UnitAddTorus.mFourierCoeff (⇑(classicalGalerkinFourierContinuousLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)) k = (classicalGalerkinLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k) t
The Fourier coefficient of the continuous smooth representative is the coefficient path constructed as the strong Galerkin limit.
theorem
AVenhance.Infra.Classical.classicalGalerkinRealSmoothLift_smoothFourierCoeff
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
Torus.smoothFourierCoeff (Torus.realToComplex (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t))
k = (classicalGalerkinLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k) t
The Fourier coefficient of the real smooth representative agrees with its Galerkin limit coefficient, in the unit cell normalization used by the periodic calculus.
noncomputable def
AVenhance.Infra.Classical.classicalGalerkinRealSmoothDerivativeL2
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
(t : ↑(Set.Icc 0 1))
:
Each limiting spatial derivative path is the torus L² class of that derivative of the
smooth representative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Classical.classicalGalerkinWordScalarPathLimit_eq_smoothDerivative
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
(t : ↑(Set.Icc 0 1))
:
classicalRealToComplexTorusCLM ((classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) t) = classicalRealToComplexTorusCLM (classicalGalerkinRealSmoothDerivativeL2 φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w t)
theorem
AVenhance.Infra.Classical.classicalGalerkinFiniteTransportFourierCoeff_eq_sum
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
(N : ℕ)
(c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))
(k : Fin 2 → ℤ)
(t : ℝ)
:
UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(fun (y : Homogenization.Vec 2) =>
Homogenization.vecDot (streamVel φ t y) (spaceGrad (realFourierModeAmbientExpansion N c) y))
x))
k = ∑ j : Fin 2,
inner ℂ
(classicalRealToComplexTorusCLM
((Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N [j]) c)))
(classicalGalerkinTransportFourierTest φ hφ k j t)
The Fourier coefficient of a finite Galerkin transport term is the sum of the pairings of the finite derivative paths with the smooth transport tests.
theorem
AVenhance.Infra.Classical.classicalGalerkinSmoothLift_laplacianFourierCoeff_eq_sum
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus (spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)) x))
k = ∑ i : Fin 2,
(classicalComplexFourierCoeffCLM k)
(classicalGalerkinRealSmoothDerivativeL2 φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per [i, i] t)
The Laplacian coefficient of the smooth limit is the sum of the limiting second derivative coefficients.
theorem
AVenhance.Infra.Classical.classicalGalerkinSmoothLift_transportFourierCoeff_eq_sum
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(classicalTransport (streamVel φ ↑t) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t))
x))
k = ∑ j : Fin 2,
inner ℂ
(classicalRealToComplexTorusCLM
(classicalGalerkinRealSmoothDerivativeL2 φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per [j] t))
(classicalGalerkinTransportFourierTest φ hφ k j ↑t)
The smooth limit's transport coefficient is the sum of its gradient pairings with the Galerkin transport tests.
theorem
AVenhance.Infra.Classical.classicalGalerkinFiniteTransportFourierCoeff_tendsto
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
Filter.Tendsto
(fun (N : ℕ) =>
UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(classicalTransport (streamVel φ ↑t)
(realFourierModeAmbientExpansion N ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)))
x))
k)
Filter.atTop
(nhds
(UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(classicalTransport (streamVel φ ↑t) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t))
x))
k))
Finite Galerkin transport Fourier coefficients converge uniformly in time to those of the smooth representative.
theorem
AVenhance.Infra.Classical.classicalGalerkinFiniteLaplacianFourierCoeff_tendsto
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
Filter.Tendsto
(fun (N : ℕ) =>
UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(spaceLap
(realFourierModeAmbientExpansion N ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)))
x))
k)
Filter.atTop
(nhds
(UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus (spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)) x))
k))
Finite Galerkin Laplacian Fourier coefficients converge to those of the smooth representative.
theorem
AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePathLimit_eq_smoothRhsFourierCoeff
(φ : ℝ → 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 θ₀)
(t : ↑(Set.Icc 0 1))
(k : Fin 2 → ℤ)
:
(classicalGalerkinFiniteFourierDerivativePathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k) t = UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(fun (y : Homogenization.Vec 2) =>
F (↑t) y + (κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y - classicalTransport (streamVel φ ↑t)
(classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y))
x))
k
The limiting time derivative of each Fourier coefficient is the coefficient of the smooth spatial right-hand side. This is the coefficient-level passage from the Galerkin ODE to the limiting PDE.
def
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquationClamp
(s : ℝ)
:
↑(Set.Icc 0 1)
Clamp a real time to the interval on which the classical equation is constructed.
Equations
Instances For
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalTimeEquationClamp_eq_of_mem
{s : ℝ}
(hs : s ∈ Set.Ioo 0 1)
:
theorem
AVenhance.Infra.Classical.classicalGalerkinTimeEquationClamp_eq_of_mem
{s : ℝ}
(hs : s ∈ Set.Ioo 0 1)
:
The time clamp agrees with the identity on the open unit interval.
theorem
AVenhance.Infra.Classical.classicalGalerkinRealSmoothLift_fourierCoeff_hasDerivAt
(φ : ℝ → 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 θ₀)
(k : Fin 2 → ℤ)
{t : ℝ}
(ht : t ∈ Set.Ioo 0 1)
:
HasDerivAt
(fun (s : ℝ) =>
(classicalGalerkinLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k)
(GalerkinSmoothTimeEquation.classicalTimeEquationClamp s))
(UnitAddTorus.mFourierCoeff
(fun (x : Parabolic.FourierGalerkin.Torus) =>
↑(Torus.periodicToTorus
(fun (y : Homogenization.Vec 2) =>
F t y + (κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨t, ⋯⟩) y - classicalTransport (streamVel φ t)
(classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨t, ⋯⟩) y))
x))
k)
t
On interior times, the Fourier coefficient path of the smooth representative has derivative equal to the corresponding coefficient of its spatial right-hand side.
noncomputable def
AVenhance.Infra.Classical.classicalGalerkinWordFourierJointTerm
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
(k : Fin 2 → ℤ)
:
A single derivative Fourier mode, continuously parameterized by time and torus position.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalGalerkinWordFourierJointTerm_norm_le
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
(k : Fin 2 → ℤ)
:
‖classicalGalerkinWordFourierJointTerm φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w k‖ ≤ classicalGalerkinFourierCoefficientBound φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w.length * classicalScaledTorusFrequencyWeight k
noncomputable def
AVenhance.Infra.Classical.classicalGalerkinWordFourierContinuousPath
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
:
The ordered spatial derivative Fourier series converges uniformly on the time-space slab.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalGalerkinWordFourierJointTerm_summable
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
:
Summable (classicalGalerkinWordFourierJointTerm φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w)
theorem
AVenhance.Infra.Classical.GalerkinSmoothTimeEquation.classicalGalerkinWordFourierSeries_toLp
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
(t : ↑(Set.Icc 0 1))
:
(ContinuousMap.toLp 2 MeasureTheory.volume ℂ)
((classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry t) = classicalRealToComplexTorusCLM ((classicalGalerkinWordScalarPathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) t)
theorem
AVenhance.Infra.Classical.classicalGalerkinWordFourierContinuousPath_eq_smoothDerivative
(φ : ℝ → 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 θ₀)
(w : List (Fin 2))
(t : ↑(Set.Icc 0 1))
(x : Parabolic.FourierGalerkin.Torus)
:
(classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) (t, x) = ↑(classicalWordDerivative w (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)
(Torus.unitTorusRepresentative 2 x))
The jointly continuous word Fourier series is the spatial derivative of the smooth lift on each time slice.