OAI/Probability/Localization/Experiment.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RepeatedLocalization.continuous_chart line 10
  2. lemma OAI.RepeatedLocalization.measurable_chart line 19
  3. lemma OAI.RepeatedLocalization.continuous_exactLabel line 22
  4. lemma OAI.RepeatedLocalization.measurable_initialCube line 32
  5. lemma OAI.RepeatedLocalization.volume_initialCube line 37
  6. lemma OAI.RepeatedLocalization.volume_initialCube_pos line 46
  7. lemma OAI.RepeatedLocalization.volume_initialCube_ne_top line 51
  8. lemma OAI.RepeatedLocalization.cubePrior_isProbabilityMeasure line 55
  9. instance OAI.RepeatedLocalization.gaussianBlockLaw_isProbabilityMeasure line 60
  10. lemma OAI.RepeatedLocalization.BlockRule.prob_le_one line 65
  11. lemma OAI.RepeatedLocalization.measurable_actualRule line 70
  12. lemma OAI.RepeatedLocalization.integrable_actualRule line 76
  13. lemma OAI.RepeatedLocalization.measurable_blockProbability line 86
  14. lemma OAI.RepeatedLocalization.blockProbability_nonneg line 90
  15. lemma OAI.RepeatedLocalization.blockProbability_sum line 94
  16. lemma OAI.RepeatedLocalization.blockProbability_le_one line 100
  17. lemma OAI.RepeatedLocalization.measurable_historyLikelihood line 106
  18. lemma OAI.RepeatedLocalization.historyLikelihood_nonneg line 110
  19. lemma OAI.RepeatedLocalization.historyLikelihood_le_one line 114