BanditRLProof.LowerBounds.InformationTheory

Chapter 14 relative entropy, with value `∞` on support mismatch or a non-integrable log-likelihood ratio.

abbrev relativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) : ENNReal

The finite regular branch of the Radon--Nikodym representation. The mass correction vanishes when `P` and `Q` are probability measures.

theorem relativeEntropy_of_absolutelyContinuous_of_integrable {α : Type*} [MeasurableSpace α] (P Q : Measure α) (hPQ : P ≪ Q) (hInt : Integrable (llr P Q) P) : relativeEntropy P Q = ENNReal.ofReal (∫ x, llr P Q x ∂P + Q.real univ - P.real univ)

Probability-measure specialization of Theorem 14.1: the finite relative entropy is exactly the expected log likelihood ratio.

theorem relativeEntropy_of_probability_absolutelyContinuous_of_integrable {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hPQ : P ≪ Q) (hInt : Integrable (llr P Q) P) : relativeEntropy P Q = ENNReal.ofReal (∫ x, llr P Q x ∂P)

The singular branch of Theorem 14.1.

theorem relativeEntropy_eq_top_of_not_absolutelyContinuous {α : Type*} [MeasurableSpace α] {P Q : Measure α} (hPQ : ¬ P ≪ Q) : relativeEntropy P Q = ∞

Exact finiteness contract for the Mathlib representation of Chapter 14 relative entropy.

theorem relativeEntropy_ne_top_iff {α : Type*} [MeasurableSpace α] {P Q : Measure α} : relativeEntropy P Q ≠ ∞ ↔ P ≪ Q ∧ Integrable (llr P Q) P

The Bernoulli relative entropy from Eq. (14.4), reusing the project's exact support and endpoint convention.

abbrev bernoulliRelativeEntropy (p q : Real) : ENNReal

Restricting both laws to a measurable event preserves the original Radon--Nikodym derivative almost everywhere on that event.

theorem rnDeriv_restrict_restrict {α : Type*} [MeasurableSpace α] {P Q : Measure α} [SigmaFinite P] [SigmaFinite Q] (hPQ : P ≪ Q) {A : Set α} (hA : MeasurableSet A) : (P.restrict A).rnDeriv (Q.restrict A) =ᵐ[Q.restrict A] P.rnDeriv Q

Relative entropy splits exactly across an event and its complement. This is the two-cell partition identity used by the event data-processing proof.

theorem relativeEntropy_restrict_add_compl {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsFiniteMeasure P] [IsFiniteMeasure Q] (hPQ : P ≪ Q) {A : Set α} (hA : MeasurableSet A) : relativeEntropy P Q = relativeEntropy (P.restrict A) (Q.restrict A) + relativeEntropy (P.restrict Aᶜ) (Q.restrict Aᶜ)

Event data processing in the finite, non-singular Bernoulli branch. This is the quantitative core of Exercise 14.10 specialized to the sigma-algebra generated by one event.

theorem bernoulliKLCore_event_le {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) (hKL : relativeEntropy P Q ≠ ∞) (hQ0 : 0 < Q.real A) (hQ1 : Q.real A < 1) : KLUCB.bernoulliKLCore (P.real A) (Q.real A) ≤ (relativeEntropy P Q).toReal

No declaration docstring is present; use the chapter context and exact statement below.

private theorem mul_sqrt_div_eq_sqrt_mul {a b : Real} (ha : 0 < a) (hb : 0 ≤ b) : a * Real.sqrt (b / a) = Real.sqrt (a * b)

The binary likelihood affinity dominates `exp(-d/2)`. This is the two-atom Jensen step in the source proof of Theorem 14.2.

theorem exp_neg_half_bernoulliKLCore_le_affinity {p q : Real} (hp0 : 0 < p) (hp1 : p < 1) (hq0 : 0 < q) (hq1 : q < 1) : Real.exp (-(KLUCB.bernoulliKLCore p q) / 2) ≤ Real.sqrt (p * q) + Real.sqrt ((1 - p) * (1 - q))

The two-atom Le Cam overlap inequality in the orientation needed for an event `A`: the affinity squared, divided by two, is bounded by `p + (1 - q)`.

theorem half_binaryAffinity_sq_le_eventError {p q : Real} (hp : KLUCB.IsBernoulliParameter p) (hq : KLUCB.IsBernoulliParameter q) : (1 / 2 : Real) * (Real.sqrt (p * q) + Real.sqrt ((1 - p) * (1 - q))) ^ 2 ≤ p + (1 - q)

Bretagnolle--Huber for the finite analytic Bernoulli KL expression.

theorem binaryBretagnolleHuberCore {p q : Real} (hp : KLUCB.IsBernoulliParameter p) (hq0 : 0 < q) (hq1 : q < 1) : (1 / 2 : Real) * Real.exp (-KLUCB.bernoulliKLCore p q) ≤ p + (1 - q)

The source convention `exp(-∞)=0`, exposed as a real-valued testing scale so Theorem 14.2 remains unconditional.

noncomputable def bretagnolleHuberScale (d : ENNReal) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem bretagnolleHuberScale_nonneg (d : ENNReal) : 0 ≤ bretagnolleHuberScale d

Exact two-atom Bretagnolle--Huber inequality, including singular Bernoulli endpoints through the extended-real testing scale.

theorem binaryBretagnolleHuber {p q : Real} (hp : KLUCB.IsBernoulliParameter p) (hq : KLUCB.IsBernoulliParameter q) : bretagnolleHuberScale (bernoulliRelativeEntropy p q) ≤ p + (1 - q)

Event-level binary data processing: observing only membership in `A` cannot increase the relative entropy.

theorem bernoulliRelativeEntropy_event_le {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bernoulliRelativeEntropy (P.real A) (Q.real A) ≤ relativeEntropy P Q

The Bretagnolle--Huber testing scale is antitone in its information argument.

theorem bretagnolleHuberScale_antitone {d D : ENNReal} (h : d ≤ D) : bretagnolleHuberScale D ≤ bretagnolleHuberScale d

*Bretagnolle--Huber inequality** (Lattimore--Szepesvári, Theorem 14.2). For any measurable event, the two testing errors are bounded below in the source KL direction `D(P,Q)`. The infinite-divergence case is included by `bretagnolleHuberScale`.

theorem bretagnolleHuber {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bretagnolleHuberScale (relativeEntropy P Q) ≤ P.real A + Q.real Aᶜ