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

defectIterate_zero_pos

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)

  71theorem defectIterate_zero_pos {t : ℝ} (ht : t ≠ 0) : 0 < defectIterate t 0 := by

proof body

Term-mode proof.

  72  rw [defectIterate_zero_eq_J_log]
  73  exact Foundation.DiscretenessForcing.J_log_pos ht
  74
  75/-! ## §2. The recurrence from the RCL -/
  76
  77/-- **The composition recurrence.**
  78
  79    dₙ₊₁ = 2 · dₙ · (dₙ + 2)
  80
  81    This is forced by the Recognition Composition Law: applying the
  82    RCL to the pair (e^{2ⁿt}, e^{−2ⁿt}) yields the cosh double-angle
  83    formula, which is exactly this recurrence.
  84
  85    Mathematical content:
  86      cosh(2·u) = 2cosh²(u) − 1
  87      ⟹ cosh(2u)−1 = 2(cosh u − 1)(cosh u + 1)
  88                    = 2·(cosh u − 1)·((cosh u − 1) + 2) -/

used by (2)

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

depends on (9)

Lean names referenced from this declaration's body.