Lean module · Foundations
BanditRLProof.LowerBounds.RelativeEntropyNonMetric
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.LowerBounds.GaussianTesting
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.relativeEntropy_triangle_counterexample
Compiled
A finite-valued Gaussian counterexample to the triangle inequality.
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_triangle_counterexampleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem relativeEntropy_triangle_counterexample : relativeEntropy (gaussianReal 0 1) (gaussianReal 1 1) + relativeEntropy (gaussianReal 1 1) (gaussianReal 2 1) < relativeEntropy (gaussianReal 0 1) (gaussianReal 2 1)
theorem
BanditRLProof.LowerBounds.bernoulliRelativeEntropy_asymmetry
Compiled
Reversing the Bernoulli comparison can change finite KL to infinite 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.bernoulliRelativeEntropy_asymmetryReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem bernoulliRelativeEntropy_asymmetry : bernoulliRelativeEntropy 0 (1 / 2) ≠ bernoulliRelativeEntropy (1 / 2) 0