increasing_cantorFunction — Mathlib

English

Let c be a real number with 0 < c < 1/2. For any natural numbers n and any functions f,g : N → Bool, if f and g agree on all indices less than n and f(n) = false while g(n) = true, then cantorFunction(c) f < cantorFunction(c) g.

Русский

Пусть c — действительное число так, что 0 < c < 1/2. Для любых натуральных n и функций f,g : N → {0,1}, если f и g совпадают на всех индексах k < n, и f(n) = 0, g(n) = 1, то CantorFunction(c) aplicado к f меньше CantorFunction(c) aplicado к g.

LaTeX

$$$0 < c < \frac{1}{2} \Rightarrow \forall n \in \mathbb{N}, \forall f,g : \mathbb{N} \to \{0,1\}, (\forall k < n, f(k) = g(k)) \land f(n) = 0 \land g(n) = 1 \Rightarrow \operatorname{cantorFunction}(c)\,f < \operatorname{cantorFunction}(c)\,g$$$

Lean4

/-- `cantorFunction c` is strictly increasing with if `0 < c < 1/2`, if we endow `ℕ → Bool` with a
lexicographic order. The lexicographic order doesn't exist for these infinitary products, so we
explicitly write out what it means. -/
theorem increasing_cantorFunction (h1 : 0 < c) (h2 : c < 1 / 2) {n : ℕ} {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k)
    (fn : f n = false) (gn : g n = true) : cantorFunction c f < cantorFunction c g :=
  by
  have h3 : c < 1 := by
    apply h2.trans
    norm_num
  induction n generalizing f g with
  | zero =>
    let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
    have hf_max : ∀ n, f n → f_max n := by
      intro n hn
      cases n
      · rw [fn] at hn
        contradiction
      simp [f_max]
    let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
    have hg_min : ∀ n, g_min n → g n := by
      intro n hn
      cases n
      · rw [gn]
      simp at hn
    apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
    refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)
    have : c / (1 - c) < 1 := by
      rw [div_lt_one, lt_sub_iff_add_lt]
      · convert _root_.add_lt_add h2 h2
        norm_num
      rwa [sub_pos]
    convert this
    · rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ← tsum_geometric_of_lt_one (le_of_lt h1) h3]
      apply zero_add
    · refine (tsum_eq_single 0 ?_).trans ?_
      · intro n hn
        cases n
        · contradiction
        simp [g_min]
      · exact cantorFunctionAux_zero _
  | succ n ih =>
    rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]
    rw [hn 0 <| zero_lt_succ n]
    gcongr
    exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn

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