OAI/Probability/Localization/Cells.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.cellWidth line 10
  2. def OAI.RepeatedLocalization.cellLower line 11
  3. def OAI.RepeatedLocalization.cellCenter line 13
  4. lemma OAI.RepeatedLocalization.cellWidth_pos line 16
  5. lemma OAI.RepeatedLocalization.cellSet_eq_pi line 20
  6. lemma OAI.RepeatedLocalization.measurableSet_cellSet line 28
  7. lemma OAI.RepeatedLocalization.volume_cellSet line 32
  8. lemma OAI.RepeatedLocalization.cellSet_subset_initialCube line 38
  9. lemma OAI.RepeatedLocalization.cubePrior_cellSet line 52
  10. lemma OAI.RepeatedLocalization.cellCenter_mem line 67
  11. def OAI.RepeatedLocalization.cellIndex line 74
  12. def OAI.RepeatedLocalization.cellAt line 78
  13. lemma OAI.RepeatedLocalization.measurable_cellIndex line 80
  14. lemma OAI.RepeatedLocalization.measurable_cellAt line 87
  15. lemma OAI.RepeatedLocalization.cellIndex_eq_of_mem line 91
  16. lemma OAI.RepeatedLocalization.mem_cellAt line 108
  17. lemma OAI.RepeatedLocalization.cellSet_disjoint line 137
  18. def OAI.RepeatedLocalization.childCell line 143
  19. lemma OAI.RepeatedLocalization.cellWidth_add line 150
  20. lemma OAI.RepeatedLocalization.childCell_lower line 155
  21. lemma OAI.RepeatedLocalization.childCell_subset line 163
  22. lemma OAI.RepeatedLocalization.cell_ext line 181
  23. def OAI.RepeatedLocalization.ancestorCell line 191
  24. lemma OAI.RepeatedLocalization.child_ancestorCell line 197
  25. lemma OAI.RepeatedLocalization.cellSet_subset_ancestor line 205
  26. lemma OAI.RepeatedLocalization.cellAt_eq_of_mem line 211
  27. lemma OAI.RepeatedLocalization.cellAt_nested line 218
  28. lemma OAI.RepeatedLocalization.cellSet_root line 226