sub_mem_Radical

formal source

  64            ring
  65    _ = 0 := by rw [hv]; ring
  66
  67theorem sub_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
  68    (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
  69    v - w ∈ Radical α := by
  70  simpa [sub_eq_add_neg] using
  71    add_mem_Radical α hv (smul_mem_Radical α (-1) hw)
  72
  73/-- The Hessian quadratic form vanishes exactly on the radical distribution. -/
  74theorem quadraticHessian_eq_zero_iff {n : ℕ} (α t v : Vec n) :
  75    quadraticHessian α t v = 0 ↔ v ∈ Radical α := by
  76  rw [quadraticHessian_eq]
  77  constructor
  78  · intro hq
  79    unfold Radical
  80    have hcosh : 0 < Real.cosh (dot α t) := by positivity
  81    have hsq : (dot α v) ^ 2 = 0 := by
  82      exact (mul_eq_zero.mp (by simpa using hq)).resolve_left hcosh.ne'
  83    have hdot : dot α v = 0 := sq_eq_zero_iff.mp hsq
  84    exact hdot
  85  · intro hv
  86    rw [mem_Radical_iff] at hv
  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