OAI/Combinatorics/IndependentSets/Reduction/FullAbsorptionSquare.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.PhaseTest.full_absorption_square line 13
  2. lemma OAI.LargeIndependentSets.PhaseTest.continuous_full_bound line 31
  3. lemma OAI.LargeIndependentSets.BooleanJunta.arbitrary_sampler_preserving line 60
  4. lemma OAI.LargeIndependentSets.BooleanJunta.arbitrary_cells_preserving line 64
  5. lemma OAI.LargeIndependentSets.BooleanJunta.arbitrary_seeds_in_unit line 70
  6. lemma OAI.LargeIndependentSets.PhaseTest.discrete_square_le_continuous line 87
  7. def OAI.LargeIndependentSets.BooleanJunta.gridIndex line 136
  8. lemma OAI.LargeIndependentSets.BooleanJunta.gridIndex_lt line 139
  9. lemma OAI.LargeIndependentSets.BooleanJunta.gridIndex_injective line 147
  10. lemma OAI.LargeIndependentSets.BooleanJunta.cube_card line 159
  11. def OAI.LargeIndependentSets.BooleanJunta.gridEquiv line 166
  12. lemma OAI.LargeIndependentSets.BooleanJunta.scalarCell_zero_grid line 170