def definition def or abbrev

`twistedPrimeCostSum`

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

formal statement (Lean)

 120def twistedPrimeCostSum (chi : ℕ → ℝ) (N : ℕ) : ℝ :=

Definition body.

 121  (Finset.range (N + 1)).sum fun p =>
 122    if Nat.Prime p then primeCost p * chi p else 0
 123

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

twistedPrimeCostSum_one_char in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use
twistedPrimeCostSum_zero in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use

Lean names referenced from this declaration's body.