RepeatedSquaring.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.repeated_squaring_bound line 10

Source documentation

Iterated squaring after a starting bound. The finite horizon avoids hypotheses on states beyond the stopping point of an algorithm.

theorem repeated_squaring_bound (x : ℕ → ℝ) (a : ℝ) (N : ℕ)
    (_ha : 0 ≤ a) (hzero : x 0 ≤ a)
    (hpos : ∀ i ≤ N, 0 ≤ x i)
    (hstep : ∀ i < N, x (i + 1) ≤ (x i) ^ 2) :
    ∀ i ≤ N, x i ≤ a ^ (2 ^ i) := by
…

theorem OAI.Problem337.repeated_squaring_one_exception line 28

Source documentation

One exceptional step is permitted to decrease the sequence without squaring it. After n steps, at least n-1 effective squarings remain.

theorem repeated_squaring_one_exception (x : ℕ → ℝ) (t N : ℕ)
    (hzero : x 0 ≤ (1 / 2 : ℝ))
    (hpos : ∀ i ≤ N, 0 ≤ x i)
    (hstep : ∀ i < N, i ≠ t → x (i + 1) ≤ (x i) ^ 2)
    (hexception : t < N → x (t + 1) ≤ x t) :
    ∀ i ≤ N, 1 ≤ i → x i ≤ (1 / 2 : ℝ) ^ (2 ^ (i - 1)) := by
…

theorem OAI.Problem337.denominator_bound_of_small_remainder line 65
Source documentation
Convert a small positive rational remainder to a large unreduced denominator. The premise 1 ≤ q*x expresses that its numerator is a positive integer.
```
theorem denominator_bound_of_small_remainder {x q : ℝ} (e : ℕ)
    (hq : 0 ≤ q) (hnum : 1 ≤ q * x)
    (hx : x ≤ (1 / 2 : ℝ) ^ e) :
    (2 : ℝ) ^ e ≤ q := by
…
```
theorem OAI.Problem337.double_power_lt_loglog_bound line 78
Source documentation
Inverting a double power, in the precise base-two convention used by the marked greedy prefix bound.
```
theorem double_power_lt_loglog_bound (n : ℕ) (T : ℝ)
    (hbound : (2 : ℝ) ^ (2 ^ n) < T) :
    (n : ℝ) < Real.log (Real.log T / Real.log 2) / Real.log 2 := by
…
```

theorem OAI.Problem337.marked_prefix_length_of_double_power line 92

Source documentation

The stopping-time estimate for a prefix whose penultimate denominator is below T.

theorem marked_prefix_length_of_double_power (j : ℕ) (T : ℝ)
    (hj : 3 ≤ j) (hbound : (2 : ℝ) ^ (2 ^ (j - 3)) < T) :
    (j : ℝ) < 3 + Real.log (Real.log T / Real.log 2) / Real.log 2 := by
…

theorem OAI.Problem337.repeated_squaring_one_exception_rat line 101

Source documentation

Rational-valued version, convenient for unreduced greedy remainders.

theorem repeated_squaring_one_exception_rat (x : ℕ → ℚ) (t N : ℕ)
    (hzero : x 0 ≤ (1 / 2 : ℚ))
    (hpos : ∀ i ≤ N, 0 ≤ x i)
    (hstep : ∀ i < N, i ≠ t → x (i + 1) ≤ (x i) ^ 2)
    (hexception : t < N → x (t + 1) ≤ x t) :
    ∀ i ≤ N, 1 ≤ i → x i ≤ (1 / 2 : ℚ) ^ (2 ^ (i - 1)) := by
…

theorem OAI.Problem337.nat_denominator_bound_of_small_remainder line 120

Source documentation

Natural denominator version of the reciprocal remainder estimate.

theorem nat_denominator_bound_of_small_remainder (R q e : ℕ)
    (hR : 0 < R) (hq : 0 < q)
    (hsmall : (R : ℚ) / (q : ℚ) ≤ (1 / 2 : ℚ) ^ e) :
    2 ^ e ≤ q := by
…

theorem OAI.Problem337.marked_greedy_chain_length_bound line 137

Source documentation

Direct interface for a marked greedy chain, indexed as in the manuscript. The exceptional transition is t; taking t beyond the horizon covers no exception.

theorem marked_greedy_chain_length_bound (R q : ℕ → ℕ) (j t T : ℕ)
    (hj : 3 ≤ j) (ht : 1 ≤ t)
    (hfirst : (R 1 : ℚ) / (q 1 : ℚ) ≤ (1 / 2 : ℚ))
    (hstep : ∀ i, 1 ≤ i → i < j - 1 → i ≠ t →
      (R (i + 1) : ℚ) / (q (i + 1) : ℚ) ≤ ((R i : ℚ) / (q i : ℚ)) ^ 2)
    (hexception : t < j - 1 →
      (R (t + 1) : ℚ) / (q (t + 1) : ℚ) ≤ (R t : ℚ) / (q t : ℚ))
    (hR : 0 < R (j - 1)) (hq : 0 < q (j - 1)) (hactive : q (j - 1) < T) :
    (j : ℝ) < 3 + Real.log (Real.log (T : ℝ) / Real.log 2) / Real.log 2 := by
…

theorem OAI.Problem337.repeated_squaring_at_most_one_exception_rat line 169

Source documentation

A form requiring only uniqueness of a transition which fails to square; there is no need to choose its index in the construction.

theorem repeated_squaring_at_most_one_exception_rat (x : ℕ → ℚ) (N : ℕ)
    (hzero : x 0 ≤ (1 / 2 : ℚ))
    (hpos : ∀ i ≤ N, 0 ≤ x i)
    (hdecrease : ∀ i < N, x (i + 1) ≤ x i)
    (hunique : ∀ i < N, ∀ j < N,
      ¬ x (i + 1) ≤ (x i) ^ 2 → ¬ x (j + 1) ≤ (x j) ^ 2 → i = j) :
    ∀ i ≤ N, 1 ≤ i → x i ≤ (1 / 2 : ℚ) ^ (2 ^ (i - 1)) := by
…

theorem OAI.Problem337.greedy_denominator_below_square line 191
Source documentation
Denominator square bound at an integer cut-off; no real rounding is involved.
```
theorem greedy_denominator_below_square (q n T : ℕ)
    (hq : q < T) (hn : n ≤ q + 1) : q * n < T ^ 2 := by
…
```