  71  exact Jcost_nonneg (aggregate_pos α x)
  72
  73/-- Log-aggregate of a componentwise product. -/
  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
  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. -/
  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.