intensityAtRung_strictly_decreasing

formal source

  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
  70  intensity_pos : ∀ k, 0 < intensityAtRung k
  71  one_step_ratio :
  72    ∀ k, intensityAtRung (k + 1) = intensityAtRung k * phi⁻¹
  73  strictly_decreasing :
  74    ∀ k, intensityAtRung (k + 1) < intensityAtRung k
  75
  76/-- Lifting-program-design certificate. -/
  77def liftingProgramCert : LiftingProgramCert where
  78  intensity_pos := intensityAtRung_pos
  79  one_step_ratio := intensityAtRung_succ_ratio
  80  strictly_decreasing := intensityAtRung_strictly_decreasing
  81
  82end
  83end LiftingProgramDesign
  84end Sport
  85end IndisputableMonolith