OAI/Probability/SLE/Mass/DiskLevelTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Area transport for the disk Green weights at individual radius levels. The derivative squared from area cancels the Green codimension factor, leaving precisely the canonical mass weight.

  1. lemma OAI.SLEExactGauge.Target.diskCompactPreimage_subset line 15
  2. lemma OAI.SLEExactGauge.Target.diskCompactPreimage_compact line 22
  3. theorem OAI.SLEExactGauge.Target.disk_level_integral_transport line 32