OAI/Analysis/CircleDomains/Sobolev/SmoothMeanCollarApplication.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the physical collar estimate to the actual smoothed mean-period data. The correction's continuity and the physical value formula come from the construction; no separate smooth circuit is assumed.

  1. theorem OAI.CircleDomainRigidity.exists_smooth_mean_collar_lower_bound line 17