def
definition
modeTrunc
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 (û₁, û₂). -/
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-/
65
66/-- Squared wave number \( |k|^2 \) as a real number. -/
67noncomputable def kSq (k : Mode2) : ℝ :=