### Abstract

The median method is an amplification result for randomized approximation algorithms described in [1]. Given an algorithm whose result is in a desired interval with a probability larger than 1/2, it is possible to improve the success probability, by running the algorithm multiple times independently and using the median. In contrast to using the mean, the amplification of the success probability grows exponentially with the number of independent runs.

This entry contains a formalization of the underlying theorem: Given a sequence of n independent random variables, which are in a desired interval with a probability 1/2 + a. Then their median will be in the desired interval with a probability of 1 − exp(−2a2 n). In particular, the success probability approaches 1 exponentially with the number of variables.

In addition to that, this entry also contains a proof that order-statistics of Borel-measurable random variables are themselves measurable and that generalized intervals in linearly ordered Borel-spaces are measurable.

### License

BSD License

### Topics

- Computer science/Algorithms/Randomized

### Session Median_Method

- Median

### Depends on

- Universal Hash Families

### Used by

- Formalization of Randomized Approximation Algorithms for Frequency Moments

### Auto-related entries

- Formalization of Randomized Approximation Algorithms for Frequency Moments

## Cite

×

Median_Method-AFP

    @article{Median_Method-AFP,
      author  = {Emin Karayel},
      title   = {Median Method},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Median_Method.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jan 25, 2022 : Isabelle2021-1