OAI/Analysis/CircleDomains/Topology/DiskArcBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The explicit index on the boundary of the disk is the floor of the lifted angle minus the starting angle. This supplies its orientation and the positive unit boundary period.

  1. lemma OAI.CircleDomainRigidity.FiniteTransfer.re_one_sub_pos_of_norm_le line 15
  2. lemma OAI.CircleDomainRigidity.FiniteTransfer.re_one_sub_div_pos line 26
  3. lemma OAI.CircleDomainRigidity.FiniteTransfer.abs_argument_turns_lt_quarter line 37
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.boundary_pathArgumentIncrement line 44
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.diskArcIndex_boundary_floor line 78