OAI/Analysis/CircleDomains/Sobolev/AxisSwapEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Swapping the two Cartesian axes preserves Dirichlet energy and round disks.

  1. def OAI.CircleDomainRigidity.axisSwap line 14
  2. theorem OAI.CircleDomainRigidity.axisSwap_apply line 16
  3. theorem OAI.CircleDomainRigidity.axisSwap_one line 18
  4. theorem OAI.CircleDomainRigidity.axisSwap_I line 20
  5. theorem OAI.CircleDomainRigidity.axisSwap_re line 22
  6. theorem OAI.CircleDomainRigidity.axisSwap_im line 24
  7. theorem OAI.CircleDomainRigidity.axisSwap_axisSwap line 26
  8. theorem OAI.CircleDomainRigidity.axisSwap_symm_apply line 29
  9. theorem OAI.CircleDomainRigidity.axisSwap_preimage_closedBall line 33
  10. theorem OAI.CircleDomainRigidity.euclideanGradientEnergy_axisSwap line 39
  11. theorem OAI.CircleDomainRigidity.integral_energy_axisSwap line 50