English
If 0 ≤ c < 1 and f ≤ g pointwise (i.e., ∀n, f(n) → g(n)), then CantorFunction c f ≤ CantorFunction c g.
Русский
Если 0 ≤ c < 1 и f по каж-ному пункту не превосходит g (∀n, f(n) → g(n)), то CantorFunction c f ≤ CantorFunction c g.
LaTeX
$$$0 \\le c \\land c < 1 \\land (\\forall n, f(n) \\to g(n)) \\Rightarrow \\operatorname{cantorFunction}(c,f) \\le \\operatorname{cantorFunction}(c,g)$$$
Lean4
theorem cantorFunction_le (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ n, f n → g n) : cantorFunction c f ≤ cantorFunction c g :=
by
apply (summable_cantor_function f h1 h2).tsum_le_tsum _ (summable_cantor_function g h1 h2)
intro n; cases h : f n
· simp [h, cantorFunctionAux_nonneg h1]
replace h3 : g n = true := h3 n h; simp [h, h3]
