FairBitProbability.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.fairBalancingBad line 14
Source documentation
A support fails balancing when one bit occurs fewer than a quarter of its distinct labels.
```
noncomputable def fairBalancingBad (S : Finset Label) : Finset (Label → Bool) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.mem_fairBalancingBad line 19
theorem OAI.QuantitativeVanDerWaerden.not_mem_fairBalancingBad_iff line 26
Source documentation
Avoiding the event says that both bits occupy at least a quarter.
```
theorem not_mem_fairBalancingBad_iff (S : Finset Label) (ω : Label → Bool) :
    ω ∉ fairBalancingBad S ↔
      ∀ b : Bool, S.card ≤ 4 * (S.filter fun i => ω i = b).card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.fairBalancingBad
theorem OAI.QuantitativeVanDerWaerden.fairBalancingBad_depends line 32
Source documentation
Agreement on the tested labels preserves membership in the bad event.
```
theorem fairBalancingBad_depends (S : Finset Label) (ω η : Label → Bool)
    (h : ∀ i ∈ S, ω i = η i) :
    ω ∈ fairBalancingBad S ↔ η ∈ fairBalancingBad S := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.fairBalancingBad
theorem OAI.QuantitativeVanDerWaerden.bernoulli_half_eq_fairWeight line 43
theorem OAI.QuantitativeVanDerWaerden.fair_balancing_tail line 52
Source documentation
The actual bad-event probability under independent fair Boolean labels.
```
theorem fair_balancing_tail (S : Finset Label) :
    FiniteProbability.prob (FiniteProbability.bernoulliWeight (1 / 2))
      (fairBalancingBad S) ≤ 2 * Real.exp (-(S.card : ℝ) / 8) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob, OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight, OAI.QuantitativeVanDerWaerden.fairBalancingBad