OAI/Analysis/CircleDomains/Selection/PhysicalMeanIndexVertical.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vertical absolute continuity and derivative bounds for the local mean index. Coordinate interchange preserves physical area, and coarea bounds the slices by the occupation density.

  1. theorem OAI.CircleDomainRigidity.physicalMeanIndex_vertical_ACL_derivative line 20