OAI/Probability/SLE/Gauge/ConformalDenseExperiment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual dense experiment transported through an arbitrary inverse chart. Its lower bound is uniform over normalized marked states and its cutoff is proportional to the physical conformal radius.

  1. lemma OAI.SLEExactGauge.segmentSausageCharge_le_stoppedWhole line 17
  2. lemma OAI.SLEExactGauge.Serpentine.dense_conformal_mass_threshold line 35
  3. theorem OAI.SLEExactGauge.Serpentine.uniform_conformal_dense_stopped_mass line 56