OAI/Analysis/CircleDomains/Sobolev/ComplexScalarEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact complex-chart energy of a smooth physical scalar, and its convergence under positive mollification.

  1. theorem OAI.CircleDomainRigidity.complex_scalar_energy_pointwise line 14
  2. theorem OAI.CircleDomainRigidity.complex_scalar_energy_integral line 27
  3. theorem OAI.CircleDomainRigidity.complex_mollification_energy_tendsto line 39