OAI/NumberTheory/EgyptianFractions/RandomGcdMarginal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Typed-sample form of the concrete reduced-modulus exceptional-event bound.

   theorem random_gcd_typed_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
       (P : Finset ℕ) (u l : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 2 ≤ S) (hV : 0 ≤ V) (hVS : V ≤ S)
       (huexp : (u : ℝ) = Real.exp V) (hprime : ∀ p ∈ P, Nat.Prime p)
       (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
       (ht : (Fintype.card ι : ℝ) ≤ S) (hsize : S ^ 99 ≤ (P.card : ℝ))
       (hl : 0 < l) (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
       (Fintype.card {f : ι → P //
         ((u / Nat.gcd (l * ∏ i, (f i : ℕ)) u : ℕ) : ℝ) < Real.exp (9 * V / 10)} : ℝ) /
           (Fintype.card (ι → P) : ℝ) ≤ Real.exp (-V / 20) := by
   …

2. theorem OAI.Problem337.RandomProducts.random_gcd_marginal_bound line 28

   Source documentation

   An exposed product may use only some of the exposed coordinates. Other exposed samples do not change its exceptional-event probability: the exact uniform marginal identity reduces it to the independently sampled product bound.

   theorem random_gcd_marginal_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
       (P : Finset ℕ) (A : Finset ι) (u l : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 2 ≤ S) (hV : 0 ≤ V) (hVS : V ≤ S)
       (huexp : (u : ℝ) = Real.exp V) (hprime : ∀ p ∈ P, Nat.Prime p)
       (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
       (ht : (A.card : ℝ) ≤ S) (hsize : S ^ 99 ≤ (P.card : ℝ))
       (hl : 0 < l) (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
       (Fintype.card {f : ι → P //
         ((u / Nat.gcd (l * ∏ i : A, (f i : ℕ)) u : ℕ) : ℝ) < Real.exp (9 * V / 10)} : ℝ) /
           (Fintype.card (ι → P) : ℝ) ≤ Real.exp (-V / 20) := by
   …