OAI/Analysis/CircleDomains/Sobolev/SmoothPathIntersections.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The smooth scalar differential bounds distinct curve intersections, including levels modulo one. The bound uses the actual curve image and is obtained from Lipschitz coarea.

  1. theorem OAI.CircleDomainRigidity.smooth_curve_mod_one_coarea_bound line 16
  2. theorem OAI.CircleDomainRigidity.integrated_smooth_pathImageCount_le_differential line 35
  3. theorem OAI.CircleDomainRigidity.integrated_smooth_circle_pathImageCount_le_differential line 48