extendByZeroCLM

formal source

 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
 133
 134/-- Divergence-free predicate for a time-dependent Fourier trajectory. -/
 135def IsDivergenceFreeTraj (u : ℝ → FourierState2D) : Prop :=
 136  ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((u t) k) = 0
 137
 138lemma divConstraint_continuous (k : Mode2) : Continuous fun v : VelCoeff => divConstraint k v := by
 139  have h0 : Continuous fun v : VelCoeff => v (0 : Fin 2) := by
 140    simpa using
 141      (PiLp.continuous_apply (p := (2 : ENNReal)) (β := fun _ : Fin 2 => ℝ) (0 : Fin 2))
 142  have h1 : Continuous fun v : VelCoeff => v (1 : Fin 2) := by
 143    simpa using
 144      (PiLp.continuous_apply (p := (2 : ENNReal)) (β := fun _ : Fin 2 => ℝ) (1 : Fin 2))