OAI/Probability/SLE/Angle/TargetDiskMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact compact and continuous conformal weight whose canonical mass has the source-prescribed disk Green potential.

  1. def OAI.SLEExactGauge.Target.diskSourceHalfPlane line 16
  2. lemma OAI.SLEExactGauge.Target.diskSourceHalfPlane_compact line 19
  3. lemma OAI.SLEExactGauge.Target.diskMap_deriv_continuous line 32
  4. def OAI.SLEExactGauge.Target.diskMassWeight line 42
  5. lemma OAI.SLEExactGauge.Target.diskMassWeight_coe line 48
  6. lemma OAI.SLEExactGauge.Target.diskMassWeight_ennreal line 53
  7. theorem OAI.SLEExactGauge.Target.potential_eq_weighted_green line 58
  8. theorem OAI.SLEExactGauge.Target.potential_toReal_eq_compactWeightedMass line 89