BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.RealMeanRegretPullCount

This module provides the Real-valued finite-arm bookkeeping surface needed by the exact LML ETC route. It is parameterized by an arm-mean function, so a later kernel bridge can instantiate mean a with the integral of the identity under arm a without changing the deterministic or Bochner proofs here.

Module map

Declarations
6
Placeholders
0

Imports

BanditRLProof.ExpectationBochnerSums, BanditRLProof.IntegrabilitySums, BanditRLProof.MathlibWrappers

Imported by

BanditRLProof, BanditRLProof.Algorithms.HeavyTailRegret, BanditRLProof.Algorithms.MOSSRegret, BanditRLProof.RealKernelRegretPullCount

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.realMeanGap Compiled

Gap from the supremum finite-arm mean, matching the scalar semantics of LML's bandit gap.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.realMeanGap

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def realMeanGap {K : Nat} (mean : Fin K -> Real) (a : Fin K) : Real
Source line 22 Chapter context: Foundations
def BanditRLProof.realMeanRegret Compiled

Real pseudo-regret written directly from arm means over a finite horizon.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.realMeanRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def realMeanRegret {K : Nat} (mean : Fin K -> Real) (action : ActionTrace (Fin K)) (n : Nat) : Real
Source line 26 Chapter context: Foundations
theorem BanditRLProof.realMeanRegret_eq_finset_sum_gap Compiled

Real mean regret is the time-indexed finite sum of selected arm gaps.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.realMeanRegret_eq_finset_sum_gap

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem realMeanRegret_eq_finset_sum_gap {K : Nat} (mean : Fin K -> Real) (action : ActionTrace (Fin K)) (n : Nat) : realMeanRegret mean action n = (Finset.range n).sum (fun t => realMeanGap mean (action t))
Source line 32 Chapter context: Foundations
theorem BanditRLProof.realMeanRegret_eq_sum_gap_mul_pullCount Compiled

Real mean regret decomposes into each arm gap times its finite-horizon pull count. This is the deterministic half of `REAL-MEAN-REGRET-PULLCOUNT`. The definition uses the same supremum-minus-mean gap as the exact LML theorem card; no rational model, kernel law, measurability, or concentration assumption appears here.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.realMeanRegret_eq_sum_gap_mul_pullCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem realMeanRegret_eq_sum_gap_mul_pullCount {K : Nat} (mean : Fin K -> Real) (action : ActionTrace (Fin K)) (n : Nat) : realMeanRegret mean action n = (Finset.univ : Finset (Fin K)).sum (fun a => realMeanGap mean a * (pullCount action a n : Real))
Source line 48 Chapter context: Foundations
theorem BanditRLProof.integrable_realMeanRegret_of_integrable_pullCount Compiled

Pull-count integrability implies integrability of Real mean regret.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.integrable_realMeanRegret_of_integrable_pullCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem integrable_realMeanRegret_of_integrable_pullCount {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (mean : Fin K -> Real) (action : Omega -> ActionTrace (Fin K)) (n : Nat) (hcount : forall a : Fin K, Integrable (fun omega => (pullCount (action omega) a n : Real)) mu) : Integrable (fun omega => realMeanRegret mean (action omega) n) mu
Source line 70 Chapter context: Foundations
theorem BanditRLProof.integral_realMeanRegret_eq_sum_gap_mul_integral_pullCount Compiled

The Bochner expectation of Real mean regret is the gap-weighted sum of expected pull counts. This is the expectation half of `REAL-MEAN-REGRET-PULLCOUNT`. Callers supply only pull-count integrability; probability-space, policy, reward-law, and sub-Gaussian contracts remain outside this bookkeeping leaf.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.integral_realMeanRegret_eq_sum_gap_mul_integral_pullCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem integral_realMeanRegret_eq_sum_gap_mul_integral_pullCount {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (mean : Fin K -> Real) (action : Omega -> ActionTrace (Fin K)) (n : Nat) (hcount : forall a : Fin K, Integrable (fun omega => (pullCount (action omega) a n : Real)) mu) : integral mu (fun omega => realMeanRegret mean (action omega) n) = (Finset.univ : Finset (Fin K)).sum (fun a => realMeanGap mean a * integral mu (fun omega => (pullCount (action omega) a n : Real)))
Source line 106 Chapter context: Foundations