OAI/Analysis/CircleDomains/Selection/PrincipalQuadrantMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The analytic inverse mean equals one, so the principal outer flux is exactly the area factor.

  1. theorem OAI.CircleDomainRigidity.principal_quadrantFlux_of_inverse_mean line 12