OAI/Probability/InvariantIsing/Haar/ProbabilityMedian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Existence of a median for every real probability law, including laws with atoms.

  1. theorem OAI.InvariantIsing.probability_real_median line 11
  2. theorem OAI.InvariantIsing.measurable_median line 54