OAI/Combinatorics/SumProduct/Alignment/EmbeddedCube01.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BaseCubeLaw.level_compact_reps line 35
  2. def OAI.BaseCubeLaw.Irrational line 43
  3. theorem OAI.BaseCubeLaw.exists_scaled_cube_law line 58
  4. structure OAI.AllLevelFactorization.Factorization.ResidueCover line 115
  5. theorem OAI.AllLevelFactorization.Factorization.residueCover_exists line 129
  6. def OAI.AllLevelFactorization.Factorization.residueCover line 147
  7. theorem OAI.AllLevelFactorization.Factorization.ResidueCover.irrational line 155
  8. def OAI.CosetCover.map line 190
  9. lemma OAI.CosetCover.map_mk line 195
  10. lemma OAI.CosetCover.continuous_map line 198
  11. lemma OAI.CosetCover.surjective_map line 202
  12. lemma OAI.CosetCover.map_smul line 207
  13. def OAI.CosetCover.probability line 213
  14. lemma OAI.CosetCover.probability_invariant line 217
  15. abbrev OAI.EmbeddedCubeHaar.inducedLattice line 234
  16. def OAI.EmbeddedCubeHaar.baseImage line 236
  17. lemma OAI.EmbeddedCubeHaar.baseImage_mk line 247
  18. lemma OAI.EmbeddedCubeHaar.baseImage_continuous line 252
  19. lemma OAI.EmbeddedCubeHaar.baseImage_injective line 260
  20. theorem OAI.EmbeddedCubeHaar.cubeInclusion line 275
  21. def OAI.EmbeddedCubeHaar.coverImage line 278
  22. lemma OAI.EmbeddedCubeHaar.coverImage_mk line 282
  23. lemma OAI.EmbeddedCubeHaar.coverImage_continuous line 287
  24. def OAI.EmbeddedCubeHaar.haarImage line 290
  25. lemma OAI.EmbeddedCubeHaar.haarImage_mk line 295
  26. lemma OAI.EmbeddedCubeHaar.haarImage_continuous line 303
  27. def OAI.EmbeddedCubeHaar.imageProbability line 315
  28. lemma OAI.EmbeddedCubeHaar.integral_imageProbability line 322
  29. lemma OAI.EmbeddedCubeHaar.imageProbability_continuous line 336