intensityAtRung

formal source

  36def referenceIntensity : ℝ := 1
  37
  38/-- Intensity at φ-ladder rung `k` (rung 0 = 1RM). -/
  39def intensityAtRung (k : ℕ) : ℝ := referenceIntensity * phi ^ (-(k : ℤ))
  40
  41theorem intensityAtRung_pos (k : ℕ) : 0 < intensityAtRung k := by
  42  unfold intensityAtRung referenceIntensity
  43  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  44  linarith [this]
  45
  46theorem intensityAtRung_succ_ratio (k : ℕ) :
  47    intensityAtRung (k + 1) = intensityAtRung k * phi⁻¹ := by
  48  unfold intensityAtRung
  49  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  50  have hzpow : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  51    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  52    rw [zpow_add₀ hphi_ne]
  53    simp
  54  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  55  rw [hcast, hzpow]; ring
  56
  57theorem intensityAtRung_strictly_decreasing (k : ℕ) :
  58    intensityAtRung (k + 1) < intensityAtRung k := by
  59  rw [intensityAtRung_succ_ratio]
  60  have hk : 0 < intensityAtRung k := intensityAtRung_pos k
  61  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  62    have hphi_gt_one : (1 : ℝ) < phi := by
  63      have := Constants.phi_gt_onePointFive; linarith
  64    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  65  have : intensityAtRung k * phi⁻¹ < intensityAtRung k * 1 :=
  66    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  67  simpa using this
  68
  69structure LiftingProgramCert where