dot_affineShift

formal source

  87    simp [hv]
  88
  89/-- Weighted dot product along an affine shift. -/
  90theorem dot_affineShift {n : ℕ} (α t v : Vec n) (s : ℝ) :
  91    dot α (affineShift t v s) = dot α t + s * dot α v := by
  92  unfold dot affineShift
  93  calc
  94    ∑ i : Fin n, α i * (t i + s * v i)
  95        = ∑ i : Fin n, (α i * t i + s * (α i * v i)) := by
  96            apply Finset.sum_congr rfl
  97            intro i hi
  98            ring
  99    _ = (∑ i : Fin n, α i * t i) + s * ∑ i : Fin n, α i * v i := by
 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. -/