OAI/Analysis/CircleDomains/Modulus/ModulusNormBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing a pointwise lower bound for every admissible metric to the measure-family modulus. The metrics retain extended values.

  1. theorem OAI.CircleDomainRigidity.le_modulus_of_admissible_norm_bound line 17