releaseRate_succ

formal source

  53  simp only [one_mul]
  54  exact pow_lt_pow_right₀ one_lt_phi h
  55
  56theorem releaseRate_succ (n : ℕ) :
  57    releaseRate (n + 1) = releaseRate n * phi := by
  58  unfold releaseRate
  59  rw [pow_succ]; ring
  60
  61/-! ## §2. Cumulative release -/
  62
  63/-- Cumulative CO₂ released over `n` rungs (geometric partial sum). -/
  64def cumulativeRelease (n : ℕ) : ℝ :=
  65  (Finset.range n).sum (fun k => releaseRate k)
  66
  67theorem cumulativeRelease_zero : cumulativeRelease 0 = 0 := by
  68  unfold cumulativeRelease; simp
  69
  70theorem cumulativeRelease_succ (n : ℕ) :
  71    cumulativeRelease (n + 1) = cumulativeRelease n + releaseRate n := by
  72  unfold cumulativeRelease
  73  rw [Finset.sum_range_succ]
  74
  75theorem cumulativeRelease_nonneg (n : ℕ) : 0 ≤ cumulativeRelease n := by
  76  unfold cumulativeRelease
  77  apply Finset.sum_nonneg
  78  intros k _
  79  exact le_of_lt (releaseRate_pos k)
  80
  81/-- Cumulative release is strictly monotonic in `n`. -/
  82theorem cumulativeRelease_strict_mono {n m : ℕ} (h : n < m) :
  83    cumulativeRelease n < cumulativeRelease m := by
  84  -- Induction on m - n.
  85  induction m, h using Nat.le_induction with
  86  | base =>