OAI/Combinatorics/IndependentSets/Reduction/Heavy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.BooleanJunta.heavy line 9
  2. lemma OAI.LargeIndependentSets.BooleanJunta.heavy_card_bound line 12
  3. lemma OAI.LargeIndependentSets.BooleanJunta.high_degree_tail line 22
  4. lemma OAI.LargeIndependentSets.BooleanJunta.low_degree_diff_sum line 41
  5. lemma OAI.LargeIndependentSets.BooleanJunta.low_degree_outside line 52
  6. theorem OAI.LargeIndependentSets.BooleanJunta.boolean_junta_error line 95
  7. lemma OAI.LargeIndependentSets.BooleanJunta.mean_const line 112
  8. lemma OAI.LargeIndependentSets.BooleanJunta.mean_sum line 114
  9. def OAI.LargeIndependentSets.BooleanJunta.tailSet line 118
  10. lemma OAI.LargeIndependentSets.BooleanJunta.mem_tailSet line 121
  11. lemma OAI.LargeIndependentSets.BooleanJunta.supported_cons line 124
  12. def OAI.LargeIndependentSets.BooleanJunta.merge line 136
  13. lemma OAI.LargeIndependentSets.BooleanJunta.bit_merge line 140
  14. lemma OAI.LargeIndependentSets.BooleanJunta.walsh_merge_mean line 151
  15. theorem OAI.LargeIndependentSets.BooleanJunta.truncate_eq_coordinate_mean line 170
  16. lemma OAI.LargeIndependentSets.BooleanJunta.truncate_bounded line 185
  17. theorem OAI.LargeIndependentSets.BooleanJunta.boolean_junta_uniform line 195