Lean module · Foundations
BanditRLProof.LowerBounds.CommonDomination
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.FiniteDiscreteKL
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.exists_commonFiniteDominatingMeasure
Compiled
The sum of two finite laws supplies the common dominating measure in the source.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.exists_commonFiniteDominatingMeasureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_commonFiniteDominatingMeasure {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : ∃ μ : Measure α, IsFiniteMeasure μ ∧ P ≪ μ ∧ Q ≪ μ
theorem
BanditRLProof.LowerBounds.exists_commonSigmaFiniteDominatingMeasure
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
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.exists_commonSigmaFiniteDominatingMeasureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_commonSigmaFiniteDominatingMeasure {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : ∃ μ : Measure α, SigmaFinite μ ∧ P ≪ μ ∧ Q ≪ μ
theorem
BanditRLProof.LowerBounds.relativeEntropy_finite_lt_top_iff_ac
Compiled
Absolute continuity suffices for finite KL on a finite alphabet, not in general.
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_lt_top_iff_acReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_finite_lt_top_iff_ac {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] : relativeEntropy P Q < ⊤ ↔ P ≪ Q