OAI/NumberTheory/EgyptianFractions/CompositeMarkedReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.CompositeSupply.quantitative_marked_length_of_supply line 14

   Source documentation

   The new fourth-power auxiliary integer can be passed directly to the already proved marked construction. Its positivity, size coefficient, and marked greedy prefix are unconditional; precisely the arithmetic supply remains as an explicit hypothesis here.

   theorem quantitative_marked_length_of_supply
       (hsupply : ∀ᶠ m : ℕ in atTop, HasRationalDivisorSupply m (multiplier m) 16) :
       ∀ ε : ℝ, 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.CompositeSupply.multiplier, OAI.Problem337.IsOneExpansion