OAI/Analysis/CircleDomains/Selection/MeanIndexHorizontalACL.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual locally lifted mean index is absolutely continuous on almost every physical horizontal line. Rational slice estimates are simultaneous, and continuity from above supplies arbitrary endpoints.

  1. theorem OAI.CircleDomainRigidity.meanIndex_horizontal_ACL_derivative line 20