Lean module · Foundations

BanditRLProof.RealMeanRegretPullCount

# Real mean-regret pull-count decomposition 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

Source: BanditRLProof/RealMeanRegretPullCount.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 6
Placeholders: 0

Imports

BanditRLProof.ExpectationBochnerSums, BanditRLProof.IntegrabilitySums, BanditRLProof.MathlibWrappers

Imported by

BanditRLProof, 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.

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.

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.

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.

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.

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.

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