def definition def or abbrev

`JcostN`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  44noncomputable def JcostN {n : ℕ} (α x : Vec n) : ℝ :=

Definition body.

  45  JlogN α (logVec x)
  46

From the project-wide theorem graph. These declarations reference this one in their body.

JcostN_eq_cosh_logsum in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_eq_Jcost_aggregate in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_eq_zero_iff in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_nonneg in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_reciprocal in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_unit in IndisputableMonolith.Cost.Ndim.Core decl_use
JcostN_dAlembert in IndisputableMonolith.Cost.Ndim.DAlembert decl_use
JcostN_submult in IndisputableMonolith.Cost.Ndim.DAlembert decl_use
zero_cost_iff_aggregate_one in IndisputableMonolith.Cost.Ndim.Neutrality decl_use
zero_cost_iff_dot_zero in IndisputableMonolith.Cost.Ndim.Neutrality decl_use
forced_of_factorization in IndisputableMonolith.Cost.Ndim.Uniqueness decl_use
forced_of_scalar_uniqueness in IndisputableMonolith.Cost.Ndim.Uniqueness decl_use
xDiagonalCorrection in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use

Lean names referenced from this declaration's body.