OAI/NumberTheory/Ostmann/Construction/OriginalMomentBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_two_pow_moment_budget line 13
2. theorem OAI.Ostmann.original_outer_moment_budget line 28
3. theorem OAI.Ostmann.original_moment_witness_probability line 58

   Source documentation

   After subtracting the large, outer, and failed-witness contributions, the second moment gives the manuscript's positive witness probability.

   theorem original_moment_witness_probability {ι : Type*} (S : Finset ι) (E : ι → Prop)
       [DecidablePred E] (F f g o : ι → ℝ) (T K : ℝ)
       (hK : 3000 ≤ K) (hKT : K ≤ T)
       (hpoint : ∀ i ∈ S, F i ≤ f i + g i + o i)
       (hfirst : Real.exp ((3 / 200 : ℝ) * K) ≤ (S.card : ℝ)⁻¹ * (∑ i ∈ S, F i))
       (hsecond : (S.card : ℝ)⁻¹ * (∑ i ∈ S, f i ^ 2) ≤
         (Real.exp ((103 / 1000 : ℝ) * K) + Real.exp (-10 * T) + Real.exp (-113 * T)) ^ 2)
       (hlarge : (S.card : ℝ)⁻¹ * (∑ i ∈ S, g i) ≤
         Real.exp ((9 / 1000 : ℝ) * K) + Real.exp (-10 * T) + Real.exp (-113 * T))
       (houter : (S.card : ℝ)⁻¹ * (∑ i ∈ S, o i) ≤ 1)
       (hfail : (S.card : ℝ)⁻¹ * (∑ i ∈ S.filter (fun i => ¬E i), f i) ≤
         Real.exp ((-797 / 1000 : ℝ) * K) + Real.exp (-10 * T) + Real.exp (-113 * T)) :
   …