summable_cantor_function — Mathlib

English

For 0 ≤ c < 1 and any f: ℕ → Bool, cantorFunctionAux c f is summable (the associated series converges).

Русский

Для 0 ≤ c < 1 и любого f: ℕ → Bool, cantorFunctionAux c f суммируемо (сумма ряда сходится).

LaTeX

$$$0 \\le c \\wedge c < 1 \\Rightarrow \\text{Summable}(\\operatorname{cantorFunctionAux}(c,f))$$$

Lean4

theorem summable_cantor_function (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) : Summable (cantorFunctionAux c f) :=
  by
  apply (summable_geometric_of_lt_one h1 h2).summable_of_eq_zero_or_self
  intro n; cases h : f n <;> simp [h]

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