OAI/Probability/SLE/Geometry/RemainderKernelCancellation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A conditional sum identity identifies the positive remaining measure. Cancellation uses sigma finiteness, not finite total trace mass.

  1. lemma OAI.SLEExactGauge.bind_add_of_ae line 15
  2. lemma OAI.SLEExactGauge.bind_remainder_eq_of_sum line 29
  3. lemma OAI.SLEExactGauge.restricted_bind_le_of_ae_le line 42