theorem
proved
tactic proof
dot_log_hadamardInv
show as:
view Lean formalization →
formal statement (Lean)
110theorem dot_log_hadamardInv {n : ℕ} (α x : Vec n) :
111 dot α (logVec (hadamardInv x)) = - dot α (logVec x) := by
proof body
Tactic-mode proof.
112 unfold dot logVec hadamardInv
113 calc
114 ∑ i : Fin n, α i * Real.log ((x i)⁻¹)
115 = ∑ i : Fin n, α i * (-Real.log (x i)) := by
116 refine Finset.sum_congr rfl ?_
117 intro i hi
118 rw [Real.log_inv]
119 _ = ∑ i : Fin n, -(α i * Real.log (x i)) := by
120 refine Finset.sum_congr rfl ?_
121 intro i hi
122 ring
123 _ = - (∑ i : Fin n, α i * Real.log (x i)) := by
124 simp
125
126/-- Reciprocity under componentwise inversion. -/