OAI/Analysis/CircleDomains/Probability/TagTupleMeasure.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Weighted tag-tuple measures. Tuple components retain the label list; slot weights depend only on the slot number and have finite total mass.

  1. def OAI.CircleDomainRigidity.LevelTuple line 16
  2. instance OAI.CircleDomainRigidity.(instance at line 18) line 18
  3. instance OAI.CircleDomainRigidity.(instance at line 20) line 20
  4. instance OAI.CircleDomainRigidity.(instance at line 21) line 21
  5. instance OAI.CircleDomainRigidity.(instance at line 22) line 22
  6. instance OAI.CircleDomainRigidity.(instance at line 25) line 25
  7. instance OAI.CircleDomainRigidity.(instance at line 29) line 29
  8. def OAI.CircleDomainRigidity.tagDataTuple line 31
  9. theorem OAI.CircleDomainRigidity.continuous_tagDataTuple line 33
  10. def OAI.CircleDomainRigidity.slotTupleMeasure line 38
  11. def OAI.CircleDomainRigidity.activeTagSlot line 41
  12. theorem OAI.CircleDomainRigidity.measurable_slotTupleMeasure line 43
  13. theorem OAI.CircleDomainRigidity.slotTupleMeasure_univ_le line 79
  14. def OAI.CircleDomainRigidity.slotWeight line 84
  15. theorem OAI.CircleDomainRigidity.slotWeight_pos line 86
  16. theorem OAI.CircleDomainRigidity.tsum_slotWeight line 90
  17. def OAI.CircleDomainRigidity.weightedTupleMeasure line 92
  18. theorem OAI.CircleDomainRigidity.weightedTupleMeasure_apply line 95
  19. theorem OAI.CircleDomainRigidity.weightedTupleMeasure_mass_le line 100
  20. instance OAI.CircleDomainRigidity.(instance at line 105) line 105
  21. theorem OAI.CircleDomainRigidity.measurable_weightedTupleMeasure line 108
  22. theorem OAI.CircleDomainRigidity.weightedTupleMeasure_slot_le line 117