See CvxLean.Tactic.DCP.Fns.LogSumExp.

theorem Vec.sum_exp_eq_sum_div {n : ℕ} (x : Fin n → ℝ) (t : ℝ) : Vec.sum (Vec.exp (x - Vec.const n t)) = Vec.sum (Vec.exp x) / t.exp

theorem Vec.sum_exp_pos {n : ℕ} (hn : 0 < n) (x : Fin n → ℝ) : 0 < Vec.sum (Vec.exp x)