BanditRLProof.Algorithms.StochasticGradientBanditExponentialAudit

A factorial comparison used to dominate the shifted exponential series.

theorem two_mul_abs_pow_div_factorial_add_two_le (x : Real) (n : Nat) : 2 * |x| ^ n / ((n + 2).factorial : Real) <= |x| ^ n / (n.factorial : Real)

The source constant `C_eta = 2 * sum_{n >= 0} (2 * eta)^n / (n + 2)!`.

noncomputable def sourceC (eta : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceC_terms_summable (eta : Real) : Summable (fun n : Nat => (2 * eta) ^ n / ((n + 2).factorial : Real))

No declaration docstring is present; use the chapter context and exact statement below.

theorem sourceC_nonneg (eta : Real) (heta : 0 <= eta) : 0 <= sourceC eta

Monotonicity needed to replace the time-varying source constants in the Theorem-1 recurrences by a common `C_eta`.

theorem sourceC_mono {eta eta' : Real} (heta : 0 <= eta) (hle : eta <= eta') : sourceC eta <= sourceC eta'

The source comparison following Theorem 1: `C_eta <= exp (2 * eta)`.

theorem sourceC_le_exp_two_mul (eta : Real) (heta : 0 <= eta) : sourceC eta <= Real.exp (2 * eta)

The exponential-series tail beginning at degree two.

noncomputable def expTailTwo (x : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem expTailTwo_terms_summable (x : Real) : Summable (fun n : Nat => x ^ (n + 2) / ((n + 2).factorial : Real))

No declaration docstring is present; use the chapter context and exact statement below.

theorem exp_eq_one_add_self_add_expTailTwo (x : Real) : Real.exp x = 1 + x + expTailTwo x

No declaration docstring is present; use the chapter context and exact statement below.

theorem expTailTwo_le_of_abs_le {x y : Real} (hxy : |x| <= y) : expTailTwo x <= expTailTwo y

No declaration docstring is present; use the chapter context and exact statement below.

theorem sq_div_two_mul_sourceC_abs_div_two (q : Real) : q ^ 2 / 2 * sourceC (|q| / 2) = expTailTwo |q|

Pointwise form of source Equation (8).

theorem exp_mul_le_sourceEqEight (q reward : Real) (hreward : |reward| <= 1) : Real.exp (q * reward) <= 1 + q * reward + q ^ 2 / 2 * sourceC (|q| / 2)

Expectation form of source Equation (8), with integrability explicit.

theorem integral_exp_mul_le_sourceEqEight {Omega : Type*} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (q : Real) (reward : Omega -> Real) (hrewardIntegrable : MeasureTheory.Integrable reward mu) (hexpIntegrable : MeasureTheory.Integrable (fun omega => Real.exp (q * reward omega)) mu) (hreward : ∀ᵐ omega ∂mu, |reward omega| <= 1) : (∫ omega, Real.exp (q * reward omega) ∂mu) <= 1 + q * (∫ omega, reward omega ∂mu) + q ^ 2 / 2 * sourceC (|q| / 2)

Equation (8) from measurability and almost-sure support in `[-1, 1]`.

theorem integral_exp_mul_le_sourceEqEight_of_ae_abs_le_one {Omega : Type*} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (q : Real) (reward : Omega -> Real) (hrewardMeasurable : MeasureTheory.AEStronglyMeasurable reward mu) (hreward : ∀ᵐ omega ∂mu, |reward omega| <= 1) : (∫ omega, Real.exp (q * reward omega) ∂mu) <= 1 + q * (∫ omega, reward omega ∂mu) + q ^ 2 / 2 * sourceC (|q| / 2)