BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.LowerBounds.CommonDensityKL

Chapter 14 Eq. (14.6), with exact common-density and infinite branches.

Module map

Declarations
5
Placeholders
0

Imports

BanditRLProof.LowerBounds.InformationTheory

Imported by

BanditRLProof, BanditRLProof.LowerBounds.CommonDensityOverlap

Declarations

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

theorem BanditRLProof.LowerBounds.llr_ae_eq_log_commonDensity Compiled

The log likelihood ratio is the log ratio of two common-measure densities.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.LowerBounds.llr_ae_eq_log_commonDensity

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

theorem llr_ae_eq_log_commonDensity {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) (hPQ : P ≪ Q) : llr P Q =ᵐ[P] fun x => Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal)
Source line 13 Chapter context: Foundations
theorem BanditRLProof.LowerBounds.integrable_commonDensity_iff Compiled

Integrability of the common-density logarithmic integrand is exactly that of LLR.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.LowerBounds.integrable_commonDensity_iff

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

theorem integrable_commonDensity_iff {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) (hPQ : P ≪ Q) : Integrable (fun x => (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal)) μ ↔ Integrable (llr P Q) P
Source line 22 Chapter context: Foundations
theorem BanditRLProof.LowerBounds.relativeEntropy_commonDensity_of_integrable Compiled

Eq. (14.6) in its supported, integrable probability-measure branch.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.LowerBounds.relativeEntropy_commonDensity_of_integrable

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

theorem relativeEntropy_commonDensity_of_integrable {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) (hPQ : P ≪ Q) (hi : Integrable (fun x => (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal)) μ) : relativeEntropy P Q = ENNReal.ofReal (∫ x, (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal) ∂μ)
Source line 33 Chapter context: Foundations
theorem BanditRLProof.LowerBounds.relativeEntropy_commonDensity_eq_if Compiled

Common-density formula with singular and nonintegrable branches kept infinite.

Used in these reading views: Bandit Book

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

Canonical node identitydeclaration:BanditRLProof.LowerBounds.relativeEntropy_commonDensity_eq_if

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

theorem relativeEntropy_commonDensity_eq_if {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) : relativeEntropy P Q = if P ≪ Q ∧ Integrable (fun x => (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal)) μ then ENNReal.ofReal (∫ x, (P.rnDeriv μ x).toReal * Real.log ((P.rnDeriv μ x).toReal / (Q.rnDeriv μ x).toReal) ∂μ) else (⊤ : ENNReal)
Source line 49 Chapter context: Foundations
theorem BanditRLProof.LowerBounds.relativeEntropy_commonDensity_klFun Compiled

Nonnegative common-density KL integral, valid even at infinite KL under AC.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.LowerBounds.relativeEntropy_commonDensity_klFun

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

theorem relativeEntropy_commonDensity_klFun {α : Type*} [MeasurableSpace α] (P Q μ : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] [SigmaFinite μ] (hP : P ≪ μ) (hQ : Q ≪ μ) (hPQ : P ≪ Q) : relativeEntropy P Q = ∫⁻ x, Q.rnDeriv μ x * ENNReal.ofReal (InformationTheory.klFun ((P.rnDeriv μ x / Q.rnDeriv μ x).toReal)) ∂μ
Source line 68 Chapter context: Foundations