zero_cost_iff_dot_zero

formal source

  20    simp [h]
  21
  22/-- Zero-cost iff weighted log sum vanishes. -/
  23theorem zero_cost_iff_dot_zero {n : ℕ} (α x : Vec n) :
  24    JcostN α x = 0 ↔ dot α (logVec x) = 0 :=
  25  JcostN_eq_zero_iff α x
  26
  27/-- Zero-cost iff aggregate equals one. -/
  28theorem zero_cost_iff_aggregate_one {n : ℕ} (α x : Vec n) :
  29    JcostN α x = 0 ↔ aggregate α x = 1 := by
  30  constructor
  31  · intro h
  32    exact (aggregate_eq_one_iff α x).2 ((zero_cost_iff_dot_zero α x).1 h)
  33  · intro h
  34    exact (zero_cost_iff_dot_zero α x).2 ((aggregate_eq_one_iff α x).1 h)
  35
  36end Ndim
  37end Cost
  38end IndisputableMonolith