OAI/Probability/SLE/Angle/TargetDiskPotential.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The prescribed disk potential is exactly the conformally weighted current Green mass of the compact disk preimage.

  1. def OAI.SLEExactGauge.Target.diskSourceCompact line 16
  2. lemma OAI.SLEExactGauge.Target.diskK_subset_unit line 18
  3. lemma OAI.SLEExactGauge.Target.diskSourceCompact_subset line 22
  4. lemma OAI.SLEExactGauge.Target.diskSourceCompact_compact line 27
  5. lemma OAI.SLEExactGauge.Target.diskSourceCompact_image line 38
  6. lemma OAI.SLEExactGauge.Target.diskMap_deriv_pos line 47
  7. theorem OAI.SLEExactGauge.Target.potential_eq_source_green_integral line 53