Coin.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CubeShuffle.QueryTree.flipCoin line 12
Source documentation
Flipping one bit is a permutation of the uniform coin space.
```
def flipCoin (i : ι) : Equiv.Perm (ι → Bool) :=
…
```
lemma OAI.CubeShuffle.QueryTree.flipCoin_apply_eq line 20
lemma OAI.CubeShuffle.QueryTree.flipCoin_apply_ne line 24
lemma OAI.CubeShuffle.QueryTree.mean_indicator_bit line 32
Source documentation
Half the uniform coin assignments have a specified bit, independently of any function which does not inspect that bit. This remains valid for adaptive functions of all the remaining bits.
```
lemma mean_indicator_bit [Fintype ι] (f : (ι → Bool) → ℝ) (i : ι) (b : Bool)
    (hf : ∀ ω, f (flipCoin i ω) = f ω) :
    finiteMean (fun ω => if ω i = b then f ω else 0) = finiteMean f / 2 := by
…
```
Mentions: OAI.CubeShuffle.QueryTree.flipCoin, OAI.CubeShuffle.finiteMean