`encodeGalerkin2D`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
domain: ClassicalBridge
line: 86 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics on GitHub at line 86.

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

  83We use `Fintype.equivFin` to give a deterministic indexing of the finite coefficient set
  84`(modes N) × Fin 2`, then store one coefficient per voxel.
  85-/
  86noncomputable def encodeGalerkin2D {N : ℕ} (u : GalerkinState N) : LNALField :=
  87  let e : Fin (Fintype.card ((modes N) × Fin 2)) ≃ ((modes N) × Fin 2) :=
  88    (Fintype.equivFin ((modes N) × Fin 2)).symm
  89  Array.ofFn (fun j => encodeIndex u (e j))
  90
  91end Encoding
  92
  93end IndisputableMonolith.ClassicalBridge.Fluids

papers checked against this theorem

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