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

etaBAt_succ_ratio

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)

  46theorem etaBAt_succ_ratio (N : ℕ) :
  47    etaBAt (N + 1) = etaBAt N * phi⁻¹ := by

proof body

Tactic-mode proof.

  48  unfold etaBAt
  49  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  50  have hzpow : phi ^ (-((N : ℤ) + 1)) = phi ^ (-(N : ℤ)) * phi⁻¹ := by
  51    rw [show (-((N : ℤ) + 1)) = -(N : ℤ) + (-1 : ℤ) by ring]
  52    rw [zpow_add₀ hphi_ne]
  53    simp
  54  have hcast : ((N + 1 : ℕ) : ℤ) = (N : ℤ) + 1 := by push_cast; ring
  55  rw [hcast, hzpow]
  56
  57/-- η_B is strictly monotone-decreasing in e-fold count. -/

used by (3)

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.