pith. machine review for the scientific record. sign in
theorem proved term proof

doubledZeroDefect_recurrence

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  40theorem doubledZeroDefect_recurrence (ρ : ℂ) :
  41    doubledZeroDefect ρ = 2 * (zeroDefect ρ) ^ 2 + 4 * zeroDefect ρ := by

proof body

Term-mode proof.

  42  rw [doubledZeroDefect_eq_cosh_sub_one, zeroDefect_eq_cosh_sub_one]
  43  rw [Real.cosh_two_mul]
  44  nlinarith [Real.cosh_sq (zeroDeviation ρ)]
  45
  46/-- The doubled zero defect is always nonnegative. -/

used by (2)

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

depends on (10)

Lean names referenced from this declaration's body.