OAI/Analysis/CircleDomains/Selection/RegularLevelFlow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complete smooth nonstationary trajectories on compact regular levels of the actual defining planar scalar function.

  1. lemma OAI.CircleDomainRigidity.smooth_integral_curve line 12
  2. structure OAI.CircleDomainRigidity.CompactRegularLevelFlow line 26
  3. lemma OAI.CircleDomainRigidity.exists_compact_regular_level_flow line 40