affineShift_mem_LevelSet

formal source

 100          rw [Finset.sum_add_distrib, Finset.mul_sum]
 101
 102/-- Directions in the radical stay inside the affine leaves `dot α = c`. -/
 103theorem affineShift_mem_LevelSet {n : ℕ} (α : Vec n) {c s : ℝ} {t v : Vec n}
 104    (ht : t ∈ LevelSet α c) (hv : v ∈ Radical α) :
 105    affineShift t v s ∈ LevelSet α c := by
 106  rw [mem_LevelSet_iff] at ht ⊢
 107  have hv' : dot α v = 0 := hv
 108  rw [dot_affineShift, ht, hv']
 109  ring
 110
 111/-- The radical distribution is integrable: its integral leaves are the affine
 112hyperplanes `dot α = c`. -/
 113theorem radical_integrable_by_affine_leaves {n : ℕ} (α : Vec n) (c : ℝ) :
 114    ∀ ⦃t v : Vec n⦄, t ∈ LevelSet α c → v ∈ Radical α →
 115      ∀ s : ℝ, affineShift t v s ∈ LevelSet α c := by
 116  intro t v ht hv s
 117  exact affineShift_mem_LevelSet α ht hv
 118
 119/-- A constant direction preserves the affine leaf through `t` exactly when it
 120lies in the radical distribution. -/
 121theorem preserves_own_leaf_iff_mem_Radical {n : ℕ} (α t v : Vec n) :
 122    (∀ s : ℝ, affineShift t v s ∈ LevelSet α (dot α t)) ↔ v ∈ Radical α := by
 123  constructor
 124  · intro h
 125    have h1 := h 1
 126    rw [mem_LevelSet_iff, dot_affineShift] at h1
 127    unfold Radical
 128    have : dot α v = 0 := by linarith
 129    exact this
 130  · intro hv s
 131    exact affineShift_mem_LevelSet α (by simp [LevelSet]) hv
 132
 133end Ndim