OAI/Analysis/CircleDomains/Probability/PathOccupation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Physical occupation of a rectifiable metric path, and its mean under a law. The measure records arclength with multiplicity, including repeated traversals.

  1. def OAI.CircleDomainRigidity.pathOccupation line 19
  2. instance OAI.CircleDomainRigidity.(instance at line 22) line 22
  3. theorem OAI.CircleDomainRigidity.pathOccupation_apply line 26
  4. theorem OAI.CircleDomainRigidity.pathOccupation_univ line 30
  5. theorem OAI.CircleDomainRigidity.lintegral_pathOccupation line 34
  6. theorem OAI.CircleDomainRigidity.measurable_pathOccupation line 41
  7. def OAI.CircleDomainRigidity.meanPathOccupation line 53
  8. theorem OAI.CircleDomainRigidity.meanPathOccupation_apply line 56
  9. theorem OAI.CircleDomainRigidity.lintegral_meanPathOccupation line 61
  10. theorem OAI.CircleDomainRigidity.measurable_meanPathOccupation line 71
  11. theorem OAI.CircleDomainRigidity.meanPathOccupation_mixture line 74