`multiChannelJCostCert`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.MultiChannelJCost on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.