coeffAt_add

formal source

  64For that, it is useful to record that `extendByZero` is a linear map.
  65-/
  66
  67lemma coeffAt_add {N : ℕ} (u v : GalerkinState N) (k : Mode2) (j : Fin 2) :
  68    coeffAt (u + v) k j = coeffAt u k j + coeffAt v k j := by
  69  classical
  70  by_cases hk : k ∈ modes N
  71  · simp [coeffAt, hk]
  72  · simp [coeffAt, hk]
  73
  74lemma coeffAt_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) (k : Mode2) (j : Fin 2) :
  75    coeffAt (c • u) k j = c * coeffAt u k j := by
  76  classical
  77  by_cases hk : k ∈ modes N
  78  · simp [coeffAt, hk]
  79  · simp [coeffAt, hk]
  80
  81lemma extendByZero_add {N : ℕ} (u v : GalerkinState N) :
  82    extendByZero (u + v) = extendByZero u + extendByZero v := by
  83  classical
  84  funext k
  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