English
The value of ofDigits is at most 1.
Русский
Значение ofDigits не превосходит 1.
LaTeX
$$$\mathrm{Real.ofDigits}(\text{digits}) \le 1$$$
Lean4
theorem ofDigits_le_one {b : ℕ} (digits : ℕ → Fin b) : ofDigits digits ≤ 1 :=
by
obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
· simp [ofDigits, ofDigitsTerm]
rify at hb
convert Summable.tsum_mono summable_ofDigitsTerm _ (fun _ ↦ ofDigitsTerm_le)
· simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
rw [tsum_mul_left, tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])]
have := sub_pos.mpr hb
field_simp
· simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)
simp [inv_lt_one_iff₀, hb]
