dot_log_hadamardInv

formal source

 107          simp [Finset.sum_sub_distrib]
 108
 109/-- Log-aggregate of a componentwise inverse. -/
 110theorem dot_log_hadamardInv {n : ℕ} (α x : Vec n) :
 111    dot α (logVec (hadamardInv x)) = - dot α (logVec x) := by
 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. -/
 127theorem JcostN_reciprocal {n : ℕ} (α x : Vec n) :
 128    JcostN α (hadamardInv x) = JcostN α x := by
 129  rw [JcostN_eq_cosh_logsum, JcostN_eq_cosh_logsum]
 130  rw [dot_log_hadamardInv, Real.cosh_neg]
 131
 132/-- Zero-cost characterization in log coordinates. -/
 133theorem JcostN_eq_zero_iff {n : ℕ} (α x : Vec n) :
 134    JcostN α x = 0 ↔ dot α (logVec x) = 0 := by
 135  unfold JcostN JlogN
 136  simpa [Jlog] using (Jlog_eq_zero_iff (t := dot α (logVec x)))
 137
 138end Ndim
 139end Cost
 140end IndisputableMonolith