MultiChannelJCostCert

formal source

  68  unfold Jcost_n
  69  congr 1; ext i; exact Jcost_symm (hx i)
  70
  71structure MultiChannelJCostCert where
  72  nonneg : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i), 0 ≤ Jcost_n x hx
  73  zero_iff : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i),
  74    Jcost_n x hx = 0 ↔ ∀ i, x i = 1
  75  at_ones : ∀ (n : ℕ), Jcost_n (fun (_ : Fin n) => (1 : ℝ)) (fun _ => one_pos) = 0
  76  symm : ∀ {n : ℕ} (x : Fin n → ℝ) (hx : ∀ i, 0 < x i),
  77    Jcost_n x hx = Jcost_n (fun i => (x i)⁻¹) (fun i => inv_pos.mpr (hx i))
  78
  79def multiChannelJCostCert : MultiChannelJCostCert where
  80  nonneg := Jcost_n_nonneg
  81  zero_iff := Jcost_n_zero_iff
  82  at_ones := fun _ => Jcost_n_at_ones
  83  symm := Jcost_n_symm
  84
  85end IndisputableMonolith.Foundation.MultiChannelJCost