BanditRLProof.ConcentrationMartingaleMaximal

Conditional Jensen turns an exponentially integrable real martingale into a nonnegative exponential submartingale.

theorem submartingale_exp_of_martingale (hS : Martingale S F μ) (hint : ∀ i, Integrable (fun ω => exp (S i ω)) μ) : Submartingale (fun i ω => exp (S i ω)) F μ

Finite-time maximal Chernoff bound with no union-bound cardinality factor. The terminal MGF supplies the variance budget; all-time exponential integrability is explicit for the Jensen producer.

theorem measure_exists_le_martingale_ge_le_exp (hS : Martingale S F μ) (hint : ∀ i t, Integrable (fun ω => exp (t * S i ω)) μ) (n : ℕ) (c : ℝ≥0) (hmgf : HasSubgaussianMGF (S n) c μ) (ε t : ℝ) (ht : 0 < t) : μ {ω | ∃ i, i ≤ n ∧ ε ≤ S i ω} ≤ ENNReal.ofReal (exp (-t * ε + (c : ℝ) * t ^ 2 / 2))

Optimized finite maximal subgaussian bound.

theorem measure_exists_le_martingale_ge_le_subgaussian (hS : Martingale S F μ) (hint : ∀ i t, Integrable (fun ω => exp (t * S i ω)) μ) (n : ℕ) (c : ℝ≥0) (hc : 0 < (c : ℝ)) (hmgf : HasSubgaussianMGF (S n) c μ) (ε : ℝ) (hε : 0 < ε) : μ {ω | ∃ i, i ≤ n ∧ ε ≤ S i ω} ≤ ENNReal.ofReal (exp (-(ε ^ 2) / (2 * (c : ℝ))))

Source Theorem 9.2 shape for independent centered subgaussian increments. The source variance is `c = σ²`; the partial sum uses X1 through Xn. Centering and coordinate measurability are explicit model contracts.

theorem measure_exists_le_independent_partialSum_ge_le_subgaussian (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (c : ℝ≥0) (hc : 0 < (c : ℝ)) (hsubG : ∀ i, HasSubgaussianMGF (X i) c μ) (n : ℕ) (hn : 0 < n) (ε : ℝ) (hε : 0 < ε) : μ {ω | ∃ i, i ≤ n ∧ ε ≤ ∑ j ∈ range i, X (j + 1) ω} ≤ ENNReal.ofReal (exp (-(ε ^ 2) / (2 * (n : ℝ) * (c : ℝ))))