A finite-epoch maximal inequality for the reverse Bessel process

Doob's maximal inequality applied to the nonnegative exponential transform of the reverse Bessel martingale controls a crossing anywhere in a finite reverse sample-size epoch by the full expectation at the epoch endpoint.

At reverse-process time k, the underlying Bessel variance uses prefix size max 2 (N - k). Thus the specialization with horizon N - m, for 2 ≤ m ≤ N, covers every prefix size from N down to m using one fixed coefficient, center, and deterministic penalty.

This module does not bound the endpoint expectation by one, connect it to the fixed-sample empirical-variance MGF, optimize the coefficient, stitch epochs, or state a PAC-Bayes theorem.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselExponentialProcess_maximal_ineq {Z : Type u_1} [MeasurableSpace Z] [Fintype Z] [MeasurableSingletonClass Z] (mu : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure mu] (N : ℕ) (hN : 2 ≤ N) (ell : Z → ℝ) (center lam penalty : ℝ) (ε : NNReal) (r : ℕ) : ↑ε * (MeasureTheory.Measure.pi fun (x : Fin N) => mu) {x : Fin N → Z | ↑ε ≤ (Finset.range (r + 1)).sup' ⋯ fun (k : ℕ) => reverseBesselExponentialProcess N hN ell center lam penalty k x} ≤ ENNReal.ofReal (∫ (x : Fin N → Z), reverseBesselExponentialProcess N hN ell center lam penalty r x ∂MeasureTheory.Measure.pi fun (x : Fin N) => mu)

Doob's finite-horizon inequality for the reverse-Bessel exponential submartingale, strengthened from the crossing-event integral to the full endpoint expectation.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselExponentialProcess_epoch_endpoint {Z : Type u_1} (N m : ℕ) (hN : 2 ≤ N) (hm : 2 ≤ m ∧ m ≤ N) (ell : Z → ℝ) (center lam penalty : ℝ) : reverseBesselExponentialProcess N hN ell center lam penalty (N - m) = fun (x : Fin N → Z) => Real.exp (lam * (center - prefixBesselVariance ⋯ ell x) - penalty)

At reverse time N - m, an epoch ending at m has exactly the prefix-m Bessel-variance exponential as its endpoint.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselExponentialProcess_epoch_maximal_ineq {Z : Type u_1} [MeasurableSpace Z] [Fintype Z] [MeasurableSingletonClass Z] (mu : MeasureTheory.Measure Z) [MeasureTheory.IsProbabilityMeasure mu] (N m : ℕ) (hN : 2 ≤ N) (hm : 2 ≤ m ∧ m ≤ N) (ell : Z → ℝ) (center lam penalty : ℝ) (ε : NNReal) : ↑ε * (MeasureTheory.Measure.pi fun (x : Fin N) => mu) {x : Fin N → Z | ↑ε ≤ (Finset.range (N - m + 1)).sup' ⋯ fun (k : ℕ) => reverseBesselExponentialProcess N hN ell center lam penalty k x} ≤ ENNReal.ofReal (∫ (x : Fin N → Z), Real.exp (lam * (center - prefixBesselVariance ⋯ ell x) - penalty) ∂MeasureTheory.Measure.pi fun (x : Fin N) => mu)

The epoch form of reverseBesselExponentialProcess_maximal_ineq: reverse times 0, ..., N - m correspond exactly to prefix sizes N, ..., m when 2 ≤ m ≤ N. The endpoint is exposed as a prefix-m statistic for the subsequent product-measure MGF bridge.