OAI/Analysis/CircleDomains/Sobolev/HeightSmoothApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the smooth annular estimate through uniform approximation and convergence of the actual Dirichlet energies.

  1. theorem OAI.CircleDomainRigidity.homeomorphic_height_log_bound_of_smooth_approximation line 12