OAI/NumberTheory/EgyptianFractions/CountingFromMarkers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.denominator_ncard_le line 10
2. lemma OAI.Problem337.missing_le_count line 23
3. lemma OAI.Problem337.loglog_count_lower_of_missing line 35

   Source documentation

   Counting available exact markers forces many expansions. The explicit threshold is irrelevant asymptotically, but keeps this bridge entirely elementary.

   lemma loglog_count_lower_of_missing (k f w : ℕ) (hk : 6000000 ≤ k)
       (hlarge : Real.exp (Real.exp ((k : ℝ) / 600)) ≤ (w : ℝ))
       (hcount : w ≤ k * f + 2) :
       (k : ℝ) / 1200 ≤ Real.log (Real.log (f : ℝ)) := by
   …

4. theorem OAI.Problem337.counting_order_of_missing_lower line 76