OAI/Probability/CriticalZ3/TrialCounts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ShellEstimates.exists_layer line 16

   Source documentation

   Averaging disjoint blocking events supplies a deterministic shell layer.

   theorem exists_layer {I : Type uI} [Fintype I] [Nonempty I]
       (Q A : I → Set Ω) (hAm : ∀ i, MeasurableSet (A i))
       (hAd : Pairwise (fun i j => Disjoint (A i) (A j))) {α : ℝ} (hα : 0 < α)
       (hblock : ∀ i, α*μ.real (Q i) ≤ μ.real (A i)) :
       ∃ i, μ.real (Q i) ≤ 1/(α*Fintype.card I) := by
   …

2. theorem OAI.ShellEstimates.success_count_bound line 37
3. theorem OAI.ShellEstimates.bad_count_bound line 60
4. theorem OAI.ShellEstimates.no_good_subset line 73
5. def OAI.TrialCounts.count line 88
6. theorem OAI.TrialCounts.count_memLp line 91
7. theorem OAI.TrialCounts.count_nonneg line 98
8. theorem OAI.TrialCounts.indicator_mean line 104
9. theorem OAI.TrialCounts.count_mean line 108
10. theorem OAI.TrialCounts.indicator_product line 119
11. theorem OAI.TrialCounts.count_variance_le line 126

    Source documentation

    Pairwise independence is all that the success-count step needs.

    theorem count_variance_le (A : I → Set Ω) (hA : ∀ i, MeasurableSet (A i))
        {c : ℝ} (hc : ∀ i, μ.real (A i) = c)
        (hpair : ∀ i j, i ≠ j → μ.real (A i ∩ A j) ≤ c*c) :
        variance (count A) μ ≤ Fintype.card I*c := by
    …

    Mentions: OAI.TrialCounts.count

12. theorem OAI.TrialCounts.no_good_probability line 155

    Source documentation

    No independence is required among bad successes or their quality tests.

    theorem no_good_probability (A B : I → Set Ω)
        (hA : ∀ i, MeasurableSet (A i)) (hB : ∀ i, MeasurableSet (B i))
        {c γ τ : ℝ} (hcpos : 0 < Fintype.card I*c) (hτ : 0 < τ)
        (hc : ∀ i, μ.real (A i) = c)
        (hpair : ∀ i j, i ≠ j → μ.real (A i ∩ A j) ≤ c*c)
        (hbad : ∀ i, μ.real (B i) ≤ c*γ/τ) :
        μ.real {ω | ∀ i, ω ∈ A i → ω ∈ B i} ≤ 4/(Fintype.card I*c)+2*γ/τ := by
    …