OAI/Probability/SLE/Angle/CanonicalAngleMixing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-centered mixing for the actual canonical angle kernel. The constants are derived from the positive spectral law, not assumed.

  1. lemma OAI.SLEExactGauge.angleSpectralLaw_lintegral_bounds line 15
  2. lemma OAI.SLEExactGauge.Target.diskMapInv_zero_arg line 38
  3. lemma OAI.SLEExactGauge.canonicalAngleAverage_uniform_bounds line 45