OAI/Analysis/CircleDomains/Probability/PathCostMeasure.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The actual three-part coding measure: physical occupation, countable preterminal visits, and weighted tuples. Finiteness is a Borel code condition.

  1. def OAI.CircleDomainRigidity.PathCostSpace line 17
  2. instance OAI.CircleDomainRigidity.(instance at line 19) line 19
  3. instance OAI.CircleDomainRigidity.(instance at line 21) line 21
  4. instance OAI.CircleDomainRigidity.(instance at line 23) line 23
  5. instance OAI.CircleDomainRigidity.(instance at line 25) line 25
  6. def OAI.CircleDomainRigidity.costPhysical line 29
  7. def OAI.CircleDomainRigidity.costAtomic line 31
  8. def OAI.CircleDomainRigidity.costTuple line 33
  9. theorem OAI.CircleDomainRigidity.measurable_costPhysical line 43
  10. theorem OAI.CircleDomainRigidity.measurable_costAtomic line 49
  11. theorem OAI.CircleDomainRigidity.measurable_costTuple line 55
  12. def OAI.CircleDomainRigidity.baseCodeOccupation line 59
  13. def OAI.CircleDomainRigidity.pathCostMeasure line 62
  14. instance OAI.CircleDomainRigidity.(instance at line 68) line 68
  15. theorem OAI.CircleDomainRigidity.baseCodeOccupation_univ line 74
  16. theorem OAI.CircleDomainRigidity.pathCostMeasure_univ line 80
  17. theorem OAI.CircleDomainRigidity.pathCostMeasure_finite_iff line 93
  18. theorem OAI.CircleDomainRigidity.measurable_baseCodeOccupation line 105
  19. theorem OAI.CircleDomainRigidity.measurable_pathCostMeasure line 110
  20. abbrev OAI.CircleDomainRigidity.FiniteCostCode line 119
  21. theorem OAI.CircleDomainRigidity.measurableSet_finiteCostCode line 122
  22. theorem OAI.CircleDomainRigidity.standardBorel_finiteCostCode line 128
  23. instance OAI.CircleDomainRigidity.(instance at line 133) line 133
  24. theorem OAI.CircleDomainRigidity.lintegral_pathCostMeasure line 139