arithGeom_strictMono — Mathlib

English

Under the same hypotheses, arithGeom is strictly increasing.

Русский

При тех же условиях arithGeom строго возрастает.

LaTeX

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

Lean4

theorem arithGeom_strictMono (ha : 1 < a) (h0 : b / (1 - a) < u₀) : StrictMono (arithGeom a b u₀) :=
  by
  refine strictMono_nat_of_lt_succ fun n ↦ ?_
  have h_lt : b / (1 - a) < arithGeom a b u₀ n := div_lt_arithGeom (by positivity) ha.ne' h0 n
  rw [div_lt_iff_of_neg (sub_neg.mpr ha)] at h_lt
  rw [arithGeom_succ]
  linarith

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