OAI/NumberTheory/EgyptianFractions/FiniteGoodExposure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Reindex independent coordinates in a uniform finite product average.

   lemma expect_product_reindex {A B X : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
       [Fintype X] (e : A ≃ B) (g : X → ℕ) (F : ℕ → ℂ) :
       (𝔼 w : A → X, F (∏ i, g (w i))) =
         𝔼 w : B → X, F (∏ i, g (w i)) := by
   …

   Mentions: OAI.Problem337.F

2. lemma OAI.Problem337.RandomProducts.double_expect_fin_eq_sum line 23

   Source documentation

   Conversion of two uniform finite function averages to the explicit normalization used in the bilinear exponential-sum estimate.

   lemma double_expect_fin_eq_sum (P : Finset ℕ) (s : ℕ)
       (F : (Fin s → ↥P) → (Fin s → ↥P) → ℂ) :
       (𝔼 a : Fin s → ↥P, 𝔼 b : Fin s → ↥P, F a b) =
         (∑ a : Fin s → ↥P, ∑ b : Fin s → ↥P, F a b) /
           ((P.card : ℂ)^s)^2 := by
   …

   Mentions: OAI.Problem337.F

3. lemma OAI.Problem337.RandomProducts.double_expect_product_reindex line 34

   Source documentation

   Reindex two independent coordinate families simultaneously.

   lemma double_expect_product_reindex {A B C D X : Type*}
       [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype X]
       [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]
       (eA : A ≃ C) (eB : B ≃ D) (g : X → ℕ) (F : ℕ → ℕ → ℂ) :
       (𝔼 a : A → X, 𝔼 b : B → X, F (∏ i, g (a i)) (∏ i, g (b i))) =
         𝔼 a : C → X, 𝔼 b : D → X, F (∏ i, g (a i)) (∏ i, g (b i)) := by
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.F

4. theorem OAI.Problem337.RandomProducts.concrete_good_exposure_expect line 51

   Source documentation

   The actual good-exposure bound with arbitrary finite coordinate types, in the nested uniform-expectation form used after conditioning.

   theorem concrete_good_exposure_expect {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
       (S V : ℝ) (hA : Fintype.card A = freshLength S V)
       (hB : Fintype.card B = freshLength 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)
       (c u : ℕ) (hu : 0 < u) [NeZero u]
       (huV : (u : ℝ) ≤ Real.exp V)
       (hq : Real.exp ((9 / 10 : ℝ) * V) ≤ ((u / c.gcd u : ℕ) : ℝ))
       (t : ZMod u) :
       ‖𝔼 a : A → ↥P, 𝔼 b : B → ↥P,
   …

   Mentions: OAI.Problem337.RandomProducts.freshLength