coeffAt
plain-language theorem explainer
The definition extracts the j-th velocity component from a truncated 2D Galerkin state at Fourier mode k, returning zero when k falls outside the finite truncation set modes N. Researchers formalizing the passage from Galerkin approximations to continuum Fourier states cite this selector when building the zero-extension map and its linearity properties. The definition proceeds by a direct membership test on the finite mode set followed by a subtype cast or the constant zero.
Claim. Let $u$ be a Galerkin state truncated at level $N$, let $k$ be a 2D Fourier mode, and let $j$ index a velocity component. The extracted coefficient equals the value of $u$ at the corresponding index when $k$ belongs to the truncated mode set, and equals zero otherwise.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to infinite Fourier coefficient states. A GalerkinState N is the Euclidean space of real coefficients indexed by the product of the finite mode set (modes N) and the two components Fin 2. Mode2 is the type of integer pairs (k1,k2), while modes N is the Finset of all such pairs with max(|k1|,|k2|) <= N.
proof idea
The definition performs a case split on membership of k in modes N. When the test succeeds it casts k to the subtype (modes N) and reads the corresponding entry from the Euclidean space u; otherwise it returns the real constant zero. No auxiliary lemmas are invoked beyond the membership predicate.
why it matters
This selector supplies the basic access function for the zero-extension embedding extendByZero, which feeds the linearity lemmas coeffAt_add and coeffAt_smul together with the norm bound norm_extendByZero_le. It therefore occupies the first concrete step in the M5 milestone that makes the Galerkin-to-continuum dependency graph explicit. The construction keeps truncation predicates visible so that later milestones can replace analytic hypotheses with proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.