Exponential transforms of the reverse Bessel martingale

For a fixed horizon and fixed exponential coefficient, an affine transform of the reverse Bessel martingale remains a martingale. Conditional Jensen then makes its exponential a nonnegative submartingale. This is the load-bearing process needed to apply Doob's finite-horizon maximal inequality to a whole sample-size epoch.

The coefficient, center, and deterministic penalty are fixed before process time. In particular, this module does not claim that a coefficient depending on the moving prefix size produces a submartingale. It also does not yet connect the endpoint expectation to the finite-product empirical-variance MGF or state a PAC-Bayes result.

noncomputable def FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselAffineScore {Z : Type u_1} (N : ℕ) (hN : 2 ≤ N) (ell : Z → ℝ) (center lam penalty : ℝ) : ℕ → (Fin N → Z) → ℝ

A fixed affine lower-tail score built from the reverse Bessel process.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselAffineScore_martingale {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 : ℝ) : MeasureTheory.Martingale (reverseBesselAffineScore N hN ell center lam penalty) (reverseBesselFiltration N) (MeasureTheory.Measure.pi fun (x : Fin N) => mu)

noncomputable def FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselExponentialProcess {Z : Type u_1} (N : ℕ) (hN : 2 ≤ N) (ell : Z → ℝ) (center lam penalty : ℝ) : ℕ → (Fin N → Z) → ℝ

Exponential of the fixed affine reverse-Bessel score.

Equations

• One or more equations did not get rendered due to their size.

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselExponentialProcess_submartingale {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 : ℝ) : MeasureTheory.Submartingale (reverseBesselExponentialProcess N hN ell center lam penalty) (reverseBesselFiltration N) (MeasureTheory.Measure.pi fun (x : Fin N) => mu)

theorem FormalSLT.PACBayes.FiniteEmpiricalVarianceReverse.reverseBesselExponentialProcess_nonneg {Z : Type u_1} (N : ℕ) (hN : 2 ≤ N) (ell : Z → ℝ) (center lam penalty : ℝ) : 0 ≤ reverseBesselExponentialProcess N hN ell center lam penalty