OAI/Analysis/CircleDomains/Selection/MeanBranchBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compact arc family's geometric index bound also bounds every mean branch on a bounded logarithmic chart.

  1. theorem OAI.CircleDomainRigidity.bounded_meanGeometricIndex_on_chart line 13