OAI/Analysis/CircleDomains/Sobolev/PlanarDifferentialEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-transfer gradient energy controls the norm of the scalar real differential in the complex coarea chart.

  1. theorem OAI.CircleDomainRigidity.norm_complex_real_linear_le line 16
  2. theorem OAI.CircleDomainRigidity.complex_chart_differential_energy_finite line 32