OAI/Combinatorics/EditApproximation/Probability/Median.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The executable upper middle order statistic

The seed pass sorts its integer copy outputs and takes index length/2. Strictly more than half the outputs below an upper bound suffice; ties and repeated values are retained by the list representation.

  1. theorem OAI.EditApproximation.upperMedian_lower line 19
  2. theorem OAI.EditApproximation.upperMedian_upper line 32
  3. theorem OAI.EditApproximation.clamped_upperMedian_spec line 70