OAI/NumberTheory/TwoPoint/Bounds/SieveModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.FiniteLaw.dependentIndependent line 17

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:17 (same declaration text).

2. lemma OAI.TwoPointCorrelations.FiniteLaw.dependentIndependent_average_product line 26

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:26 (same declaration text).

3. lemma OAI.TwoPointCorrelations.FiniteLaw.dependentIndependent_probability_all line 34

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:34 (same declaration text).

4. lemma OAI.TwoPointCorrelations.FiniteLaw.probability_complement line 49

   Distinct definitions of this name: OAI/NumberTheory/TwoPoint/Circuits/CircuitIsolation.lean:50 (different declaration text), OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:49 (same declaration text). Qualify references as OAI.TwoPointCorrelations.FiniteLaw.probability_complement@path.

5. lemma OAI.TwoPointCorrelations.FiniteLaw.dependentIndependent_intersection line 62

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:62 (same declaration text).

6. lemma OAI.TwoPointCorrelations.FiniteLaw.dependentIndependent_avoid line 78

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:78 (same declaration text).

7. def OAI.TwoPointCorrelations.elementarySymmetric line 90

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:90 (same declaration text).

8. lemma OAI.TwoPointCorrelations.independent_intersectionMass line 93

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:93 (same declaration text).

9. theorem OAI.TwoPointCorrelations.elementarySymmetric_exp_bound line 104

   Source documentation

   Exponential weighting bounds one elementary symmetric layer. This avoids factorial estimates and gives the same finite-sieve tail.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:104 (same declaration text).

   theorem elementarySymmetric_exp_bound {ι : Type*} (P : Finset ι) (a : ι → ℝ)
       (ha : ∀ i ∈ P, 0 ≤ a i) (j : ℕ) (t : ℝ) (ht : 0 < t) :
       elementarySymmetric P a j ≤ Real.exp (t * ∑ i ∈ P, a i) / t ^ j := by
   …

   Mentions: OAI.TwoPointCorrelations.elementarySymmetric

10. lemma OAI.TwoPointCorrelations.elementarySymmetric_two_bound line 138

    Source documentation

    A direct useful specialization: tail order j and total local mass M give exp(2M) / 2^j.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:138 (same declaration text).

    lemma elementarySymmetric_two_bound {ι : Type*} (P : Finset ι) (a : ι → ℝ)
        (ha : ∀ i ∈ P, 0 ≤ a i) (j : ℕ) :
        elementarySymmetric P a j ≤ Real.exp (2 * ∑ i ∈ P, a i) / (2 : ℝ) ^ j :=
    …

    Mentions: OAI.TwoPointCorrelations.elementarySymmetric

11. theorem OAI.TwoPointCorrelations.elementarySymmetric_log_tail line 146

    Source documentation

    The next-layer tail is already at most L⁻¹⁰⁰ once its order exceeds 220 log L and the total local mass is at most 5 log L. The manuscript uses the considerably larger order 1000 log L.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:146 (same declaration text).

    theorem elementarySymmetric_log_tail {ι : Type*} (P : Finset ι) (a : ι → ℝ)
        (ha : ∀ i ∈ P, 0 ≤ a i) (j : ℕ) (L : ℝ) (hL : 1 ≤ L)
        (hmass : (∑ i ∈ P, a i) ≤ 5 * Real.log L)
        (hj : 220 * Real.log L ≤ (j : ℝ)) :
        elementarySymmetric P a j ≤ L ^ (-100 : ℝ) := by
    …

    Mentions: OAI.TwoPointCorrelations.elementarySymmetric

12. theorem OAI.TwoPointCorrelations.finite_independent_sieve_bound line 171

    Source documentation

    Finite sieve upper bound with the independent local model fully evaluated. The only arithmetic premise is the error of each actual intersection count.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/SieveModel.lean:171 (same declaration text).

    theorem finite_independent_sieve_bound {ι α : Type*}
        [Fintype ι] [DecidableEq ι] [Fintype α]
        {A : ι → Type*} [∀ i, Fintype (A i)]
        (actual : FiniteLaw α) (E : ι → α → Prop)
        (laws : ∀ i, FiniteLaw (A i)) (bad : ∀ i, A i → Prop)
        (r : ℕ) (err : Finset ι → ℝ)
        (herr : ∀ S ∈ (univ : Finset ι).powerset, S.card ≤ 2 * r →
          |actual.probability (eventIntersection E S) -
            ∏ i ∈ S, (laws i).probability (bad i)| ≤ err S) :
        actual.probability (avoidsEvents univ E) ≤
          (∏ i, (1 - (laws i).probability (bad i))) +
          elementarySymmetric univ (fun i => (laws i).probability (bad i)) (2 * r + 1) +
    …

    Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.eventIntersection, OAI.TwoPointCorrelations.avoidsEvents, OAI.TwoPointCorrelations.elementarySymmetric