theorem
proved
tactic proof
dot_log_hadamardMul
show as:
view Lean formalization →
formal statement (Lean)
74theorem dot_log_hadamardMul {n : ℕ} (α x y : Vec n)
75 (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
76 dot α (logVec (hadamardMul x y)) = dot α (logVec x) + dot α (logVec y) := by
proof body
Tactic-mode proof.
77 unfold dot logVec hadamardMul
78 calc
79 ∑ i : Fin n, α i * Real.log (x i * y i)
80 = ∑ i : Fin n, α i * (Real.log (x i) + Real.log (y i)) := by
81 refine Finset.sum_congr rfl ?_
82 intro i hi
83 rw [Real.log_mul (show x i ≠ 0 from (hx i).ne') (show y i ≠ 0 from (hy i).ne')]
84 _ = ∑ i : Fin n, (α i * Real.log (x i) + α i * Real.log (y i)) := by
85 refine Finset.sum_congr rfl ?_
86 intro i hi
87 ring
88 _ = (∑ i : Fin n, α i * Real.log (x i)) + (∑ i : Fin n, α i * Real.log (y i)) := by
89 simpa using Finset.sum_add_distrib
90
91/-- Log-aggregate of a componentwise quotient. -/