UnionBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_exists_le line 12
Source documentation
The indexed union bound uses no independence among the events.
```
theorem prob_exists_le (μ : FiniteLaw Ω) (P : ι → Ω → Prop) :
    μ.prob (fun ω => ∃ i, P i ω) ≤ ∑ i, μ.prob (P i) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_forall_ge line 39
Source documentation
Simultaneous success is bounded using only the individual marginals.
```
theorem prob_forall_ge (μ : FiniteLaw Ω) (P : ι → Ω → Prop) :
    1 - ∑ i, (1 - μ.prob (P i)) ≤ μ.prob (fun ω => ∀ i, P i ω) := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.FiniteLaw
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_forall_ge_of_const line 50
theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.exists_forall_of_const line 56