def
definition
encodeIndex
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics on GitHub at line 69.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
GalerkinState -
Mode2 -
modes -
LNALField -
LNALVoxel -
coeffMag -
coeffSign -
voxel -
sigma -
of -
one -
of -
one -
of -
of -
tau -
ell -
sigma -
one -
one
used by
formal source
66 if x < 0 then (-1) else 1
67
68/-- Encode a single Galerkin coefficient (at one Fourier mode and one component) into an LNAL voxel. -/
69noncomputable def encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) : LNALVoxel :=
70 let k : Mode2 := (i.1 : Mode2)
71 let x : ℝ := u i
72 let r6 : Reg6 :=
73 { nuPhi := coeffMag x
74 ell := k.1
75 sigma := coeffSign x
76 tau := k.2
77 kPerp := Int.ofNat i.2.val
78 phiE := decide (x < 0) }
79 (r6, Aux5.zero)
80
81/-- Encode an entire 2D Galerkin state into an `LNALField`.
82
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