OAI/Probability/SLE/Geometry/NormalizedCoefficientLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The inner mesh limit in the prescribed coefficient is the clipped moment of the actual canonical disk mass at the prescribed level.

  1. lemma OAI.SLEExactGauge.Target.measurable_potentialDifference line 15
  2. lemma OAI.SLEExactGauge.Target.discreteMass_comp_measurable line 28
  3. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.normalized_clipped_coefficient_limit line 49