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

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

  35theorem spectralGap_strictly_decreasing (k : ℕ) :
  36    spectralGap (k + 1) < spectralGap k := by

proof body

Tactic-mode proof.

  37  unfold spectralGap
  38  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  39  have h : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  40    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  41    rw [zpow_add₀ hphi_ne]; simp
  42  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  43  rw [hcast, h]
  44  have hk_pos : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  45  have hphi_inv_lt_one : phi⁻¹ < 1 :=
  46    inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
  47  have : phi ^ (-(k : ℤ)) * phi⁻¹ < phi ^ (-(k : ℤ)) * 1 :=
  48    mul_lt_mul_of_pos_left hphi_inv_lt_one hk_pos
  49  simpa using this
  50
  51/-- The AS-level spectral gap at k=2 (the observed CAIDA value ≈ 0.382 ≈ 1/φ²). -/

used by (1)

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

depends on (12)

Lean names referenced from this declaration's body.