OAI/Combinatorics/SumProduct/Alignment/CubeLocal01.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeLocalHaar.conjugateLattice line 28
  2. lemma OAI.CubeLocalHaar.mem_conjugateLattice line 32
  3. def OAI.CubeLocalHaar.baseImage line 39
  4. lemma OAI.CubeLocalHaar.baseImage_mk line 50
  5. lemma OAI.CubeLocalHaar.baseImage_continuous line 54
  6. lemma OAI.CubeLocalHaar.baseImage_injective line 62
  7. def OAI.CubeLocalHaar.haarImage line 76
  8. lemma OAI.CubeLocalHaar.haarImage_mk line 80
  9. lemma OAI.CubeLocalHaar.haarImage_continuous line 86
  10. def OAI.FiniteHaarTests.discrepancy line 111
  11. lemma OAI.FiniteHaarTests.discrepancy_bound line 124
  12. theorem OAI.FiniteHaarTests.compact_tests line 139
  13. theorem OAI.FiniteHaarTests.continuous_test line 154
  14. theorem OAI.CubeLocalHaar.haar_limit_compact line 201
  15. lemma OAI.CubeLocalHaar.cubeQuotient_compact line 262
  16. def OAI.CubeLocalHaar.frozenTest line 274
  17. lemma OAI.CubeLocalHaar.frozenTest_continuous line 279
  18. theorem OAI.CubeLocalHaar.uniform_freezing line 287
  19. def OAI.CubeLocalHaar.imageProbability line 306
  20. lemma OAI.CubeLocalHaar.integral_imageProbability line 312