OAI/NumberTheory/EgyptianFractions/RandomProductWidePool.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomProducts.wide_fresh_product_le_exp line 10

   Source documentation

   The random-product estimate only needs the coarser upper bound S^101: a fixed-width prime interval is not required.

   theorem wide_fresh_product_le_exp {S V : ℝ} (hS : 2 ≤ S)
       (hV : 100000 * Real.log S ≤ V) :
       (S ^ 101) ^ freshLength S V ≤ Real.exp ((4 / 5 : ℝ) * V) := by
   …

   Mentions: OAI.Problem337.RandomProducts.freshLength

2. theorem OAI.Problem337.RandomProducts.wide_fresh_samples_product_le_exp line 24
3. theorem OAI.Problem337.RandomProducts.wide_fresh_samples_product_lt_modulus line 36