OAI/Combinatorics/IndependentSets/Reduction/Cube.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.BooleanJunta.Cube line 8
  2. instance OAI.LargeIndependentSets.BooleanJunta.cubeFintype line 12
  3. instance OAI.LargeIndependentSets.BooleanJunta.cubeNonempty line 18
  4. def OAI.LargeIndependentSets.BooleanJunta.mean line 22
  5. lemma OAI.LargeIndependentSets.BooleanJunta.mean_zero line 24
  6. lemma OAI.LargeIndependentSets.BooleanJunta.mean_succ line 28
  7. lemma OAI.LargeIndependentSets.BooleanJunta.mean_add line 35
  8. lemma OAI.LargeIndependentSets.BooleanJunta.mean_sub line 38
  9. lemma OAI.LargeIndependentSets.BooleanJunta.mean_mul line 41
  10. lemma OAI.LargeIndependentSets.BooleanJunta.mean_nonneg line 44
  11. lemma OAI.LargeIndependentSets.BooleanJunta.mean_mono line 47
  12. lemma OAI.LargeIndependentSets.BooleanJunta.mean_cauchy line 50
  13. def OAI.LargeIndependentSets.BooleanJunta.evenPart line 54
  14. def OAI.LargeIndependentSets.BooleanJunta.oddPart line 57
  15. def OAI.LargeIndependentSets.BooleanJunta.noise line 60
  16. lemma OAI.LargeIndependentSets.BooleanJunta.mean_square_split line 64
  17. lemma OAI.LargeIndependentSets.BooleanJunta.mean_noise_fourth line 73
  18. theorem OAI.LargeIndependentSets.BooleanJunta.hypercontractive_two_four line 85
  19. lemma OAI.LargeIndependentSets.BooleanJunta.evenPart_noise line 118
  20. lemma OAI.LargeIndependentSets.BooleanJunta.oddPart_noise line 124
  21. lemma OAI.LargeIndependentSets.BooleanJunta.mean_product_split line 130
  22. lemma OAI.LargeIndependentSets.BooleanJunta.noise_selfadjoint line 141
  23. lemma OAI.LargeIndependentSets.BooleanJunta.mean_holder_four line 158
  24. theorem OAI.LargeIndependentSets.BooleanJunta.noise_small_l1 line 196