OAI/Probability/SLE/Geometry/PhysicalCenteredWeights.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed-center product estimate in physical conformal coordinates. Derivative factors are retained so that area transport cancels them in the disk moment integral, including near the endpoint angles.

  1. lemma OAI.SLEExactGauge.Multipoint.physical_stoppedGreen_level_bound line 16
  2. lemma OAI.SLEExactGauge.Multipoint.centered_target_weights_capped line 30
  3. theorem OAI.SLEExactGauge.Multipoint.physical_stoppedGreen_centered_product_bound line 64