OAI/Analysis/CircleDomains/Sobolev/ModelLocalEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Properness of the actual inverse projection bounds images of bounded source sets. Complex change of variables then gives their finite energy.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.projection_bounded_lifts line 18
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.function_bounded_on_source_ball line 34
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.derivative_energy_on_source_ball line 47