OAI/Analysis/CircleDomains/Sobolev/SobolevLevelOscillation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the smooth image estimate to a Sobolev approximation on a finite-length level. The conclusion holds on every measurable connected subset simultaneously; no exceptional set of arcs is introduced.

  1. theorem OAI.CircleDomainRigidity.connected_level_oscillation_of_approximation line 14