coeffAt
plain-language theorem explainer
coeffAt reads the j-component of velocity coefficient at wavevector k from a GalerkinState truncated at level N, returning zero for any k outside the finite set modes N. Workers on the Galerkin-to-Fourier embedding in 2D fluid models cite it when building the zero-extension map and its linearity properties. The definition executes a direct membership test on the Finset modes N followed by subtype projection or the constant zero.
Claim. Let $u$ be a Galerkin velocity field truncated at level $N$, let $k=(k_1,k_2)$ be a wavevector in $ℤ^2$, and let $j∈{0,1}$. Then coeffAt$(u,k,j)$ equals the corresponding entry of $u$ when $max(|k_1|,|k_2|)≤N$ and equals $0$ otherwise.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to an infinite Fourier coefficient state. GalerkinState $N$ is the Euclidean space $ℝ^{(modes N)×Fin 2}$ whose coordinates are the velocity coefficients on the truncated modes. Mode2 is the type $ℤ×ℤ$ of 2D Fourier wavevectors; modes $N$ is the explicit Finset of all pairs with $max(|k_1|,|k_2|)≤N$.
proof idea
The definition performs a case split on the proposition $k∈modes N$. When the test succeeds it casts $k$ to the subtype $(modes N)$ and indexes the EuclideanSpace coordinate $(k',j)$; otherwise it returns the scalar $0$. No external lemmas are applied.
why it matters
coeffAt is the primitive selector used to define extendByZero, the canonical embedding of a GalerkinState into FourierState2D. It is invoked inside the proofs of coeffAt_add, coeffAt_smul, extendByZero_laplacianCoeff and norm_extendByZero_le. The definition therefore supplies the first concrete step of the M5 continuum-limit pipeline that later replaces compactness hypotheses with explicit arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.