OAI/Analysis/CircleDomains/Topology/PotentialPhysicalPaths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constructed potential controls every physical domain path. In particular it controls ordinary chart segments with their line density.

  1. theorem OAI.CircleDomainRigidity.potential_physical_path_bound line 21
  2. theorem OAI.CircleDomainRigidity.potential_chart_interval_bound line 48