OAI/Probability/SLE/Mass/DilationMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact area and measure transport for positive real dilations of the half-plane. These are the spatial factors in capacity scaling.

  1. lemma OAI.SLEExactGauge.source_scale_area_lintegral line 15
  2. def OAI.SLEExactGauge.halfPlaneDilation line 39
  3. lemma OAI.SLEExactGauge.halfPlaneDilation_apply line 60
  4. def OAI.SLEExactGauge.Multipoint.dilationMass line 65
  5. lemma OAI.SLEExactGauge.Multipoint.dilationMass_apply line 69
  6. lemma OAI.SLEExactGauge.Multipoint.dilationMass_realDensity line 79
  7. lemma OAI.SLEExactGauge.Multipoint.dilationMass_initialGreen line 124
  8. lemma OAI.SLEExactGauge.Multipoint.dilationMass_bind line 129
  9. lemma OAI.SLEExactGauge.Multipoint.dilationMass_mono line 143
  10. lemma OAI.SLEExactGauge.Multipoint.dilationMass_ne_zero_iff line 147