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

k_peak_adjacent_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)

  48theorem k_peak_adjacent_ratio (k_0 : ℝ) (n : ℕ) (h : 0 < k_0) :
  49    k_peak k_0 (n + 1) / k_peak k_0 n = phi := by

proof body

Term-mode proof.

  50  unfold k_peak
  51  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
  52  have h_k0_ne : k_0 ≠ 0 := ne_of_gt h
  53  have h_pow_n_ne : phi ^ n ≠ 0 := pow_ne_zero n h_phi_ne
  54  rw [pow_succ]
  55  field_simp
  56
  57/-- The second-to-first peak ratio is `φ`. -/

used by (3)

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

depends on (6)

Lean names referenced from this declaration's body.