OAI/Analysis/CircleDomains/Selection/RegularLevelFlowOrbit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Time translation and exact orbit identities for the constructed regular-level flow.

  1. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.trajectory_shift line 13
  2. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.trajectory_shift_of_eq line 24
  3. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.range_eq_of_mem line 31
  4. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.periodic_of_return line 44
  5. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.orbits_eq_or_disjoint line 50