MarkedEndgame.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.marked_tail_disjoint line 13
Source documentation
A positive tail whose total is smaller than every reserved term cannot reuse a reserved denominator.
```
theorem marked_tail_disjoint (p t : Finset ℕ)
    (hsmall : ∀ d ∈ p, (∑ e ∈ t, (1 : ℚ) / (e : ℚ)) < 1 / (d : ℚ)) :
    Disjoint p t := by
…
```

theorem OAI.Problem337.marked_expansion_of_small_tail line 25

Source documentation

Adjoining a small distinct tail preserves every denominator in the prefix, including the prescribed marker, and adds the lengths exactly.

theorem marked_expansion_of_small_tail (p t : Finset ℕ) (m : ℕ)
    (hp : ∀ d ∈ p, 1 ≤ d) (ht : ∀ d ∈ t, 1 ≤ d)
    (hm : m ∈ p)
    (hsum : (∑ d ∈ p, (1 : ℚ) / (d : ℚ)) +
      (∑ d ∈ t, (1 : ℚ) / (d : ℚ)) = 1)
    (hsmall : ∀ d ∈ p, (∑ e ∈ t, (1 : ℚ) / (e : ℚ)) < 1 / (d : ℚ)) :
    ∃ n : Fin (p.card + t.card) → ℕ,
      IsOneExpansion n ∧ ∃ i, n i = m := by
…

Mentions: OAI.Problem337.IsOneExpansion

theorem OAI.Problem337.marked_expansion_of_egyptian_tail line 61

Source documentation

The small-tail assembly accepts the standard Egyptian expansion interface.

theorem marked_expansion_of_egyptian_tail {k : ℕ} {x : ℚ}
    (p : Finset ℕ) (m : ℕ) (n : Fin k → ℕ)
    (hp : ∀ d ∈ p, 1 ≤ d) (hm : m ∈ p)
    (hn : IsEgyptianExpansion x n)
    (hsum : (∑ d ∈ p, (1 : ℚ) / (d : ℚ)) + x = 1)
    (hsmall : ∀ d ∈ p, x < 1 / (d : ℚ)) :
    ∃ n' : Fin (p.card + k) → ℕ,
      IsOneExpansion n' ∧ ∃ i, n' i = m := by
…

Mentions: OAI.Problem337.IsEgyptianExpansion, OAI.Problem337.IsOneExpansion

theorem OAI.Problem337.quantitative_marked_length_of_prefix_group_budget line 90

Source documentation

The explicit bookkeeping at the end of the marked construction. The prefix costs 1 / log 2 and sixteen terms in each of 16 / log 2 groups; the reserved marker is absorbed by the diverging double logarithm.

theorem quantitative_marked_length_of_prefix_group_budget
    (hbudget : ∀ δ : ℝ, 0 < δ → ∀ᶠ m : ℕ in atTop,
      ∃ j G k : ℕ, ∃ n : Fin k → ℕ,
        IsOneExpansion n ∧ (∃ i, n i = m) ∧
        k ≤ 1 + j + 16 * G ∧
        (j : ℝ) ≤ (1 / Real.log 2 + δ) * Real.log (Real.log (m : ℝ)) ∧
        (G : ℝ) ≤ (16 / Real.log 2 + δ) * Real.log (Real.log (m : ℝ))) :
    ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
      ∀ m : ℕ, M ≤ m → ∃ k : ℕ, ∃ n : Fin k → ℕ,
        IsOneExpansion n ∧ (∃ i, n i = m) ∧
        (k : ℝ) ≤ (257 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)) := by
…

Mentions: OAI.Problem337.IsOneExpansion