OAI/Analysis/CircleDomains/Sobolev/SmoothMeanPeriodData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single constructed mean-period coordinate retains its real atlas, closed masked levels, vanishing correction, and actual smooth physical representative. The analytic and topological data come from one law.

  1. structure OAI.CircleDomainRigidity.SmoothMeanPeriodData line 22
  2. theorem OAI.CircleDomainRigidity.exists_smooth_mean_period_data line 71