OAI/Computability/MinUncut/Games/FiniteNoise.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Reduction.FiniteNoise.realizedBit line 12
2. def OAI.MinUncutGames.Reduction.FiniteNoise.realizedNoise line 14
3. theorem OAI.MinUncutGames.Reduction.FiniteNoise.realizedBit_eq_true_iff line 17
4. theorem OAI.MinUncutGames.Reduction.FiniteNoise.coordinate_fiber_sum line 21
5. theorem OAI.MinUncutGames.Reduction.FiniteNoise.noiseWeight_eq_fiber_sum line 45
6. theorem OAI.MinUncutGames.Reduction.FiniteNoise.fiber_product_eq_indicator line 57
7. theorem OAI.MinUncutGames.Reduction.FiniteNoise.expect_realizedNoise line 70