cumulativeRelease_zero

formal source

  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 =>
  87      rw [cumulativeRelease_succ]
  88      have := releaseRate_pos n; linarith
  89  | succ k _ ih =>
  90      rw [cumulativeRelease_succ]
  91      have := releaseRate_pos k; linarith
  92
  93/-! ## §3. Master certificate -/
  94
  95structure MarsAtmosphereJCostScheduleCert where
  96  rate_zero : releaseRate 0 = r_0
  97  rate_pos : ∀ n, 0 < releaseRate n