OAI/Geometry/RCD/Sobolev/ConditionalSelfPair.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The independent conditional self-coupling over a measurable observable

  1. def OAI.RegularPointCoordinates.conditionalSelfPair line 15
  2. theorem OAI.RegularPointCoordinates.conditionalSelfPair_marginals line 21
  3. instance OAI.RegularPointCoordinates.conditionalSelfPair_finite line 37
  4. theorem OAI.RegularPointCoordinates.conditionalSelfPair_common line 42