English
CantorFunction c f satisfies a recursive decomposition: discrete initial term plus c times CantorFunction on the tail.
Русский
CantorFunction c f удовлетворяет рекурсивному разложению: начальный член плюс c умноженное на CantorFunction по хвосту.
LaTeX
$$$\\operatorname{cantorFunction}(c,f) = \\operatorname{cond}(f(0),1,0) + c \\cdot \\operatorname{cantorFunction}\\left(c, n \\mapsto f(n+1)\\right)$$$
Lean4
theorem cantorFunction_succ (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) :
cantorFunction c f = cond (f 0) 1 0 + c * cantorFunction c fun n => f (n + 1) :=
by
rw [cantorFunction, (summable_cantor_function f h1 h2).tsum_eq_zero_add]
rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]
