proofs
Provedattentionimportance-samplingrejection-samplingseparation

A family with bounded importance factor and unbounded rejection envelope

For all M∈R\htmlData{mx=1}{M \in \htmlData{mx=0}{\mathbb{R}}}, if 1<M1 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{M}, then

1≤2MM+1∧2MM+1<2∧1<M1 \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\frac{\htmlData{mx=1}{2\htmlData{mx=0}{M}}}{\htmlData{mx=3}{\htmlData{mx=2}{M} + 1}}} \mathbin{\htmlData{mx=15}{\land}} \htmlData{mx=10}{\frac{\htmlData{mx=7}{2\htmlData{mx=6}{M}}}{\htmlData{mx=9}{\htmlData{mx=8}{M} + 1}}} \mathrel{\htmlData{mx=11}{<}} 2 \mathbin{\htmlData{mx=14}{\land}} 1 \mathrel{\htmlData{mx=13}{<}} \htmlData{mx=12}{M}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
<Less than
1 is strictly smaller than M. (1 < M)
≤At most
1 is less than or equal to 2 · M/(M + 1). (1 ≤ 2 * M / (M + 1))
·Multiplication
2 times M. (2 * M)
a/bDivision
2 · M divided by M + 1. In Lean, dividing by 0 gives 0. (2 * M / (M + 1))
+Addition
M plus 1. (M + 1)
∧And
Both hold: 2 · M/(M + 1) < 2, and 1 < M. (2 * M / (M + 1) < 2 ∧ 1 < M)

For M>1, the example family has importance second-moment factor C=2M/(M+1), which stays in [1,2), while the rejection envelope K=M grows without bound.

How it was proved

Proved
5 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
14 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements