OAI/Analysis/CircleDomains/Topology/RealCircleRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurable real-plane representatives of smooth circle coordinates, with the exact original L2 partial norms. No global real lift is used.

  1. theorem OAI.CircleDomainRigidity.exists_real_circle_representative line 17