OAI/Analysis/CircleDomains/Modulus/BarrierModulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform modulus bound, derived from the constructed compatible barrier and valid for the actual finite constrained coding-measure family.

  1. theorem OAI.CircleDomainRigidity.barrier_modulus_lower_bound line 19