OAI/Analysis/CircleDomains/Sobolev/SmoothMeanRealRepresentative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Apply real-plane coordinate transport to the smooth mean. The original quantitative partial norms are retained and the physical circle values are unchanged in the domain.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.euclidean_smooth line 18
  2. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.exists_real_representative line 33
  3. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.real_branch_smooth line 67