Bonferroni.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The finite even-order sieve, before any independence or prime estimates.

def OAI.TwoPointCorrelations.avoidsEvents line 13
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:13 (same declaration text).
def OAI.TwoPointCorrelations.eventIntersection line 16
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:16 (same declaration text).
def OAI.TwoPointCorrelations.eventIntersectionCount line 19
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:19 (same declaration text).
def OAI.TwoPointCorrelations.truncatedEventCount line 23
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:23 (same declaration text).
lemma OAI.TwoPointCorrelations.eventIntersectionCount_eq_choose line 27
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:27 (same declaration text).
lemma OAI.TwoPointCorrelations.truncatedEventCount_eq_choose line 46
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:46 (same declaration text).
lemma OAI.TwoPointCorrelations.avoidsEvents_iff_card_zero line 53
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:53 (same declaration text).
lemma OAI.TwoPointCorrelations.real_alternating_choose line 58
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:58 (same declaration text).
lemma OAI.TwoPointCorrelations.alternating_choose_zero line 63
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:63 (same declaration text).
lemma OAI.TwoPointCorrelations.even_binomial_lower line 73
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:73 (same declaration text).
lemma OAI.TwoPointCorrelations.odd_binomial_upper line 84
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:84 (same declaration text).
theorem OAI.TwoPointCorrelations.bonferroni_even_pointwise line 98
Source documentation
Even truncation dominates the actual avoidance indicator pointwise.
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:98 (same declaration text).
```
theorem bonferroni_even_pointwise {ι α : Type*}
    (P : Finset ι) (E : ι → α → Prop) (r : ℕ) (x : α) :
    (if avoidsEvents P E x then (1 : ℝ) else 0) ≤ truncatedEventCount P E (2 * r) x := by
…
```
Mentions: OAI.TwoPointCorrelations.avoidsEvents, OAI.TwoPointCorrelations.truncatedEventCount
theorem OAI.TwoPointCorrelations.bonferroni_odd_pointwise line 105
Source documentation
Odd truncation gives the opposite bound.
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:105 (same declaration text).
```
theorem bonferroni_odd_pointwise {ι α : Type*}
    (P : Finset ι) (E : ι → α → Prop) (r : ℕ) (x : α) :
    truncatedEventCount P E (2 * r + 1) x ≤
      if avoidsEvents P E x then (1 : ℝ) else 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.truncatedEventCount, OAI.TwoPointCorrelations.avoidsEvents
lemma OAI.TwoPointCorrelations.truncatedEventCount_odd line 112
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:112 (same declaration text).
theorem OAI.TwoPointCorrelations.bonferroni_remainder_pointwise line 126
Source documentation
The excess of the even truncation is bounded by the very next intersection layer. No convergence argument is involved.
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:126 (same declaration text).
```
theorem bonferroni_remainder_pointwise {ι α : Type*}
    (P : Finset ι) (E : ι → α → Prop) (r : ℕ) (x : α) :
    truncatedEventCount P E (2 * r) x ≤
      (if avoidsEvents P E x then (1 : ℝ) else 0) +
        eventIntersectionCount P E (2 * r + 1) x := by
…
```
Mentions: OAI.TwoPointCorrelations.truncatedEventCount, OAI.TwoPointCorrelations.avoidsEvents, OAI.TwoPointCorrelations.eventIntersectionCount
def OAI.TwoPointCorrelations.eventIntersectionMass line 135
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:135 (same declaration text).
def OAI.TwoPointCorrelations.truncatedEventMass line 139
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:139 (same declaration text).
lemma OAI.TwoPointCorrelations.average_eventIntersectionCount line 143
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:143 (same declaration text).
lemma OAI.TwoPointCorrelations.average_truncatedEventCount line 150
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:150 (same declaration text).
theorem OAI.TwoPointCorrelations.bonferroni_even line 167
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:167 (same declaration text).
theorem OAI.TwoPointCorrelations.bonferroni_remainder line 173
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:173 (same declaration text).
def OAI.TwoPointCorrelations.sieveIntersectionError line 183
Source documentation
Total error in the finitely many intersection counts used by a sieve truncation. Each subset appears just once.
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:183 (same declaration text).
```
noncomputable def sieveIntersectionError {ι : Type*}
    (P : Finset ι) (err : Finset ι → ℝ) (r : ℕ) : ℝ :=
…
```
lemma OAI.TwoPointCorrelations.truncatedEventMass_comparison line 187
Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:187 (same declaration text).

theorem OAI.TwoPointCorrelations.bonferroni_transfer line 221

Source documentation

Exact finite sieve transfer. An independent residue model can be inserted only after its intersections have actually been counted.

Also declared: OAI/NumberTheory/TwoPointCorrelations/Bonferroni.lean:221 (same declaration text).

theorem bonferroni_transfer {ι α β : Type*} [Fintype α] [Fintype β]
    (μ : FiniteLaw α) (ν : FiniteLaw β) (P : Finset ι)
    (E : ι → α → Prop) (F : ι → β → Prop) (r : ℕ) (err : Finset ι → ℝ)
    (herr : ∀ S ∈ P.powerset, S.card ≤ 2 * r →
      |μ.probability (eventIntersection E S) -
        ν.probability (eventIntersection F S)| ≤ err S) :
    μ.probability (avoidsEvents P E) ≤ ν.probability (avoidsEvents P F) +
      eventIntersectionMass ν P F (2 * r + 1) + sieveIntersectionError P err (2 * r) := by
…

Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.eventIntersection, OAI.TwoPointCorrelations.avoidsEvents, OAI.TwoPointCorrelations.eventIntersectionMass, OAI.TwoPointCorrelations.sieveIntersectionError