OAI/Probability/SLE/Angle/AngleMomentUniqueness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cosine eigenpolynomials determine finite angle laws on [0, pi].

  1. def OAI.SLEExactGauge.angleIntegralLinear line 14
  2. lemma OAI.SLEExactGauge.angle_polynomial_moments_of_eigen_moments line 22
  3. lemma OAI.SLEExactGauge.angle_continuous_moments_of_polynomial_moments line 35
  4. lemma OAI.SLEExactGauge.angleMeasures_eq_of_eigenMoments line 70