Lean module · Foundations
BanditRLProof.LowerBounds.FiniteDiscreteKL
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.InformationTheory
Imported by
BanditRLProof, BanditRLProof.LowerBounds.CommonDomination, BanditRLProof.LowerBounds.CrossEntropy, BanditRLProof.LowerBounds.FinitePartitionKL
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.LowerBounds.absolutelyContinuous_iff_atom_support
Compiled
On a finite alphabet, absolute continuity is exactly atomwise support inclusion.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.absolutelyContinuous_iff_atom_supportReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem absolutelyContinuous_iff_atom_support {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) : P ≪ Q ↔ ∀ x, Q {x} = 0 → P {x} = 0
theorem
BanditRLProof.LowerBounds.rnDeriv_mul_atom
Compiled
Atomwise density identity, retaining zero-mass atoms.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.rnDeriv_mul_atomReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem rnDeriv_mul_atom {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) (x : α) : P.rnDeriv Q x * Q {x} = P {x}
theorem
BanditRLProof.LowerBounds.rnDeriv_atom_eq_div
Compiled
On a positive reference atom, the RN density is the atom-mass ratio.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.rnDeriv_atom_eq_divReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem rnDeriv_atom_eq_div {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) (x : α) (hq : Q {x} ≠ 0) : P.rnDeriv Q x = P {x} / Q {x}
theorem
BanditRLProof.LowerBounds.relativeEntropy_eq_top_of_atom_support_mismatch
Compiled
A positive source atom absent from the reference law forces infinite KL.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.relativeEntropy_eq_top_of_atom_support_mismatchReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_eq_top_of_atom_support_mismatch {α : Type*} [MeasurableSpace α] (P Q : Measure α) (x : α) (hp : P {x} ≠ 0) (hq : Q {x} = 0) : relativeEntropy P Q = ∞
theorem
BanditRLProof.LowerBounds.relativeEntropy_finite_klFun
Compiled
Finite-alphabet KL in its nonnegative convex-integrand form.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.relativeEntropy_finite_klFunReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_finite_klFun {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) : relativeEntropy P Q = ∑ x, ENNReal.ofReal (InformationTheory.klFun ((P {x} / Q {x}).toReal)) * Q {x}
theorem
BanditRLProof.LowerBounds.relativeEntropy_finite_sum_log
Compiled
Textbook Eq. (14.4) on any finite alphabet in the supported branch.
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.relativeEntropy_finite_sum_logReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_finite_sum_log {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (h : P ≪ Q) : relativeEntropy P Q = ENNReal.ofReal (∑ x, (P {x}).toReal * Real.log ((P {x}).toReal / (Q {x}).toReal))
theorem
BanditRLProof.LowerBounds.relativeEntropy_finite_eq_if
Compiled
Eq. (14.4), including the infinite branch when atomwise support fails.
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.relativeEntropy_finite_eq_ifReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_finite_eq_if {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : relativeEntropy P Q = if ∀ x, Q {x} = 0 → P {x} = 0 then ENNReal.ofReal (∑ x, (P {x}).toReal * Real.log ((P {x}).toReal / (Q {x}).toReal)) else ∞
theorem
BanditRLProof.LowerBounds.relativeEntropy_finite_eq_top_iff
Compiled
Finite alphabets have infinite KL exactly at a support mismatch.
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.relativeEntropy_finite_eq_top_iffReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_finite_eq_top_iff {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : relativeEntropy P Q = ∞ ↔ ∃ x, P {x} ≠ 0 ∧ Q {x} = 0