aggregate_pos

formal source

  44noncomputable def JcostN {n : ℕ} (α x : Vec n) : ℝ :=
  45  JlogN α (logVec x)
  46
  47@[simp] theorem aggregate_pos {n : ℕ} (α x : Vec n) : 0 < aggregate α x := by
  48  unfold aggregate
  49  exact Real.exp_pos _
  50
  51@[simp] theorem JcostN_eq_Jcost_aggregate {n : ℕ} (α x : Vec n) :
  52    JcostN α x = Jcost (aggregate α x) := by
  53  rfl
  54
  55theorem JlogN_eq_cosh_sub_one {n : ℕ} (α t : Vec n) :
  56    JlogN α t = Real.cosh (dot α t) - 1 := by
  57  simpa [JlogN] using (Jcost_exp_cosh (dot α t))
  58
  59theorem JcostN_eq_cosh_logsum {n : ℕ} (α x : Vec n) :
  60    JcostN α x = Real.cosh (dot α (logVec x)) - 1 := by
  61  simpa [JcostN, JlogN] using (Jcost_exp_cosh (dot α (logVec x)))
  62
  63/-- Normalization at the identity vector. -/
  64theorem JcostN_unit {n : ℕ} (α : Vec n) :
  65    JcostN α (fun _ => 1) = 0 := by
  66  simp [JcostN, JlogN, dot, logVec, Jcost_unit0]
  67
  68/-- Non-negativity follows from scalar non-negativity at positive aggregate. -/
  69theorem JcostN_nonneg {n : ℕ} (α x : Vec n) : 0 ≤ JcostN α x := by
  70  rw [JcostN_eq_Jcost_aggregate]
  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