[RemyDegenne]

This PR adds the Bernoulli maximal inequality [DLB17, Lemma F.4], [EV26, Lemma 20]. If X i is ℱ (i + 1)-measurable with values in [0, 1] almost surely and P i is a version of E[X i | ℱ i], then for every δ > 0, ℙ(∃ n, ∑_{i < n} X i < (1/2) ∑_{i < n} P i - log (1 / δ)) ≤ δ (LMLExplore.measure_exists_sum_lt_half_mul_sum_sub_le). This is the "counts versus pseudo-counts" tool n ≥ n̄/2 - log(3SAH/δ) that ReinforcementLearning Layer 19.2 (RF-Express [MDJKLV21, Theorem 1]) lists among the tools to prove. Its instance at the visits of a step–state–action pair, at confidence δ/(3SAH), gives the counts event of that analysis. The other Layer 19.2 tools are either in flight (KL-to-Bernstein transport and variance transfers #291, the self-bounding inequality #287) or still to port (the logarithmic sum bound). After this PR, the milestone still needs the logarithmic sum bound, the threshold β from Layer 3.4, and the RF-Express algorithm with its PAC and sample-complexity theorem on statesEnv (Layer 7.7).

The new file LMLExplore/Probability/Martingale/BernoulliMaximal.lean (160 lines) adds:

• LMLExplore.condExp_exp_condExp_div_two_sub_le_one: the one-step bound E[exp (E[X | m] / 2 - X) | m] ≤ 1 for X measurable with values in [0, 1] a.s. It is proved from the chord exp (-x) ≤ 1 - (1 - e⁻¹) x on [0, 1] (Mathlib's convexOn_exp), the pull-out property, and 1 - e⁻¹ ≥ 1/2 (Mathlib's Real.exp_neg_one_lt_half).
• LMLExplore.measure_exists_sum_lt_half_mul_sum_sub_le: the time-uniform inequality. It goes through LMLExplore's LMLExplore.supermartingale_exp_sum_of_condExp_exp_le_one and Ville's inequality MeasureTheory.Supermartingale.measure_exists_le_le.

LMLExplore's fixed-η Freedman inequality LMLExplore.measure_exists_mul_sum_condExp_sq_add_log_div_le_sum_le, applied to P i - X i with η = 1/2, gives only - 2 log (1 / δ). The sharper constant needs the dedicated one-step bound above.

This PR ports Essakine2026Tight/ForLMLExplore/Probability/Martingale/Ville.lean from RemyDegenne/Essakine2026Tight at commit 9c77165d56f81c1db7a9835068356bb14886a3be (Apache 2.0, author Rémy Degenne). It generalizes and re-proves that material as follows:

• The source assumes X i ∈ {0, 1} everywhere, together with P i ∈ [0, 1] and ℱ i-strong measurability of P i. Here X i ∈ [0, 1] holds only almost surely, and P i is any version of the conditional mean. Its range and measurability are then derived rather than assumed, and the convexity chord replaces the {0, 1} identity.
• The declarations are in the LMLExplore namespace, next to Freedman's inequality, rather than in MeasureTheory.
• The one-step lemma is renamed from condExp_exp_sub_le_one to condExp_exp_condExp_div_two_sub_le_one, to name its conclusion.

No declaration is removed or renamed on main.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R12

🤖 Prepared with Claude Code