OAI/Combinatorics/IndependentSets/Reduction/CellLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.BooleanJunta.uniformLaw_singleton line 10
  2. lemma OAI.LargeIndependentSets.BooleanJunta.uniformLaw_pi line 16
  3. def OAI.LargeIndependentSets.BooleanJunta.cellLaw line 24
  4. instance OAI.LargeIndependentSets.BooleanJunta.cellLaw_probability line 25
  5. def OAI.LargeIndependentSets.BooleanJunta.mergeSeed line 28
  6. lemma OAI.LargeIndependentSets.BooleanJunta.mergeSeed_preserving line 31
  7. lemma OAI.LargeIndependentSets.BooleanJunta.cells_preserving line 40
  8. def OAI.LargeIndependentSets.BooleanJunta.cellPoint line 49
  9. lemma OAI.LargeIndependentSets.BooleanJunta.scalarCell_distance line 52
  10. lemma OAI.LargeIndependentSets.BooleanJunta.sample_cell_distance line 58
  11. lemma OAI.LargeIndependentSets.BooleanJunta.seeds_in_unit line 65
  12. lemma OAI.LargeIndependentSets.BooleanJunta.sample_cell_error line 74
  13. def OAI.LargeIndependentSets.BooleanJunta.rowFlip line 82
  14. def OAI.LargeIndependentSets.BooleanJunta.rowInfluence line 84
  15. lemma OAI.LargeIndependentSets.BooleanJunta.cells_update_flip line 87
  16. lemma OAI.LargeIndependentSets.BooleanJunta.rowInfluence_eq_integral line 95
  17. lemma OAI.LargeIndependentSets.BooleanJunta.rowInfluence_cell_bound line 105
  18. lemma OAI.LargeIndependentSets.BooleanJunta.total_rowInfluence_cell_bound line 150