Lean module · Foundations

BanditRLProof.LowerBounds.FinitePartitionKLRecovery

The finite-discretisation definition of KL equals the RN definition.

Module map

Source: BanditRLProof/LowerBounds/FinitePartitionKLRecovery.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 4
Placeholders: 0

Imports

BanditRLProof.LowerBounds.FinitePartitionKL, BanditRLProof.LowerBounds.RelativeEntropyFiltration

Imported by

BanditRLProof

Declarations

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

theorem BanditRLProof.LowerBounds.exists_fin_encoding_of_finite_range Compiled

A measurable finite-range map admits a finite code and an exact decoder.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.LowerBounds.exists_fin_encoding_of_finite_range

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

theorem exists_fin_encoding_of_finite_range {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (f : α → β) (hf : Measurable f) (hfin : (Set.range f).Finite) : ∃ (n : ℕ) (g : α → Fin n), Measurable g ∧ ∃ d : Fin n → β, f = d ∘ g

Source line 15 Chapter context: Foundations

theorem BanditRLProof.LowerBounds.exists_fin_observation_densityApproximation Compiled

Each density-approximation layer is contained in a finite observation sigma-algebra.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.LowerBounds.exists_fin_observation_densityApproximation

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

theorem exists_fin_observation_densityApproximation {α : Type*} [m : MeasurableSpace α] (r : α → ENNReal) (n : ℕ) : ∃ (k : ℕ) (g : α → Fin k) (_hg : Measurable g), densityApproximationFiltration r n ≤ (inferInstance : MeasurableSpace (Fin k)).comap g

Source line 31 Chapter context: Foundations

theorem BanditRLProof.LowerBounds.relativeEntropy_trim_mono Compiled

Refining a sub-sigma-algebra can only increase its retained KL.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.LowerBounds.relativeEntropy_trim_mono

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

theorem relativeEntropy_trim_mono {α : Type*} {m₁ m₂ m₀ : MeasurableSpace α} (P Q : @Measure α m₀) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h₁₂ : m₁ ≤ m₂) (h₂ : m₂ ≤ m₀) : @relativeEntropy α m₁ (P.trim (h₁₂.trans h₂)) (Q.trim (h₁₂.trans h₂)) ≤ @relativeEntropy α m₂ (P.trim h₂) (Q.trim h₂)

Source line 56 Chapter context: Foundations

theorem BanditRLProof.LowerBounds.finitePartitionRelativeEntropy_eq_relativeEntropy Compiled

Textbook Eq. (14.5) and Theorem 14.1: finite discretisations recover RN KL.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret · Chapter 14: Foundations of Information Theory

Canonical node identity

declaration:BanditRLProof.LowerBounds.finitePartitionRelativeEntropy_eq_relativeEntropy

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

theorem finitePartitionRelativeEntropy_eq_relativeEntropy {α : Type*} [m : MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : finitePartitionRelativeEntropy P Q = relativeEntropy P Q

Source line 65 Chapter context: Foundations