OAI/Analysis/CircleDomains/Sobolev/ComplexRealEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identifying the line-payment energy with the transferred real energy

The finite transfer uses real coordinate pairs, while round disks and line payment use complex coordinates. The canonical linear equivalence preserves volume and identifies the two ordinary gradient integrands.

  1. theorem OAI.CircleDomainRigidity.euclideanGradientEnergy_eq_real_gradientEnergy line 23
  2. theorem OAI.CircleDomainRigidity.real_gradient_energy_in_complex_coordinates line 33