OAI/Probability/SLE/Geometry/CenteredCellTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual centered cell tails, and finite strict-past tests, are bounded by the prescribed limiting disk tail after angular mixing at the start.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.centered_cell_tail_of_angle_bound line 18
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.centered_strict_past_cell_tail_of_angle_bound line 67