mem_LevelSet_iff

formal source

  31@[simp] theorem mem_Radical_iff {n : ℕ} (α : Vec n) (v : Vec n) :
  32    v ∈ Radical α ↔ dot α v = 0 := Iff.rfl
  33
  34@[simp] theorem mem_LevelSet_iff {n : ℕ} (α : Vec n) (c : ℝ) (t : Vec n) :
  35    t ∈ LevelSet α c ↔ dot α t = c := Iff.rfl
  36
  37@[simp] theorem zero_mem_Radical {n : ℕ} (α : Vec n) :
  38    (fun _ => 0 : Vec n) ∈ Radical α := by
  39  unfold Radical dot
  40  simp
  41
  42theorem add_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
  43    (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
  44    v + w ∈ Radical α := by
  45  unfold Radical dot at hv hw ⊢
  46  have hv0 : ∑ i : Fin n, α i * v i = 0 := hv
  47  have hw0 : ∑ i : Fin n, α i * w i = 0 := hw
  48  calc
  49    ∑ i : Fin n, α i * (v i + w i)
  50        = (∑ i : Fin n, α i * v i) + ∑ i : Fin n, α i * w i := by
  51            simp [mul_add, Finset.sum_add_distrib]
  52    _ = 0 := by rw [hv0, hw0]; ring
  53
  54theorem smul_mem_Radical {n : ℕ} (α : Vec n) {v : Vec n} (s : ℝ)
  55    (hv : v ∈ Radical α) :
  56    s • v ∈ Radical α := by
  57  unfold Radical dot at hv ⊢
  58  calc
  59    ∑ i : Fin n, α i * (s * v i)
  60        = s * ∑ i : Fin n, α i * v i := by
  61            rw [Finset.mul_sum]
  62            apply Finset.sum_congr rfl
  63            intro i hi
  64            ring