OAI/Analysis/CircleDomains/Probability/SlotLawMeasures.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Each fixed slot distribution is dominated by the mean weighted tuple measure, and hence inherits its absolute continuity. Inactive slots have zero mass, so these are subprobability measures.

  1. def OAI.CircleDomainRigidity.baseCodeSlot line 19
  2. theorem OAI.CircleDomainRigidity.measurable_baseCodeSlot line 22
  3. def OAI.CircleDomainRigidity.slotLaw line 27
  4. theorem OAI.CircleDomainRigidity.slotLaw_apply line 30
  5. theorem OAI.CircleDomainRigidity.slotLaw_univ_le line 35
  6. theorem OAI.CircleDomainRigidity.weighted_slotLaw_le line 43
  7. theorem OAI.CircleDomainRigidity.slotLaw_absolutelyContinuous line 56