OAI/Probability/InvariantIsing/Gaussian/MPTrigonometricIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The elementary semicircle-over-resolvent integral needed by the MP density.

  1. lemma OAI.InvariantIsing.mp_sine_fraction_identity line 11
  2. theorem OAI.InvariantIsing.mp_integral_sine_fraction line 18