OAI/Probability/InvariantIsing/Gaussian/MPTrigonometricCritical.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The zero-edge endpoint of the MP angular integral.

  1. lemma OAI.InvariantIsing.mp_critical_sine_fraction line 10
  2. theorem OAI.InvariantIsing.mp_integral_sine_fraction_critical line 19