`FourierState2D`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
domain: ClassicalBridge
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  34-/
  35
  36/-- Full (infinite) Fourier coefficient state for a 2D velocity field on 𝕋². -/
  37abbrev FourierState2D : Type := Mode2 → VelCoeff
  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`). -/
  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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.