OAI/Probability/RadialTransition/BoxEnsembles.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.halfCube line 14
  2. lemma OAI.RadialTransition.measurableSet_halfCube line 16
  3. lemma OAI.RadialTransition.halfCube_ae_cube line 25
  4. lemma OAI.RadialTransition.restrict_halfCube line 35
  5. abbrev OAI.RadialTransition.GridIndex line 38
  6. def OAI.RadialTransition.gridEmbed line 40
  7. lemma OAI.RadialTransition.gridEmbed_injective line 42
  8. lemma OAI.RadialTransition.halfCube_grid_cover line 49
  9. lemma OAI.RadialTransition.gridEmbed_mem_halfCube_iff line 62
  10. lemma OAI.RadialTransition.halfCube_eq_gridUnion line 73
  11. lemma OAI.RadialTransition.volume_halfCube line 79
  12. def OAI.RadialTransition.macroOf line 82
  13. def OAI.RadialTransition.blockEmbed line 84
  14. lemma OAI.RadialTransition.blockEmbed_macro line 91
  15. lemma OAI.RadialTransition.blockEmbed_injective line 102
  16. lemma OAI.RadialTransition.blockEmbed_surjective line 115
  17. def OAI.RadialTransition.boundaryCoord line 125
  18. lemma OAI.RadialTransition.card_boundaryCoord line 128
  19. def OAI.RadialTransition.boundarySlice line 148
  20. def OAI.RadialTransition.boundaryGrid line 151
  21. lemma OAI.RadialTransition.mem_boundaryGrid line 154
  22. lemma OAI.RadialTransition.card_boundaryGrid line 171
  23. lemma OAI.RadialTransition.inner_block_macro line 181
  24. lemma OAI.RadialTransition.sum_blockGrid line 200
  25. lemma OAI.RadialTransition.grid_sum_boundary_bound line 207