OAI/Probability/InvariantIsing/Gaussian/MPDensitySubstitution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact real change of variables for the literal MP density on its support interval.

  1. lemma OAI.InvariantIsing.continuous_mpAngle line 10
  2. lemma OAI.InvariantIsing.measurable_mpDensity line 13
  3. lemma OAI.InvariantIsing.mpAngle_deriv_nonpos line 17
  4. theorem OAI.InvariantIsing.mpDensity_substitution line 22