OAI/NumberTheory/EgyptianFractions/RandomCorrelation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomProducts.correlation_of_exposed_products line 12

   Source documentation

   Transfer an exposed product factorization to a pair-correlation estimate. The bad-exposure counting and the fresh-product cancellation are separate, explicit inputs, so this lemma does not assume probabilistic independence.

   theorem correlation_of_exposed_products
       {Ω E A B : Type*} [Fintype Ω] [Fintype E] [Fintype A] [Fintype B]
       [Nonempty E] [Nonempty A] [Nonempty B]
       (e : Ω ≃ E × (A × B)) (pI pJ : Ω → ℕ)
       (U V : E → ℕ) (f : A → ℕ) (g : B → ℕ)
       (hI : ∀ c a b, pI (e.symm (c, (a, b))) = U c * f a * g b)
       (hJ : ∀ c a b, pJ (e.symm (c, (a, b))) = V c)
       (u l : ℕ) [NeZero u] (bad : Finset E) (ε δ : ℝ) (hδ : 0 ≤ δ)
       (hbad : (bad.card : ℝ) / Fintype.card E ≤ ε)
       (hgood : ∀ c, c ∉ bad →
         ‖𝔼 a : A, 𝔼 b : B,
           ZMod.stdAddChar (((l * U c * f a * g b : ℕ) : ZMod u) -
   …