Majority-vote amplification: if each run fails w.p. ≤ 1/4, P(≥ half of k i.i.d. runs fail) ≤ (7/8)^k

For all $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$, $\htmlData{mx=3}{w : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$, $\htmlData{mx=3}{\mathit{bad} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\operatorname{Prop}}}$ and $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$, if $\htmlData{mx=4}{\forall \omega,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}}$, $\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1$ and $\htmlData{mx=6}{\sum_{\omega \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{filter}}(\htmlData{mx=1}{\mathit{bad}})}} \htmlData{mx=5}{\htmlData{mx=3}{w}(\htmlData{mx=4}{\omega})}} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\frac{1}{4}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{DecidablePred}}\,\htmlData{mx=1}{\mathit{bad}}}$), then