def definition def or abbrev

`universalCost`

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

formal statement (Lean)

  98def universalCost (f : P →₀ ℕ) : ℝ :=

Definition body.

  99  f.sum (fun p k => (k : ℝ) * primeJcost p)
 100

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

universalCost_add in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universal_cost_certificate in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universalCost_nonneg in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universalCost_pos in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universalCost_single in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universalCost_single_one in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universalCost_smul_single in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
universalCost_zero in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use

Lean names referenced from this declaration's body.

primeJcost in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use