Theorem: Vec.sum_exp_eq_sum_div (CvxLean/Lib/Math/LogSumExp.lean)

State before:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ sum (exp (x - const n t)) = sum (exp x) / t.exp
Tactic:
unfold Vec.sum
State after:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = (Finset.univ.sum fun i => exp x i) / t.exp

State before:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = (Finset.univ.sum fun i => exp x i) / t.exp
Tactic:
rw [Finset.sum_div]
State after:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = Finset.univ.sum fun i => exp x i / t.exp

State before:
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (Finset.univ.sum fun i => exp (x - const n t) i) = Finset.univ.sum fun i => exp x i / t.exp
Tactic:
congr
State after:
case e_f
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (fun i => exp (x - const n t) i) = fun i => exp x i / t.exp

State before:
case e_f
n : ℕ
x : Fin n → ℝ
t : ℝ
⊢ (fun i => exp (x - const n t) i) = fun i => exp x i / t.exp
Tactic:
ext i
State after:
case e_f.h
n : ℕ
x : Fin n → ℝ
t : ℝ
i : Fin n
⊢ exp (x - const n t) i = exp x i / t.exp

State before:
case e_f.h
n : ℕ
x : Fin n → ℝ
t : ℝ
i : Fin n
⊢ exp (x - const n t) i = exp x i / t.exp
Tactic:
simp [Vec.exp, Vec.const, Real.exp_sub]
State after:
no goals