OAI/Probability/SLE/Geometry/CanonicalCoefficientIntegrability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability and removal of the exact coefficient's clipping, using the canonical terminal disk moment as a dominator.

  1. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.density_disk_terminal_integrable line 22
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.clippedCoefficient_unclip_limit line 46