Lean module · Foundations
BanditRLProof.LowerBounds.CrossEntropy
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.
def
BanditRLProof.LowerBounds.discreteCrossEntropy
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
Canonical node identity
declaration:BanditRLProof.LowerBounds.discreteCrossEntropyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def discreteCrossEntropy {α : Type*} [Fintype α] (p q : α → ℝ) : ℝ
theorem
BanditRLProof.LowerBounds.discreteCrossEntropy_sub_entropy
Compiled
The unrounded information-cost interpretation of Eq. (14.4).
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.discreteCrossEntropy_sub_entropyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem discreteCrossEntropy_sub_entropy {α : Type*} [Fintype α] (p q : α → ℝ) (hsupport : ∀ i, p i ≠ 0 → q i ≠ 0) : discreteCrossEntropy p q - discreteEntropy Finset.univ p = ∑ i, p i * Real.log (p i / q i)
theorem
BanditRLProof.LowerBounds.relativeEntropy_finite_crossEntropy
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.relativeEntropy_finite_crossEntropyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_finite_crossEntropy {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (h : P ≪ Q) : relativeEntropy P Q = ENNReal.ofReal (discreteCrossEntropy (fun i => (P {i}).toReal) (fun i => (Q {i}).toReal) - discreteEntropy Finset.univ (fun i => (P {i}).toReal))
theorem
BanditRLProof.LowerBounds.entropyTerm_tendsto_zero_right
Compiled
The source's zero-mass entropy convention agrees with the right-hand limit.
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.entropyTerm_tendsto_zero_rightReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem entropyTerm_tendsto_zero_right : Filter.Tendsto (fun x : ℝ => x * Real.log x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)