OAI/Analysis/CircleDomains/Modulus/PriorityWeights.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Countable priority weights form a subprobability distribution. The remaining mass belongs to the original horizontal coordinate.

  1. def OAI.CircleDomainRigidity.priorityRemainder line 14
  2. def OAI.CircleDomainRigidity.priorityWeight line 17
  3. theorem OAI.CircleDomainRigidity.priorityRemainder_succ line 19
  4. theorem OAI.CircleDomainRigidity.priorityRemainder_mem_unit line 23
  5. theorem OAI.CircleDomainRigidity.priorityWeight_nonneg line 33
  6. theorem OAI.CircleDomainRigidity.priorityWeight_sum line 36
  7. theorem OAI.CircleDomainRigidity.priorityWeight_summable line 45
  8. theorem OAI.CircleDomainRigidity.priorityWeight_tsum_mem_unit line 52
  9. theorem OAI.CircleDomainRigidity.priorityWeighted_summable line 60
  10. def OAI.CircleDomainRigidity.priorityInfiniteValue line 67
  11. theorem OAI.CircleDomainRigidity.priorityInfiniteValue_norm_le line 70