noncomputable def decimalPrefix (digits : ℕ → Fin 10) (n : ℕ) : ℝ

The partial sum D n of the decimal expansion determined by digits.

def decimalBounds (digits : ℕ → Fin 10) (x : ℝ) : Prop

The decimal digits digits approximate x with the bounds D n ≤ x ≤ D n + 1/10^n.

def decimalBoundsStrict (digits : ℕ → Fin 10) (x : ℝ) : Prop

The decimal digits digits approximate x with strict lower bounds D n < x and start with a leading 0 digit.

theorem decimalPrefix_succ (digits : ℕ → Fin 10) (n : ℕ) : decimalPrefix digits (n + 1) = decimalPrefix digits n + ↑↑(digits (n + 1)) / 10 ^ (n + 1)

Expanding one more digit in the decimal prefix.

theorem decimalPrefix_nonneg (digits : ℕ → Fin 10) (n : ℕ) : 0 ≤ decimalPrefix digits n

theorem decimalPrefix_le_succ (digits : ℕ → Fin 10) (n : ℕ) : decimalPrefix digits n ≤ decimalPrefix digits (n + 1)

theorem decimalPrefix_monotone (digits : ℕ → Fin 10) : Monotone (decimalPrefix digits)

theorem decimalPrefix_tail_le (digits : ℕ → Fin 10) (n k : ℕ) : decimalPrefix digits (n + k) ≤ decimalPrefix digits n + 1 / 10 ^ n

Bounding the tail of the decimal prefix by a geometric sum.

theorem decimalPrefix_le_one (digits : ℕ → Fin 10) (n : ℕ) : decimalPrefix digits n ≤ 1

Each decimal prefix is bounded above by 1.

theorem decimalPrefix_le_prefix_add (digits : ℕ → Fin 10) (n m : ℕ) : decimalPrefix digits m ≤ decimalPrefix digits n + 1 / 10 ^ n

A global bound on any prefix in terms of the n-th prefix.

theorem one_div_pow_ten_lt {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ), 1 / 10 ^ n < ε

Powers 1/10^n can be made arbitrarily small.

theorem exists_sup_decimalBounds (digits : ℕ → Fin 10) : ∃ x ∈ Set.Icc 0 1, decimalBounds digits x

Using the supremum of decimal prefixes gives an x satisfying the decimal bounds.

theorem decimalBounds_value_unique (digits : ℕ → Fin 10) {x y : ℝ} (hx : decimalBounds digits x) (hy : decimalBounds digits y) : x = y

The value determined by a given digit stream satisfying decimal bounds is unique.

theorem decimalBounds_strict_of_pos_digits {digits : ℕ → Fin 10} {x : ℝ} (hzero : digits 0 = 0) (hpos : ∀ (n : ℕ), 0 < ↑↑(digits (n + 1))) (h : decimalBounds digits x) : decimalBoundsStrict digits x

theorem diagonal_digits_value (digits : ℕ → Fin 10) (hzero : digits 0 = 0) (hpos : ∀ (n : ℕ), 0 < ↑↑(digits (n + 1))) : ∃! y : ℝ, y ∈ Set.Icc 0 1 ∧ decimalBoundsStrict digits y

theorem exists_digits_decimalBoundsStrict {x : ℝ} (hx : x ∈ Set.Ioc 0 1) : ∃ (digits : ℕ → Fin 10), decimalBoundsStrict digits x

theorem decimalBoundsStrict_digits_unique {x : ℝ} {digits₁ digits₂ : ℕ → Fin 10} (h₁ : decimalBoundsStrict digits₁ x) (h₂ : decimalBoundsStrict digits₂ x) : digits₁ = digits₂

theorem decimal_expansion_properties : (∀ (digits : ℕ → Fin 10), ∃! x : ℝ, x ∈ Set.Icc 0 1 ∧ decimalBounds digits x) ∧ ∀ x ∈ Set.Ioc 0 1, (∃ (digits : ℕ → Fin 10), decimalBounds digits x) ∧ ∃! digits : ℕ → Fin 10, decimalBoundsStrict digits x

Proposition 1.5.1. (i) Every infinite sequence of digits 0.d1d2d3… represents a unique real number x ∈ [0, 1] such that D n ≤ x ≤ D n + 1/10^n for all n ∈ ℕ, where D n is the partial sum of the first n digits. (ii) For every x ∈ (0, 1] there exists an infinite sequence of digits representing x, and there is a unique representation satisfying D n < x ≤ D n + 1/10^n for all n ∈ ℕ.

theorem diagonal_not_in_enumeration (f : ℕ → ↑(Set.Ioc 0 1)) : ∃ y ∈ Set.Ioc 0 1, ∀ (n : ℕ), y ≠ ↑(f n)

Diagonal number built from an enumeration of (0, 1] differs from every entry.

theorem cantor_uncountable_Ioc : ¬(Set.Ioc 0 1).Countable

Theorem 1.5.2 (Cantor): The set (0, 1] is uncountable.

theorem rational_decimal_digits_eventually_periodic (x : ℚ) (digits : ℕ → Fin 10) (_hx : ↑x ∈ Set.Ioc 0 1) (hx_digits : decimalBounds digits ↑x) : ∃ (N : ℕ) (P : ℕ), 0 < N ∧ 0 < P ∧ ∀ {n : ℕ}, N ≤ n → digits n = digits (n + P)

Proposition 1.5.3: If a rational number x ∈ (0, 1] has decimal expansion 0.d₁d₂d₃…, then its digits eventually repeat, i.e., there exist positive integers N and P such that dₙ = dₙ₊ₚ for all n ≥ N.

def Nat.triangle : ℕ → ℕ

Triangular numbers: triangle n = 1 + 2 + … + n.

@[simp]

theorem Nat.triangle_zero : triangle 0 = 0

theorem Nat.triangle_succ' (n : ℕ) : (n + 1).triangle = n.triangle + (n + 1)

noncomputable def digitsInc : ℕ → Fin 10

Digits for Example 1.5.4: 1 at triangular indices and 0 otherwise.

theorem digitsInc_triangle (k : ℕ) : digitsInc (k + 1).triangle = 1

theorem digitsInc_zero {n : ℕ} (h : ¬∃ (k : ℕ), n = (k + 1).triangle) : digitsInc n = 0

theorem digitsInc_le_one (n : ℕ) : ↑↑(digitsInc n) ≤ 1

theorem triangle_strictMono : StrictMono Nat.triangle

theorem le_triangle_succ (k : ℕ) : k ≤ (k + 1).triangle

theorem digitsInc_nonperiodic_gap (N P : ℕ) : 0 < P → ∃ n ≥ N, digitsInc n = 1 ∧ digitsInc (n + P) = 0

noncomputable def decimalWithIncreasingZeroBlocks : ℝ

Example 1.5.4: The real number with decimal expansion 0.101001000100001…, whose 1s occur at the positions 1, 3, 6, 10, … (each separated by an increasing block of zeros), is irrational.

theorem decimalWithIncreasingZeroBlocks_bounds : decimalBoundsStrict digitsInc decimalWithIncreasingZeroBlocks

theorem irrational_decimalWithIncreasingZeroBlocks : Irrational decimalWithIncreasingZeroBlocks

The number decimalWithIncreasingZeroBlocks from Example 1.5.4 is irrational.