decodeGalerkin2D

formal source

 230
 231This is a left-inverse of `encodeGalerkin2D` only up to the coarse quantization used by `coeffMag`.
 232-/
 233noncomputable def decodeGalerkin2D {N : ℕ} (field : LNALField)
 234    (hsize : field.size = Fintype.card ((modes N) × Fin 2)) : GalerkinState N :=
 235  WithLp.toLp 2 (fun i : ((modes N) × Fin 2) =>
 236    let j : Fin (Fintype.card ((modes N) × Fin 2)) := (Fintype.equivFin ((modes N) × Fin 2)) i
 237    decodeCoeff (field[(Fin.cast hsize.symm j)]))
 238
 239/-- Hypothesis: one LNAL spatial step simulates one discrete Galerkin step (exactly). -/
 240structure SimulationHypothesis (N : ℕ) where
 241  /-- The LNAL program used for the simulation. -/
 242  P : LProgram
 243  /-- The discrete (time-stepping) map on Galerkin states. -/
 244  step : GalerkinState N → GalerkinState N
 245  /-- One-step commutation: execute then encode = encode then step. -/
 246  comm :
 247      ∀ u : GalerkinState N,
 248        (independent.step P (encodeGalerkin2D u)) = encodeGalerkin2D (step u)
 249
 250/-- Trivial simulation: use the `LISTEN noop` LNAL program and take the discrete step as `id`. -/
 251@[simp] def SimulationHypothesis.trivial (N : ℕ) : SimulationHypothesis N :=
 252  { P := listenNoopProgram
 253    step := id
 254    comm := by
 255      intro u
 256      simp }
 257
 258/-- A concrete, nontrivial simulation instance: `FOLD 1` corresponds to `foldPlusOneStep`. -/
 259noncomputable def SimulationHypothesis.foldPlusOne (N : ℕ) : SimulationHypothesis N :=
 260  { P := foldPlusOneProgram
 261    step := foldPlusOneStep
 262    comm := by
 263      intro u