OAI/Probability/SLE/Multipoint/MultipointPhysicalGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Disk uniformizations of the actual surviving physical domains. The radius includes the derivative of the original conformal map, with no uniform bound on that derivative.

  1. def OAI.SLEExactGauge.physicalConformalRadius line 15
  2. def OAI.SLEExactGauge.physicalDiskChart line 18
  3. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.physical_disk_chart line 21
  4. theorem OAI.SLEExactGauge.IsCapacityTwoWitness.physical_interaction_decay line 86