OAI/NumberTheory/EgyptianFractions/ConcreteGoodExposure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.RandomProducts.fresh_wide_product_le_exp line 10

   Source documentation

   Allows the wider prime pool with upper endpoint S^101.

   lemma fresh_wide_product_le_exp {S V : ℝ} (hS : 1 < S)
       (hV : 100000 * Real.log S ≤ V) :
       (S ^ 101) ^ freshLength S V ≤ Real.exp ((4 / 5 : ℝ) * V) := by
   …

   Mentions: OAI.Problem337.RandomProducts.freshLength

2. lemma OAI.Problem337.RandomProducts.fresh_wide_samples_lt_modulus line 24
3. theorem OAI.Problem337.RandomProducts.concrete_good_exposure_bound line 45

   Source documentation

   Concrete good-exposure estimate, with atom decay proved rather than assumed.

   theorem concrete_good_exposure_bound
       (S V : ℝ) (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S)
       (P : Finset ℕ) (hPprime : ∀ p ∈ P, Nat.Prime p)
       (hPcard : S ^ 99 ≤ (P.card : ℝ))
       (hPupper : ∀ p ∈ P, (p : ℝ) ≤ S ^ 101)
       (a u : ℕ) (hu : 0 < u) [NeZero u]
       (huV : (u : ℝ) ≤ Real.exp V)
       (hq : Real.exp ((9 / 10 : ℝ) * V) ≤ ((u / a.gcd u : ℕ) : ℝ))
       (t : ZMod u) :
       ‖(∑ w₁ : Fin (freshLength S V) → ↥P,
         ∑ w₂ : Fin (freshLength S V) → ↥P,
         ZMod.stdAddChar
   …

   Mentions: OAI.Problem337.RandomProducts.freshLength