  64-/
  65
  66/-- Squared wave number \( |k|^2 \) as a real number. -/
  67noncomputable def kSq (k : Mode2) : ℝ :=
  68  (k.1 : ℝ) ^ 2 + (k.2 : ℝ) ^ 2
  69
  70/-- Fourier Laplacian on coefficients: (Δ û)(k) = -|k|² û(k). -/
  71noncomputable def laplacianCoeff {N : ℕ} (u : GalerkinState N) : GalerkinState N :=
  72  WithLp.toLp 2 (fun kc => (-kSq ((kc.1 : Mode2))) * u kc)
  73
  74/-- Abstract Galerkin convection operator (projected nonlinearity).
  75
  76Later we will replace this with the explicit Fourier convolution + Leray projection. -/
  77def ConvectionOp (N : ℕ) : Type :=
  78  GalerkinState N → GalerkinState N → GalerkinState N
  79
  80/-- Discrete Navier–Stokes RHS: u' = νΔu - B(u,u). -/
  81noncomputable def galerkinNSRHS {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : GalerkinState N) :
  82    GalerkinState N :=
  83  (ν • laplacianCoeff u) - (B u u)
  84
  85/-!
  86## Energy functional and inviscid conservation
  87-/
  88
  89/-- Discrete kinetic energy: \(E(u)=\frac12 \|u\|^2\). -/
  90noncomputable def discreteEnergy {N : ℕ} (u : GalerkinState N) : ℝ :=
  91  (1 / 2 : ℝ) * ‖u‖ ^ 2
  92
  93/-- Algebraic hypothesis capturing the skew-symmetry of the Galerkin nonlinearity in L²:
  94\( \langle B(u,u), u \rangle = 0 \). -/
  95structure EnergySkewHypothesis {N : ℕ} (B : ConvectionOp N) : Prop where
  96  skew : ∀ u : GalerkinState N, ⟪B u u, u⟫_ℝ = 0
  97

papers checked against this theorem

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