OAI/Analysis/CircleDomains/Modulus/CodeModulusExtraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measure-family duality and probability lifting produce a law on the constrained codes from a positive modulus bound.

  1. theorem OAI.CircleDomainRigidity.costAdmissible_iff_constrained line 30
  2. theorem OAI.CircleDomainRigidity.positive_modulus_code_law line 44