OAI/Analysis/CircleDomains/Probability/BarrierCodeLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Failure of a small compatible barrier yields a probability law, using ADMS duality, Bogachev lifting, and the resulting modulus bound.

  1. theorem OAI.CircleDomainRigidity.exists_positive_barrier_duality_parameter line 17
  2. theorem OAI.CircleDomainRigidity.code_law_of_no_small_compatible_barrier line 28
  3. theorem OAI.CircleDomainRigidity.prescribed_countable_law_of_no_small_barrier line 97