`multiChannelJCostCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.MultiChannelJCost
domain: Foundation
line: 79 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.MultiChannelJCost on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

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