MeanBranchAtlas.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded real representatives for the actual mean on a punctured spherical mask. The countable logarithmic atlas and every bound are constructed from the compact arc law.

theorem OAI.CircleDomainRigidity.exists_bounded_mean_branch_atlas line 22