OAI/Probability/GammaPassage/GridIndependence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.Grid.DependsOnEdges line 10
2. def OAI.GammaFPP.Grid.extendEdgeWeights line 13
3. theorem OAI.GammaFPP.Grid.measurable_extendEdgeWeights line 16
4. theorem OAI.GammaFPP.Grid.DependsOnEdges.restriction_iff line 24
5. theorem OAI.GammaFPP.Grid.DependsOnEdges.compl line 31
6. theorem OAI.GammaFPP.Grid.dependsOnEdges_biInter line 36
7. theorem OAI.GammaFPP.Grid.disjoint_edge_events_independent line 52
8. theorem OAI.GammaFPP.Grid.disjoint_edge_events_inter_probability line 74
9. theorem OAI.GammaFPP.Grid.disjoint_edge_events_iIndepSet line 107
10. theorem OAI.GammaFPP.Grid.disjoint_trials_failure_bound line 120

    Source documentation

    The amplification step in cr:rare-fast: M disjoint trials with individual success probability at least p have joint failure probability at most (1-p)^M.

    theorem disjoint_trials_failure_bound (h : GammaEnvironment shape rate P τ)
        {ι : Type*} (t : Finset ι) (A : ι → Set (Edge → ℝ)) (S : ι → Finset Edge)
        (hA : ∀ i ∈ t, MeasurableSet (A i)) (hAS : ∀ i ∈ t, DependsOnEdges (A i) (S i))
        (hdis : Set.Pairwise (↑t : Set ι) (fun i j => Disjoint (S i) (S j)))
        (p : ℝ)
        (hprob : ∀ i ∈ t, p ≤ P.real {ω | (fun e => τ e ω) ∈ A i}) :
        P.real {ω | ∀ i ∈ t, (fun e => τ e ω) ∉ A i} ≤ (1-p)^t.card := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.Grid.DependsOnEdges