OAI/Analysis/CircleDomains/Sobolev/ComplexWedgeIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The area contribution to the Stokes estimate has the sharp factor sqrt(pi) times the containing radius.

  1. theorem OAI.CircleDomainRigidity.integral_complexCovector_wedge_le line 15