OAI/Analysis/CircleDomains/Rigidity/QuarterFluxIntegrability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The four quarter-arc coordinate functions of a measurable bounded field have the integrability needed for the projection identity.

  1. theorem OAI.CircleDomainRigidity.quadrant_components_integrable line 12