OAI/Probability/InvariantIsing/Gaussian/MPAngularShift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The elementary shifted angular integral for the MP Stieltjes transform.

  1. lemma OAI.InvariantIsing.mp_shifted_centre_exceeds_radius line 10
  2. lemma OAI.InvariantIsing.mp_shifted_sine_integrable line 16
  3. lemma OAI.InvariantIsing.mp_shifted_angular_integral line 21