MarkedReduction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.HasQuantitativeMarkedPrefix line 14
Source documentation
The precise portion of the marked greedy-prefix output used by the final construction. The marker is not included in p; it is inserted afterwards.
```
def HasQuantitativeMarkedPrefix (m K : ℕ) : Prop :=
…
```

theorem OAI.Problem337.quantitative_marked_length_of_supply_and_prefix line 27

Source documentation

Full quantitative endgame: a rational-divisor supply with a logarithmic size estimate and the marked greedy prefix imply the 257 / log 2 + ε bound. Both remaining construction inputs are exposed explicitly.

theorem quantitative_marked_length_of_supply_and_prefix (K : ℕ → ℕ)
    (hKpositive : ∀ᶠ m : ℕ in atTop, 0 < K m)
    (hsize : ∀ δ : ℝ, 0 < δ → ∀ᶠ m : ℕ in atTop,
      Real.log (K m : ℝ) ≤ (32 / Real.log 2 + δ) * Real.log (m : ℝ) *
        Real.log (Real.log (m : ℝ)))
    (hsupply : ∀ᶠ m : ℕ in atTop, HasRationalDivisorSupply m (K m) 16)
    (hprefix : ∀ᶠ m : ℕ in atTop, HasQuantitativeMarkedPrefix m (K 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.HasRationalDivisorSupply, OAI.Problem337.HasQuantitativeMarkedPrefix, OAI.Problem337.IsOneExpansion