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

echoAmplitude_strictly_decreasing

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)

  60theorem echoAmplitude_strictly_decreasing (n : ℕ) :
  61    echoAmplitude (n + 1) < echoAmplitude n := by

proof body

Term-mode proof.

  62  rw [echoAmplitude_succ_ratio]
  63  have hn : 0 < echoAmplitude n := echoAmplitude_pos n
  64  have : phi⁻¹ < 1 :=
  65    inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
  66  linarith [mul_lt_iff_lt_one_right hn |>.mpr this]
  67
  68/-- Per-event echo-amplitude chain for catalog events. -/

used by (1)

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.