AutoSamplingTheory.TechnicalLemmas.Algebra.LinearGrowthOfStep

- A uniform lower bound on every one-step increment telescopes linearly.

theorem linear_growth_of_step_growth
    (r : ℕ → ℝ) (delta : ℝ)
    (hstep : ∀ n : ℕ, r n + delta ≤ r (n + 1)) :
    ∀ n : ℕ, r 0 + (n : ℝ) * delta ≤ r n := by
  intro n
  induction n with
  | zero => simp
  | succ n ih =>
      calc
        r 0 + ((n + 1 : ℕ) : ℝ) * delta =
            (r 0 + (n : ℝ) * delta) + delta := by
              simp [Nat.cast_add]
              ring
        _ ≤ r n + delta := by
          linarith [ih]
        _ ≤ r (n + 1) := hstep n

end Algebra
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Algebra/LinearGrowthOfStep.lean:17published source at 0e31a3cda412