Lean module · Foundations
BanditRLProof.LowerBounds.BanditHistoryDataProcessing
This module proves the measurable-observation data-processing leaf needed by the stopping-time extension in Lattimore--Szepesvari, *Bandit Algorithms*, Exercise 15.7. It also specializes the leaf to the compiled deterministic finite-history divergence decomposition of Lemma 15.1.
Module map
Imports
BanditRLProof.LowerBounds.BanditHistoryKL, BanditRLProof.LowerBounds.RelativeEntropyFiltration
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.LowerBounds.klDiv_map_le
Compiled
Kullback--Leibler divergence cannot increase under a measurable observation. The proof reuses Chapter 14's map/trim identity and sub-sigma-algebra KL contraction. The infinite-KL branch is explicit, so absolute continuity is derived only in the finite branch and is not a caller assumption.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 15: Minimax Lower Bounds
Canonical node identity
declaration:BanditRLProof.LowerBounds.klDiv_map_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem klDiv_map_le {Source Target : Type*} [MeasurableSpace Source] [MeasurableSpace Target] (mu nu : Measure Source) [IsFiniteMeasure mu] [IsFiniteMeasure nu] (observe : Source -> Target) (hobserve : Measurable observe) : InformationTheory.klDiv (mu.map observe) (nu.map observe) <= InformationTheory.klDiv mu nu
theorem
BanditRLProof.LowerBounds.klDiv_observedBanditHistory_le_expectedPulls_sum
Compiled
Any measurable statistic of a deterministic finite bandit history has KL at most the first-law expected pull-count-weighted arm information. This is the data-processing half of Exercise 15.7 at a fixed horizon. It is not the stopping-time theorem because the right-hand side still counts all pulls through `lastRound`.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 15: Minimax Lower Bounds
Canonical node identity
declaration:BanditRLProof.LowerBounds.klDiv_observedBanditHistory_le_expectedPulls_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem klDiv_observedBanditHistory_le_expectedPulls_sum {K : Nat} {Reward : Type v} {Observation : Type w} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] [MeasurableSpace Observation] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (lastRound : Nat) (observe : History.FinitePairHistory (Fin K) Reward lastRound -> Observation) (hobserve : Measurable observe) : InformationTheory.klDiv ((canonicalBanditHistoryMeasure algorithm armLaw lastRound).map observe) ((canonicalBanditHistoryMeasure algorithm referenceArmLaw lastRound).map observe) <= ∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm * InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm)