Research proof index

Marginalized Jensen / Cauchy-Schwarz step for the forking lemma. If a per-element bound acc x · (acc x / q − hinv) ≤ B x holds for every x (with acc x ≤ 1), and we marginalize over the output distribution of any mx : m X with [MonadLiftT m SPMF], then the marginalized expectation μ := ∑' x, Pr[= x | mx] · acc x satisfies the same forking-b...