OAI/Combinatorics/IndependentSets/Reduction/Circle.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LargeIndependentSets.Circle line 11
  2. instance OAI.LargeIndependentSets.circleProbability line 12
  3. def OAI.LargeIndependentSets.realToTorus line 14
  4. lemma OAI.LargeIndependentSets.circle_quotient_lipschitz line 16
  5. lemma OAI.LargeIndependentSets.realToTorus_lipschitz line 22
  6. lemma OAI.LargeIndependentSets.circle_quotient_preserving line 31
  7. lemma OAI.LargeIndependentSets.realToTorus_preserving line 35
  8. lemma OAI.LargeIndependentSets.torus_average_lift line 39
  9. theorem OAI.LargeIndependentSets.torus_junta_uniform line 53
  10. def OAI.LargeIndependentSets.circleInfluence line 74
  11. theorem OAI.LargeIndependentSets.torus_influences line 77
  12. def OAI.LargeIndependentSets.ProductAveraging.reindex line 126
  13. lemma OAI.LargeIndependentSets.ProductAveraging.reindex_preserving line 127
  14. lemma OAI.LargeIndependentSets.ProductAveraging.reindex_lipschitz line 133
  15. lemma OAI.LargeIndependentSets.ProductAveraging.reindex_mix line 141
  16. lemma OAI.LargeIndependentSets.ProductAveraging.average_reindex line 154