theorem
proved
tactic proof
dot_log_hadamardDiv
show as:
view Lean formalization →
formal statement (Lean)
92theorem dot_log_hadamardDiv {n : ℕ} (α x y : Vec n)
93 (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
94 dot α (logVec (hadamardDiv x y)) = dot α (logVec x) - dot α (logVec y) := by
proof body
Tactic-mode proof.
95 unfold dot logVec hadamardDiv
96 calc
97 ∑ i : Fin n, α i * Real.log (x i / y i)
98 = ∑ i : Fin n, α i * (Real.log (x i) - Real.log (y i)) := by
99 refine Finset.sum_congr rfl ?_
100 intro i hi
101 rw [Real.log_div (show x i ≠ 0 from (hx i).ne') (show y i ≠ 0 from (hy i).ne')]
102 _ = ∑ i : Fin n, (α i * Real.log (x i) - α i * Real.log (y i)) := by
103 refine Finset.sum_congr rfl ?_
104 intro i hi
105 ring
106 _ = (∑ i : Fin n, α i * Real.log (x i)) - (∑ i : Fin n, α i * Real.log (y i)) := by
107 simp [Finset.sum_sub_distrib]
108
109/-- Log-aggregate of a componentwise inverse. -/