OAI/Analysis/CircleDomains/Sobolev/OpenMeanCircleSmoothing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smoothing the actual physical mean on an open disk chart, with all local logarithmic charts and the partition constructed internally.

  1. theorem OAI.CircleDomainRigidity.open_physical_mean_circle_smoothing line 19