logVec

formal source

  21def dot {n : ℕ} (α t : Vec n) : ℝ := ∑ i : Fin n, α i * t i
  22
  23/-- Componentwise logarithm. -/
  24noncomputable def logVec {n : ℕ} (x : Vec n) : Vec n := fun i => Real.log (x i)
  25
  26/-- Componentwise multiplication. -/
  27def hadamardMul {n : ℕ} (x y : Vec n) : Vec n := fun i => x i * y i
  28
  29/-- Componentwise inversion. -/
  30noncomputable def hadamardInv {n : ℕ} (x : Vec n) : Vec n := fun i => (x i)⁻¹
  31
  32/-- Componentwise division. -/
  33noncomputable def hadamardDiv {n : ℕ} (x y : Vec n) : Vec n := fun i => x i / y i
  34
  35/-- Exponential aggregate `R(x) = exp(∑ αᵢ log xᵢ)`. -/
  36noncomputable def aggregate {n : ℕ} (α x : Vec n) : ℝ :=
  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