coeffAt

formal source

  43-/
  44
  45/-- Read a single component coefficient at mode `k` (zero if `k ∉ modes N`). -/
  46noncomputable def coeffAt {N : ℕ} (u : GalerkinState N) (k : Mode2) (j : Fin 2) : ℝ :=
  47  if hk : k ∈ modes N then
  48    -- `k` as an element of the finite index type `(modes N)`
  49    let k' : (modes N) := ⟨k, hk⟩
  50    u (k', j)
  51  else
  52    0
  53
  54/-- Extend a truncated Galerkin state by zero to a full Fourier coefficient state. -/
  55noncomputable def extendByZero {N : ℕ} (u : GalerkinState N) : FourierState2D :=
  56  fun k =>
  57    -- Build a 2-vector coefficient from its two components.
  58    !₂[coeffAt u k ⟨0, by decide⟩, coeffAt u k ⟨1, by decide⟩]
  59
  60/-!
  61## Linearity of the zero-extension embedding
  62
  63We will eventually want to pass (linear) identities from Galerkin trajectories to limits.
  64For that, it is useful to record that `extendByZero` is a linear map.
  65-/
  66
  67lemma coeffAt_add {N : ℕ} (u v : GalerkinState N) (k : Mode2) (j : Fin 2) :
  68    coeffAt (u + v) k j = coeffAt u k j + coeffAt v k j := by
  69  classical
  70  by_cases hk : k ∈ modes N
  71  · simp [coeffAt, hk]
  72  · simp [coeffAt, hk]
  73
  74lemma coeffAt_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) (k : Mode2) (j : Fin 2) :
  75    coeffAt (c • u) k j = c * coeffAt u k j := by
  76  classical