k_peak_adjacent_ratio

formal source

  45  exact mul_pos h (pow_pos phi_pos n)
  46
  47/-- Adjacent peak ratio is exactly `φ`. -/
  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
  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 `φ`. -/
  58theorem peak_2_1_ratio (k_0 : ℝ) (h : 0 < k_0) :
  59    k_peak k_0 2 / k_peak k_0 1 = phi :=
  60  k_peak_adjacent_ratio k_0 1 h
  61
  62/-- The third-to-second peak ratio is `φ`. -/
  63theorem peak_3_2_ratio (k_0 : ℝ) (h : 0 < k_0) :
  64    k_peak k_0 3 / k_peak k_0 2 = phi :=
  65  k_peak_adjacent_ratio k_0 2 h
  66
  67/-- The third-to-first peak ratio is `φ²`. -/
  68theorem peak_3_1_ratio (k_0 : ℝ) (h : 0 < k_0) :
  69    k_peak k_0 3 / k_peak k_0 1 = phi ^ 2 := by
  70  unfold k_peak
  71  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
  72  have h_k0_ne : k_0 ≠ 0 := ne_of_gt h
  73  field_simp
  74
  75/-- The peak ratios are independent of the base scale `k_0`. -/
  76theorem peak_ratios_scale_invariant
  77    (k_0 k_0' : ℝ) (n m : ℕ) (h : 0 < k_0) (h' : 0 < k_0') :
  78    k_peak k_0 (n + m) / k_peak k_0 n = k_peak k_0' (n + m) / k_peak k_0' n := by