bernoulli_powerset_event_prob_eq_product_measure

Companion of the keystone bridge for EVENT PROBABILITIES. The powerset event probability $\Pr_p[\mathrm{Event}] = \sum_{\Omega : \mathrm{Event}(\Omega)} p^{|\Omega|}(1-p)^{N-|\Omega|}$ (bernoulliEventProb) equals the real-valued measure under the stock Mathlib product-Bernoulli measure bernMeasure of the pulled-back event $\{\omega : \mathrm{Event}(\mathrm{indicatorToFinset}\,\omega)\}$. This lets every tail / concentration statement phrased on the bespoke bernoulliEventProb be transported to a genuine Mathlib measure-probability $\mu.\mathrm{real}\,S$, unlocking measure-theoretic tail tools (Markov, condExp, decoupling) on the powerset model. Proof: rewrite bernoulliEventProb as the bernoulliExpectation of the {0,1}-indicator, apply the keystone bridge, then identify the integral of the pulled-back indicator with the measure of the pulled-back set (integral_indicator_one; all sets measurable on the discrete indicator space).