OAI/Analysis/CircleDomains/Sobolev/PhysicalRoundIntegrals.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of round-disk integrals and smooth partial derivatives between the physical Euclidean plane and the complex plane.

  1. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_norm line 13
  2. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_preimage_ball line 20
  3. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_integral_ball line 25
  4. theorem OAI.CircleDomainRigidity.physical_real_volume_ball line 32
  5. theorem OAI.CircleDomainRigidity.physical_complex_partial line 39
  6. theorem OAI.CircleDomainRigidity.smooth_physical_disk_vertical_flux line 50
  7. theorem OAI.CircleDomainRigidity.smooth_physical_disk_jacobian line 69