finite induction

Stream: general

[Patrick Massot]

What is the idiomatic way to do finite induction?

lemma geom_lt {u : ℕ → ℝ} {k : ℝ} {n : ℕ} (h : ∀ m ≤ n, k*u m < u (m + 1)) :
k^(n + 1) *u 0 < u (n + 1) :=
begin
sorry
end

[Floris van Doorn]

In this particular case you can prove it by induction on n (though that might not work in general):

lemma geom_lt {u : ℕ → ℝ} {k : ℝ} (hk : 0 < k) {n : ℕ} (h : ∀ m ≤ n, k * u m < u (m + 1)) :
k^(n + 1) *u 0 < u (n + 1) :=
begin
  induction n with n ih,
  { convert h 0 (le_refl 0), rw [pow_one] },
  { refine lt_trans _ (h n.succ (le_refl n.succ)),
    rw [add_comm, pow_add, pow_one, mul_assoc, mul_lt_mul_left hk],
    refine ih (λ m hm, h m $ hm.step) }
end

More in the spirit of finite induction, you can generalize the result, and just induction on m with the hypothesis m ≤ n around (the proof is very similar, but you have to come up with the intermediate statement first)

lemma geom_lt' {u : ℕ → ℝ} {k : ℝ} (hk : 0 < k) {n : ℕ} (h : ∀ m ≤ n, k * u m < u (m + 1)) {m : ℕ}
  (hm : m ≤ n) : k^(m + 1) * u 0 < u (m + 1) :=
begin
  induction m with m ih,
  { convert h 0 (zero_le n), rw [pow_one] },
  { refine lt_trans _ (h m.succ hm),
    rw [add_comm, pow_add, pow_one, mul_assoc, mul_lt_mul_left hk],
    refine ih (le_trans (nat.le_succ m) hm) }
end