FairBitTail.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.FairBitTail.weight line 21
Source documentation
Each independent fair-bit assignment has this product weight.
```
def weight (_ω : Label → Bool) : ℝ := ∏ _i : Label, (1 / 2 : ℝ)
```
theorem OAI.QuantitativeVanDerWaerden.FairBitTail.weight_nonneg line 23
def OAI.QuantitativeVanDerWaerden.FairBitTail.deviation line 29
Source documentation
The centered deficit contributed by one bit.
```
def deviation (b x : Bool) : ℝ := if x = b then -(1 / 2 : ℝ) else 1 / 2
```
theorem OAI.QuantitativeVanDerWaerden.FairBitTail.sum_deviation line 31
theorem OAI.QuantitativeVanDerWaerden.FairBitTail.exponential_moment line 49
Source documentation
The exact moment generating function on any distinct label support.
```
theorem exponential_moment (S : Finset Label) (b : Bool) :
    (∑ ω : Label → Bool, weight ω *
      Real.exp (∑ i ∈ S, deviation b (ω i))) =
        Real.cosh (1 / 2 : ℝ) ^ S.card := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FairBitTail.weight, OAI.QuantitativeVanDerWaerden.FairBitTail.deviation
theorem OAI.QuantitativeVanDerWaerden.FairBitTail.exponential_moment_le line 75

theorem OAI.QuantitativeVanDerWaerden.FairBitTail.one_bit_tail line 88

Source documentation

Exponential Markov for the lower tail of either selected bit.

theorem one_bit_tail (S : Finset Label) (b : Bool) :
    (∑ ω : Label → Bool,
      if 4 * (S.filter fun i => ω i = b).card < S.card then weight ω else 0) ≤
        Real.exp (-(S.card : ℝ) / 8) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.FairBitTail.weight

theorem OAI.QuantitativeVanDerWaerden.FairBitTail.balancing_tail line 127
Source documentation
Some bit has fewer than a quarter of the tested labels with probability at most 2 exp(-|S|/8). The empty support is included.
```
theorem balancing_tail (S : Finset Label) :
    (∑ ω : Label → Bool,
      if ∃ b : Bool, 4 * (S.filter fun i => ω i = b).card < S.card
      then weight ω else 0) ≤ 2 * Real.exp (-(S.card : ℝ) / 8) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FairBitTail.weight