OAI/Analysis/CircleDomains/Modulus/MeanIndexArcPayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual local branch of the averaged ray index is paid for by the finite expected intersection measure of a prior level union.

  1. theorem OAI.CircleDomainRigidity.lifted_mean_index_arc_payment line 19