Probability-weighted Cauchy-Schwarz / Jensen inequalities

Inequalities relating per-element bounds and their probabilistic averages, for use in forking-lemma-style game-hopping arguments where the outermost step marginalizes over a random key (or, more generally, an arbitrary HasEvalSPMF monad output).

The headline lemma is marginalized_jensen_forking_bound: given a per-element bound acc x · (acc x / q − hinv) ≤ B x and weights Pr[= x | mx] for some monadic computation mx, the marginalized expectation μ := 𝔼[acc] satisfies the same shape:

μ · (μ / q − hinv) ≤ 𝔼[B].

The forking-lemma instantiation is q := qH + 1, hinv := 1/|Chal|, with acc x the per-pk fork-success probability, B x the per-pk extraction-success probability, and mx := keygen. The integration step is genuinely lossy (Cauchy-Schwarz on Pr[= · | mx]), so this lemma sits at the heart of any keygen-marginalized fork-based extraction bound.

theorem OracleComp.EvalDist.marginalized_jensen_forking_bound {m : Type → Type v} [Monad m] [HasEvalSPMF m] {X : Type} (mx : m X) (acc B : X → ENNReal) (q hinv : ENNReal) (hinv_ne_top : hinv ≠ ⊤) (hacc_le : ∀ (x : X), acc x ≤ 1) (hper : ∀ (x : X), acc x * (acc x / q - hinv) ≤ B x) : (∑' (x : X), Pr[= x | mx] * acc x) * ((∑' (x : X), Pr[= x | mx] * acc x) / q - hinv) ≤ ∑' (x : X), Pr[= x | mx] * B x

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 HasEvalSPMF, then the marginalized expectation μ := ∑' x, Pr[= x | mx] · acc x satisfies the same forking-bound shape:

μ · (μ / q − hinv) ≤ ∑' x, Pr[= x | mx] · B x.

The proof uses Cauchy-Schwarz μ² ≤ ∑' x, Pr[= x | mx] · acc x² (via ENNReal.sq_tsum_le_tsum_sq with weights summing to ≤ 1) and ENNReal.mul_sub to distribute the truncated subtraction across the sum.

Intended use. In Pointcheval-Stern / Bellare-Neven style EUF-CMA-to-relation reductions, instantiate as follows:

• mx := hr.gen (key generator),
• acc (pk, sk) := Pr[fork point exists | run nmaAdv on pk],
• B (pk, sk) := Pr[extraction succeeds | reduction pk],
• q := qH + 1, hinv := 1 / |Chal|.

The per-element hypothesis hper is then exactly the conclusion of replayForkingBound (or seededForkingBound) at a fixed pk, composed with the special-soundness extractor.

This generalizes the obvious [Fintype X] Cauchy-Schwarz: the tsum form handles the typical case where X = Stmt × Wit (uncountable in general, supported on whatever keygen reaches).