OAI/Probability/SLE/Multipoint/MultipointTupleNull.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Distinctness of planar integration tuples. The values assigned to the distance kernel on collision diagonals do not affect its integral.

  1. lemma OAI.SLEExactGauge.Multipoint.ae_tuple_pair_ne line 14
  2. theorem OAI.SLEExactGauge.Multipoint.ae_tuple_injective line 41
  3. theorem OAI.SLEExactGauge.Multipoint.ae_tuple_avoids line 56