OAI/Analysis/CircleDomains/Modulus/ConstrainedCostCodes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual finite coding-measure family with a prescribed null residual-image constraint, as a standard Borel space of codes.

  1. abbrev OAI.CircleDomainRigidity.ConstrainedCostCode line 23
  2. theorem OAI.CircleDomainRigidity.measurableSet_constrainedCostCode line 29
  3. theorem OAI.CircleDomainRigidity.standardBorel_constrainedCostCode line 37
  4. def OAI.CircleDomainRigidity.finiteCodeMeasure line 43
  5. theorem OAI.CircleDomainRigidity.measurable_finiteCodeMeasure line 47
  6. def OAI.CircleDomainRigidity.constrainedCodeMeasure line 52
  7. theorem OAI.CircleDomainRigidity.measurable_constrainedCodeMeasure line 56
  8. def OAI.CircleDomainRigidity.sparseConstrainedCostCode line 61
  9. theorem OAI.CircleDomainRigidity.measurable_sparseConstrainedCostCode line 71