div_lt_arithGeom — Mathlib

English

If 1 < a and b/(1-a) < u0, then arithGeom(a,b,u0) is strictly increasing in n.

Русский

Если 1 < a и b/(1-a) < u0, тогда arithGeom(a,b,u0) строго возрастает как функция от n.

LaTeX

$$1 < a \land \frac{b}{1-a} < u_0 \Rightarrow \operatorname{StrictMono}(\mathrm{arithGeom}(a,b,u_0))$$

Lean4

theorem div_lt_arithGeom (ha_pos : 0 < a) (ha_ne : a ≠ 1) (h0 : b / (1 - a) < u₀) (n : ℕ) :
    b / (1 - a) < arithGeom a b u₀ n := by
  induction n with
  | zero => exact h0
  | succ n hn =>
    calc
      b / (1 - a)
      _ = a * (b / (1 - a)) + b := by grind
      _ < a * arithGeom a b u₀ n + b := by gcongr

Похожие утверждения