extendByZeroLinear

formal source

  99  simpa [neg_one_smul] using (extendByZero_smul (N := N) (-1) u)
 100
 101/-- `extendByZero` packaged as a linear map. -/
 102noncomputable def extendByZeroLinear (N : ℕ) : GalerkinState N →ₗ[ℝ] FourierState2D :=
 103  { toFun := extendByZero
 104    map_add' := extendByZero_add (N := N)
 105    map_smul' := by
 106      intro c u
 107      -- `simp` expects `c • x`; our lemma is stated in that form.
 108      simpa using (extendByZero_smul (N := N) c u) }
 109
 110/-- `extendByZero` as a *continuous* linear map.
 111
 112This is available because `GalerkinState N` is finite-dimensional, hence every linear map out of it
 113is continuous. -/
 114noncomputable def extendByZeroCLM (N : ℕ) : GalerkinState N →L[ℝ] FourierState2D :=
 115  LinearMap.toContinuousLinearMap (extendByZeroLinear N)
 116
 117/-!
 118## Divergence-free structure (Fourier side) and limit stability
 119
 120A structural property we can pass to the limit using only modewise convergence is a closed,
 121linear constraint such as “divergence-free in Fourier variables”:
 122
 123`k₁ * û₁(t,k) + k₂ * û₂(t,k) = 0` for every mode `k`.
 124-/
 125
 126/-- Real Fourier-side divergence constraint for a single mode. -/
 127noncomputable def divConstraint (k : Mode2) (v : VelCoeff) : ℝ :=
 128  (k.1 : ℝ) * v (0 : Fin 2) + (k.2 : ℝ) * v (1 : Fin 2)
 129
 130/-- Fourier-side divergence-free predicate (modewise, at a fixed time). -/
 131def IsDivergenceFree (u : FourierState2D) : Prop :=
 132  ∀ k : Mode2, divConstraint k (u k) = 0