`Mode2`

definition

show as: view math explainer →

module: IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D
domain: ClassicalBridge
line: 34 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D on GitHub at line 34.

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

used by

formal source

  31-/
  32
  33/-- A 2D Fourier mode (k₁, k₂). -/
  34abbrev Mode2 : Type := ℤ × ℤ
  35
  36/-- Truncation predicate: max(|k₁|,|k₂|) ≤ N. -/
  37def modeTrunc (N : ℕ) (k : Mode2) : Prop :=
  38  max k.1.natAbs k.2.natAbs ≤ N
  39
  40/-- The finite set of truncated modes. -/
  41noncomputable def modes (N : ℕ) : Finset Mode2 :=
  42  ((Finset.Icc (-((N : ℤ))) (N : ℤ)).product (Finset.Icc (-((N : ℤ))) (N : ℤ)))
  43
  44lemma mem_modes_iff {N : ℕ} {k : Mode2} :
  45    k ∈ modes N ↔ k.1 ∈ Finset.Icc (-((N : ℤ))) (N : ℤ) ∧ k.2 ∈ Finset.Icc (-((N : ℤ))) (N : ℤ) := by
  46  simp [modes, and_left_comm, and_assoc, and_comm]
  47
  48/-!
  49## Galerkin state space
  50-/
  51
  52-- We use Euclidean (L²) norms/inner products for energy identities, so we model coefficients
  53-- in `EuclideanSpace`, not plain Pi types (which carry the sup norm).
  54
  55/-- Velocity Fourier coefficient at a mode: a Euclidean real 2-vector (û₁, û₂). -/
  56abbrev VelCoeff : Type := EuclideanSpace ℝ (Fin 2)
  57
  58/-- The Galerkin state: velocity coefficients for each truncated mode and each component. -/
  59abbrev GalerkinState (N : ℕ) : Type :=
  60  EuclideanSpace ℝ ((modes N) × Fin 2)
  61
  62/-!
  63## Discrete dynamics
  64-/

papers checked against this theorem

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