OAI/Analysis/CircleDomains/Probability/SlotPairNull.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independent active tag tuples avoid every product-null tuple event. Inactive slots carry no tuple mass.

  1. def OAI.CircleDomainRigidity.activeSlotPairs line 14
  2. theorem OAI.CircleDomainRigidity.measurableSet_activeSlotPairs line 17
  3. theorem OAI.CircleDomainRigidity.ae_active_slots_avoid line 39
  4. theorem OAI.CircleDomainRigidity.ae_slot_pair_avoids_product_null line 52