OAI/Probability/SLE/Mass/PhysicalDiskMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The disk scalar controls the actual centered and rescaled inverse Loewner pushforward. The marked angle is retained exactly.

  1. lemma OAI.SLEExactGauge.diskChartMass_eq_of_coordinates line 16
  2. lemma OAI.SLEExactGauge.diskToHalfPlane_real_affine line 34
  3. lemma OAI.SLEExactGauge.physicalDiskChart_normalized line 42
  4. lemma OAI.SLEExactGauge.physicalDiskChart_mass_eq line 51
  5. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.physical_quarter_mass_bounds line 66