def definition def or abbrev

`sigmaCore`

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

formal statement (Lean)

  13def sigmaCore (n : ℕ) (a2 : ℝ) : ℝ :=

Definition body.

  14  let num := (3 : ℝ) ^ n * (a2) ^ n
  15  let den := 2 * (1 - 2 * a2) ^ (2 * n - 1)
  16  num / den
  17

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