LevelSet

formal source

  21  { v | dot α v = 0 }
  22
  23/-- The affine leaves orthogonal to the active direction. -/
  24def LevelSet {n : ℕ} (α : Vec n) (c : ℝ) : Set (Vec n) :=
  25  { t | dot α t = c }
  26
  27/-- Affine translation along a constant direction. -/
  28def affineShift {n : ℕ} (t v : Vec n) (s : ℝ) : Vec n :=
  29  fun i => t i + s * v i
  30
  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 : ℝ)