def definition def or abbrev

`partialSum`

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

formal statement (Lean)

  23noncomputable def partialSum (n : ℕ) : ℝ :=

Definition body.

  24  (Finset.range n).sum (fun i => coeff i)
  25
  26/-- Generating functional F(z) := log(1 + z/φ).  -/

Lean names referenced from this declaration's body.

F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
coeff in IndisputableMonolith.Pipelines decl_use
F in IndisputableMonolith.Pipelines decl_use