Part of: The digit sequence has infinitely many ones and infinitely many zeros; and a rational constant would have eventually periodic digits.
TheoremeventuallyPeriodic_of_not_irrational
If \varrho is not irrational, then the bit sequence is eventually periodic: there
exist N and P > 0 with b_{k+P} = b_k for all k \ge N.
Lean code for Theorem eventuallyPeriodic_of_not_irrational
-
≈
theorem eventuallyPeriodic_of_not_irrational : ¬ Irrational
Irrational (x : ℝ) : PropA real number is irrational if it is not equal to any rational number.ϱA362583.ϱ : ℝThe prime race constant (the A362583 constant): the sum of the series `ϱ = Σ_{k ≥ 0} bit k · 2^{-(k+1)}`, i.e. the real number whose `k`-th binary digit is `bit k` — in binary `0.b₀b₁b₂…₂ ≈ 0.7004001…` (decimal). OEIS A362583 lists the successive digit prefixes read as binary integers.→ ∃ NℕPℕ, 0ℕ< Pℕ∧ ∀ kℕ≥ Nℕ, bitA362583.bit (k : ℕ) : ℕ`k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`. The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1` (primes `3, 5, 7, 11, 13, 17, 19, 23`).(kℕ+ Pℕ) = bitA362583.bit (k : ℕ) : ℕ`k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`. The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1` (primes `3, 5, 7, 11, 13, 17, 19, 23`).kℕtheorem eventuallyPeriodic_of_not_irrational : ¬ Irrational
Irrational (x : ℝ) : PropA real number is irrational if it is not equal to any rational number.ϱA362583.ϱ : ℝThe prime race constant (the A362583 constant): the sum of the series `ϱ = Σ_{k ≥ 0} bit k · 2^{-(k+1)}`, i.e. the real number whose `k`-th binary digit is `bit k` — in binary `0.b₀b₁b₂…₂ ≈ 0.7004001…` (decimal). OEIS A362583 lists the successive digit prefixes read as binary integers.→ ∃ NℕPℕ, 0ℕ< Pℕ∧ ∀ kℕ≥ Nℕ, bitA362583.bit (k : ℕ) : ℕ`k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`. The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1` (primes `3, 5, 7, 11, 13, 17, 19, 23`).(kℕ+ Pℕ) = bitA362583.bit (k : ℕ) : ℕ`k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`. The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1` (primes `3, 5, 7, 11, 13, 17, 19, 23`).kℕ
Define the binary tails t_k := \sum_{j \ge 0} b_{k+j}\, 2^{-(j+1)}, so that t_0 = \varrho;
the argument runs through the tails, in the Lean file's zero-based indexing.
First, t_k \in (0,1) strictly for every k: infinitely many later ones force
t_k > 0, and infinitely many later zeros force t_k < 1. Next, the recurrence
t_k = (b_k + t_{k+1})/2 holds by splitting off the first term of the tail, so if b_k = 1
then t_k \in (1/2, 1) and if b_k = 0 then t_k \in (0, 1/2). In particular
t_k \ne 1/2 always, so t_k determines b_k (b_k = 1 \iff t_k > 1/2) and hence
also t_{k+1} = 2 t_k - b_k.
Because 2^k \varrho is an integer plus t_k and t_k \in (0,1), we have
t_k = \operatorname{fract}(2^k \varrho). If \varrho is rational with denominator b,
then each t_k = \operatorname{fract}(2^k \varrho) lies in the finite set
\{0, 1/b, \ldots, (b-1)/b\} — in Lean, the denominator of the rational witness produced by
unfolding "not irrational" — so by pigeonhole there are m < n with t_m = t_n. Since
t_k determines both b_k and t_{k+1}, induction propagates the collision:
t_{m+i} = t_{n+i} and b_{m+i} = b_{n+i} for all i \ge 0. Hence the bits are periodic
with period P = n - m from index m. \blacksquare
≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.
introIntroduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.
* `intro` by itself introduces one anonymous hypothesis, which can be accessed
by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
can be anonymized via `_`, given a type ascription, or matched against a pattern:
```lean
-- ... ⊢ α × β → ...
intro (a, b)
-- ..., a : α, b : β ⊢ ...
```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
```lean
intro
| n + 1, 0 => tac
| ...
```
h
obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.
```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```
If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
If `type` is omitted, `:= proof` is required.
⟨m, n, hmn, ht⟩ := exists_t_collision h
refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
⟨m, n - m, by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
, fun k hk ↦ ?_⟩
obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.
```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```
If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
If `type` is omitted, `:= proof` is required.
⟨i, rfl⟩ : ∃ i, k = m + i := ⟨k - m, by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
⟩
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hbi : bit (m + i) = bit (n + i) := bit_eq_of_t_eq (t_eq_add ht i)
rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
[show m + i + (n - m) = n + i from by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
, ← hbi]