abbrev
definition
def or abbrev
FourierState2D
show as:
view Lean formalization →
formal statement (Lean)
37abbrev FourierState2D : Type := Mode2 → VelCoeff
proof body
Definition body.
38
39/-!
40## Embedding: GalerkinState N → FourierState2D
41
42We extend a truncated state by zero outside the truncation window.
43-/
44
45/-- Read a single component coefficient at mode `k` (zero if `k ∉ modes N`). -/
used by (40)
-
continuum_limit_exists -
ConvergenceHypothesis -
ConvergenceHypothesis -
DuhamelKernelDominatedConvergenceAt -
duhamelKernelDominatedConvergenceAt_of_forcing -
duhamelKernelIntegral -
duhamelRemainderOfGalerkin -
extendByZero -
extendByZeroCLM -
extendByZeroLinear -
ForcingDominatedConvergenceAt -
ForcingDominatedConvergenceAt -
galerkinForcing -
GalerkinForcingDominatedConvergenceHypothesis -
IdentificationHypothesis -
IsDivergenceFree -
IsDivergenceFreeTraj -
IsNSDuhamelTraj -
IsStokesMildTraj -
IsStokesODETraj -
nsDuhamelCoeffBound -
nsDuhamelCoeffBound_galerkinKernel -
nsDuhamelCoeffBound_galerkinKernel_of_forcing -
nsDuhamelCoeffBound_kernelIntegral -
nsDuhamelCoeffBound_kernelIntegral_of_forcing -
nsDuhamel_of_forall -
nsDuhamel_of_forall_kernelIntegral -
nsDuhamel_of_forall_kernelIntegral_of_forcing -
of_convectionNormBound -
of_convectionNormBound_of_continuous