BanditRLProof.LowerBounds.InformationTheory

A finite-alphabet binary prefix code. Excluding the empty codeword is the regularity condition needed for concatenations of repeated messages to be uniquely decodable.

structure BinaryPrefixCode (Symbol : Type*) where

A prefix-free codebook with no empty codeword is uniquely decodable.

theorem uniquelyDecodable_range (code : BinaryPrefixCode Symbol) : InformationTheory.UniquelyDecodable (Set.range code.encode)

The finite set of codewords induced by a finite source alphabet.

noncomputable def codebook [Fintype Symbol] [DecidableEq Symbol] (code : BinaryPrefixCode Symbol) : Finset (List Bool)

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

theorem coe_codebook [Fintype Symbol] [DecidableEq Symbol] (code : BinaryPrefixCode Symbol) : (code.codebook : Set (List Bool)) = Set.range code.encode

Kraft--McMillan for a finite binary prefix code, obtained by adapting the codebook to Mathlib's uniquely-decodable-code theorem.

theorem kraft_inequality [Fintype Symbol] [DecidableEq Symbol] (code : BinaryPrefixCode Symbol) : ∑ word ∈ code.codebook, (1 / 2 : Real) ^ word.length ≤ 1

Natural-log entropy (nats) of a finite supported mass function, Eq. (14.3).

noncomputable def discreteEntropy (support : Finset Symbol) (probability : Symbol → Real) : Real

Base-two entropy (bits) of a finite supported mass function.

noncomputable def discreteEntropyBaseTwo (support : Finset Symbol) (probability : Symbol → Real) : Real

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

theorem discreteEntropyBaseTwo_eq_div_log_two (support : Finset Symbol) (probability : Symbol → Real) : discreteEntropyBaseTwo support probability = discreteEntropy support probability / Real.log 2

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

theorem discreteEntropy_nonneg (support : Finset Symbol) (probability : Symbol → Real) (hprobability : ∀ symbol ∈ support, 0 ≤ probability symbol ∧ probability symbol ≤ 1) : 0 ≤ discreteEntropy support probability

Expected binary codeword length, the objective in Eq. (14.1).

noncomputable def expectedCodeLength [Fintype Symbol] (probability : Symbol → Real) (code : BinaryPrefixCode Symbol) : Real

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

theorem expectedCodeLength_nonneg [Fintype Symbol] (probability : Symbol → Real) (code : BinaryPrefixCode Symbol) (hprobability : ∀ symbol, 0 ≤ probability symbol) : 0 ≤ expectedCodeLength probability code

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

Relative entropy vanishes exactly when the finite measures agree.

theorem relativeEntropy_eq_zero_iff {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsFiniteMeasure P] [IsFiniteMeasure Q] : relativeEntropy P Q = 0 ↔ P = Q

Exercise 14.10 in its full sub-sigma-algebra form: forgetting measurable sets cannot increase relative entropy. The proof uses the Radon--Nikodym conditional-expectation identity and conditional Jensen for `klFun`.

theorem relativeEntropy_trim_le {α : Type*} {m m₀ : MeasurableSpace α} {P Q : @Measure α m₀} [IsFiniteMeasure P] [IsFiniteMeasure Q] (hm : m ≤ m₀) : @relativeEntropy α m (P.trim hm) (Q.trim hm) ≤ @relativeEntropy α m₀ P Q

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ᶜ