OAI/Analysis/CircleDomains/Sobolev/SmoothMeanCircuit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A physical smooth circle coordinate has an actual smooth, period-one real lift on a circuit whenever it is the perturbed mean on a lifted punctured-disk circuit. No smoothness of the boundary angle is required.

  1. theorem OAI.CircleDomainRigidity.exists_smooth_mean_circuit_lift line 19
  2. theorem OAI.CircleDomainRigidity.mean_circuit_integral_lower_bound line 50