OAI/Analysis/CircleDomains/Topology/MeanArcIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Borel arc index is averaged against the actual arc law. On the boundary its average is the positive Stieltjes coordinate already proved.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.meanDiskArcIndex line 15
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.meanDiskArcIndex_translate line 19
  3. def OAI.CircleDomainRigidity.FiniteTransfer.arcStartingAngleLaw line 27
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_arcStartingAngle line 30
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.totalDiskArcIndex_boundary_ae line 34
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_totalDiskArcIndex_boundary line 48
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.meanDiskArcIndex_boundary line 61