JlogN

formal source

  37  Real.exp (dot α (logVec x))
  38
  39/-- Log-coordinate `n`-dimensional cost. -/
  40noncomputable def JlogN {n : ℕ} (α t : Vec n) : ℝ :=
  41  Jcost (Real.exp (dot α t))
  42
  43/-- Original positive-coordinate `n`-dimensional cost. -/
  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]