OAI/Analysis/CircleDomains/Probability/MeasurableArcIndex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A Borel version of the explicit index, including a value on the coincidence set. Its deck identity holds everywhere, before averaging.

  1. instance OAI.CircleDomainRigidity.FiniteTransfer.(instance at line 17) line 17
  2. instance OAI.CircleDomainRigidity.FiniteTransfer.(instance at line 20) line 20
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_normalizedArgument line 23
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_circleRepresentative line 32

    Distinct definitions of this name: OAI/Analysis/CircleDomains/Modulus/CircleWedgeCost.lean:21 (same statement text; different proof or body). Qualify references as OAI.CircleDomainRigidity.FiniteTransfer.measurable_circleRepresentative@path.

  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_diskInitialArgument line 35
  6. def OAI.CircleDomainRigidity.FiniteTransfer.totalPathArgumentIncrement line 43
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_totalPathArgumentIncrement line 46
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.totalPathArgumentIncrement_of_avoids line 55
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_totalPathArgumentIncrement line 60
  10. def OAI.CircleDomainRigidity.FiniteTransfer.totalDiskArcIndex line 66
  11. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_totalDiskArcIndex line 70
  12. theorem OAI.CircleDomainRigidity.FiniteTransfer.totalDiskArcIndex_of_avoids line 81
  13. theorem OAI.CircleDomainRigidity.FiniteTransfer.totalDiskArcIndex_translate line 87
  14. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousAt_totalDiskArcIndex line 93