  18abbrev Vec (n : ℕ) := Fin n → ℝ
  19
  20/-- Weighted dot product used by the logarithmic aggregate. -/
  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) :

papers checked against this theorem

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