OAI/Probability/SLE/Angle/TargetAngleLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The angle law in the prescribed coefficient formula is a probability measure supported on the nondegenerate disk charts.

  1. lemma OAI.SLEExactGauge.Target.angleLaw_ae_mem line 14
  2. lemma OAI.SLEExactGauge.Target.angle_normalizer_pos line 21
  3. lemma OAI.SLEExactGauge.Target.angle_normalizer_lt_top line 37
  4. theorem OAI.SLEExactGauge.Target.angleLaw_isProbability line 53