extendByZero_smul

formal source

  85  ext j
  86  fin_cases j <;> simp [extendByZero, coeffAt_add]
  87
  88lemma extendByZero_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) :
  89    extendByZero (c • u) = c • (extendByZero u) := by
  90  classical
  91  funext k
  92  ext j
  93  fin_cases j <;> simp [extendByZero, coeffAt_smul]
  94
  95lemma extendByZero_neg {N : ℕ} (u : GalerkinState N) :
  96    extendByZero (-u) = -extendByZero u := by
  97  classical
  98  -- `-u = (-1) • u` and `extendByZero` is linear.
  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