OAI/Probability/SLE/Loewner/TargetJointMeasurability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Joint measurability in the initial disk angle. The potential is needed only on the open angle interval, where the exact initial disk radius is 1 - ‖x‖²; this avoids imposing any regularity at degenerate disk charts.

  1. lemma OAI.SLEExactGauge.Target.measurable_diskMapInv_joint line 16
  2. lemma OAI.SLEExactGauge.Target.measurable_joint_clockIntegrand line 21
  3. lemma OAI.SLEExactGauge.Target.measurable_clock_joint line 49
  4. lemma OAI.SLEExactGauge.Target.measurable_angle_joint line 75
  5. lemma OAI.SLEExactGauge.Target.measurableSet_disk_surviving_joint line 99
  6. def OAI.SLEExactGauge.Target.diskGreenFormula line 113
  7. lemma OAI.SLEExactGauge.Target.measurable_diskGreenFormula line 119
  8. lemma OAI.SLEExactGauge.Target.diskGreenFormula_eq line 130
  9. lemma OAI.SLEExactGauge.Target.measurable_diskPotentialFormula line 137
  10. lemma OAI.SLEExactGauge.Target.measurable_potential_angle line 149
  11. lemma OAI.SLEExactGauge.Target.measurable_potential_restricted_angle line 162