OAI/Analysis/CircleDomains/Selection/LogarithmicRectangleCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Construct the nested rectangular lift charts and subordinate smooth partition used to smooth the mean index. The logarithmic lifts come from the actual covering map, not additional hypotheses.

  1. theorem OAI.CircleDomainRigidity.exists_logarithmic_rectangle_data line 19
  2. theorem OAI.CircleDomainRigidity.exists_logarithmic_rectangle_partition line 57