OAI/Analysis/CircleDomains/Selection/PrincipalQuadrantGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Inversion sends each quarter circle to the opposite vertical quarter. The principal flux density is the mean of its analytic inverse germ.

  1. theorem OAI.CircleDomainRigidity.star_quadrantNormal line 12
  2. theorem OAI.CircleDomainRigidity.inverse_quadrantPoint line 16
  3. theorem OAI.CircleDomainRigidity.principal_quadrant_density line 23