OAI/Probability/SLE/Multipoint/MultipointPhysicalProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Physical-domain multipoint approach bounds, including arbitrary positive targets through the paper's capped product.

  1. theorem OAI.SLEExactGauge.Multipoint.physical_radius_multipoint_bound line 16
  2. theorem OAI.SLEExactGauge.Multipoint.capped_physical_radius_multipoint_bound line 48