OAI/Analysis/CircleDomains/Probability/CodeLawMeasures.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual mean occupation, atomic and tuple measures of a law on base codes. Their sum is exactly the barycenter of the coding measures.

  1. theorem OAI.CircleDomainRigidity.measurable_baseCodeAtomic line 24
  2. theorem OAI.CircleDomainRigidity.measurable_baseCodeTuple line 31
  3. def OAI.CircleDomainRigidity.meanCodeOccupation line 35
  4. def OAI.CircleDomainRigidity.meanCodeAtomic line 38
  5. def OAI.CircleDomainRigidity.meanCodeTuple line 42
  6. def OAI.CircleDomainRigidity.meanCodeCost line 46
  7. theorem OAI.CircleDomainRigidity.meanCodeOccupation_apply line 51
  8. theorem OAI.CircleDomainRigidity.meanCodeAtomic_apply line 58
  9. theorem OAI.CircleDomainRigidity.meanCodeTuple_apply line 66
  10. theorem OAI.CircleDomainRigidity.meanCodeCost_apply line 71
  11. theorem OAI.CircleDomainRigidity.meanCodeCost_eq line 77