OAI/Computability/VertexCover/Reduction/FiniteNoise.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Reduction.FiniteNoise.realizedBit line 39
2. def OAI.UniqueGames.Reduction.FiniteNoise.realizedNoise line 41
3. theorem OAI.UniqueGames.Reduction.FiniteNoise.realizedBit_eq_true_iff line 44
4. theorem OAI.UniqueGames.Reduction.FiniteNoise.coordinate_fiber_sum line 48
5. theorem OAI.UniqueGames.Reduction.FiniteNoise.noiseWeight_eq_fiber_sum line 72
6. theorem OAI.UniqueGames.Reduction.FiniteNoise.fiber_product_eq_indicator line 84
7. theorem OAI.UniqueGames.Reduction.FiniteNoise.expect_realizedNoise line 97