OAI/Combinatorics/IndependentSets/Reduction/ArbitraryRealJunta.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargeIndependentSets.arbitrary_real_junta line 11
  2. abbrev OAI.LargeIndependentSets.PhaseTest.Circle line 45
  3. instance OAI.LargeIndependentSets.PhaseTest.circleProbability line 46
  4. def OAI.LargeIndependentSets.PhaseTest.rotationLaw line 48
  5. instance OAI.LargeIndependentSets.PhaseTest.rotationProbability line 49
  6. def OAI.LargeIndependentSets.PhaseTest.representative line 51
  7. lemma OAI.LargeIndependentSets.PhaseTest.representative_mem line 52
  8. lemma OAI.LargeIndependentSets.PhaseTest.representative_measurable line 54
  9. lemma OAI.LargeIndependentSets.PhaseTest.representative_coe line 56
  10. lemma OAI.LargeIndependentSets.PhaseTest.representative_eq line 57
  11. lemma OAI.LargeIndependentSets.PhaseTest.quotient_preserving line 60
  12. lemma OAI.LargeIndependentSets.PhaseTest.representative_preserving line 64
  13. def OAI.LargeIndependentSets.PhaseTest.rotate line 72
  14. lemma OAI.LargeIndependentSets.PhaseTest.rotate_preserving line 73
  15. lemma OAI.LargeIndependentSets.PhaseTest.rotate_coe line 75
  16. def OAI.LargeIndependentSets.PhaseTest.phase line 81
  17. def OAI.LargeIndependentSets.PhaseTest.auxiliary line 83
  18. def OAI.LargeIndependentSets.PhaseTest.blockShift line 86
  19. lemma OAI.LargeIndependentSets.PhaseTest.blockShift_preserving line 90
  20. lemma OAI.LargeIndependentSets.PhaseTest.full_block_absorption line 102
  21. lemma OAI.LargeIndependentSets.PhaseTest.absorption_integral line 120
  22. lemma OAI.LargeIndependentSets.PhaseTest.auxiliary_lipschitz line 137
  23. lemma OAI.LargeIndependentSets.PhaseTest.auxiliary_mean_zero line 147