OAI/Analysis/CircleDomains/Probability/PathPortionMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The arclength measure of a constant-extended path portion is exactly the restriction of the original time measure. Thus adjacent portions add without charging their shared endpoint.

  1. theorem OAI.CircleDomainRigidity.Ioc_timeClip line 16
  2. theorem OAI.CircleDomainRigidity.pathLengthMeasure_clipped line 31
  3. def OAI.CircleDomainRigidity.pathPortionOccupation line 46
  4. theorem OAI.CircleDomainRigidity.pathOccupation_clipped line 50
  5. theorem OAI.CircleDomainRigidity.pathPortionOccupation_congr line 59
  6. theorem OAI.CircleDomainRigidity.pathPortionOccupation_add line 71
  7. theorem OAI.CircleDomainRigidity.measurable_pathPortionOccupation line 97