OAI/Combinatorics/IndependentSets/Reduction/FiniteNoise.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Reduction.FiniteNoise.realizedBit line 11
2. def OAI.IndependentSetsGames.Reduction.FiniteNoise.realizedNoise line 13
3. theorem OAI.IndependentSetsGames.Reduction.FiniteNoise.realizedBit_eq_true_iff line 16
4. theorem OAI.IndependentSetsGames.Reduction.FiniteNoise.coordinate_fiber_sum line 20
5. theorem OAI.IndependentSetsGames.Reduction.FiniteNoise.noiseWeight_eq_fiber_sum line 44
6. theorem OAI.IndependentSetsGames.Reduction.FiniteNoise.fiber_product_eq_indicator line 56
7. theorem OAI.IndependentSetsGames.Reduction.FiniteNoise.expect_realizedNoise line 69