OAI/NumberTheory/EgyptianFractions/SupplySize.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.supplyPrimeCount line 11

   Source documentation

   Number of primes used by a logarithmic supply construction.

   def supplyPrimeCount (a : ℝ) (m : ℕ) : ℕ := ⌈a * Real.log (m : ℝ)⌉₊

2. def OAI.Problem337.supplyInteger line 14

   Source documentation

   A common supply denominator, before the rational-representation argument.

   def supplyInteger (a : ℝ) (m : ℕ) : ℕ :=
   …

3. lemma OAI.Problem337.supplyInteger_pos line 18
4. lemma OAI.Problem337.tendsto_supplyPrimeCount line 21
5. lemma OAI.Problem337.log_factorial_le_square line 26
6. lemma OAI.Problem337.eventually_log_supplyInteger_le_aux line 41
7. lemma OAI.Problem337.eventually_log_supplyInteger_le line 105

   Source documentation

   The logarithmic supply has the sharp leading size coefficient 2*a. Only elementary Chebyshev bounds are used; no prime number theorem is assumed.

   lemma eventually_log_supplyInteger_le {a ε : ℝ} (ha : 0 < a) (hε : 0 < ε) :
       ∀ᶠ m : ℕ in atTop,
         Real.log (supplyInteger a m : ℝ) ≤
           (2 * a + ε) * Real.log (m : ℝ) * Real.log (Real.log (m : ℝ)) := by
   …

   Mentions: OAI.Problem337.supplyInteger

8. lemma OAI.Problem337.eventual_marked_supply_size line 130
9. lemma OAI.Problem337.log_supplyInteger_lower line 139
10. lemma OAI.Problem337.marked_supplyInteger_gt line 163
11. lemma OAI.Problem337.marked_supply_size line 181
12. lemma OAI.Problem337.supplyPrimeCount_marked_eq line 193
13. lemma OAI.Problem337.eventually_small_dvd_supplyInteger line 201
14. def OAI.Problem337.rationalSupplyBase line 211

    Source documentation

    The prime product indexed by the argument used in the rational supply.

    def rationalSupplyBase (u : ℕ) : ℕ :=
    …

15. lemma OAI.Problem337.rationalSupplyBase_dvd_mono line 214
16. lemma OAI.Problem337.rationalSupplyBase_fourth_power line 224
17. lemma OAI.Problem337.rationalSupplyBase_sq_dvd_supplyInteger line 229
18. lemma OAI.Problem337.fourth_power_le_divisors_card_rationalSupplyBase line 235
19. lemma OAI.Problem337.rationalSupplyBase_le_supplyInteger line 254
20. lemma OAI.Problem337.eventually_log_rationalSupplyBase_le line 270