OAI/Analysis/CircleDomains/Sobolev/SmoothMeanPhysicalBranches.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The retained mean branches project to the actual physical circle coordinate. Its smoothness upgrades those continuous branches to smooth real functions on the physical patch, as required by terminal filling.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.branch_physical_projection line 20
  2. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.branch_physical_smooth line 36