BanditRLProof.LowerBounds.FinitePartitionKL

Convexity bounds the divergence of total masses by finite-measure KL.

theorem totalMass_klFun_le_relativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : ENNReal.ofReal (InformationTheory.klFun ((P univ / Q univ).toReal)) * Q univ ≤ relativeEntropy P Q

KL splits into the restrictions to all cells of a finite observation.

theorem sum_relativeEntropy_restrict_fibers {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) {n : ℕ} (f : α → Fin n) (hf : Measurable f) : (∑ i, relativeEntropy (P.restrict (f ⁻¹' {i})) (Q.restrict (f ⁻¹' {i}))) = relativeEntropy P Q

Finite-valued measurable observations cannot increase KL.

theorem relativeEntropy_finite_map_le {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] {n : ℕ} (f : α → Fin n) (hf : Measurable f) : relativeEntropy (P.map f) (Q.map f) ≤ relativeEntropy P Q

Relative entropy defined by the supremum over finite measurable observations.

def finitePartitionRelativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) : ENNReal

The finite-discretisation supremum never exceeds RN relative entropy.

theorem finitePartitionRelativeEntropy_le_relativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] : finitePartitionRelativeEntropy P Q ≤ relativeEntropy P Q

Every finite measurable observation is included in the defining supremum.

theorem relativeEntropy_map_le_finitePartitionRelativeEntropy {α : Type*} [MeasurableSpace α] (P Q : Measure α) {n : ℕ} (f : α → Fin n) (hf : Measurable f) : relativeEntropy (P.map f) (Q.map f) ≤ finitePartitionRelativeEntropy P Q

On an already finite observation space, the identity partition loses nothing.

theorem finitePartitionRelativeEntropy_fin_eq {n : ℕ} (P Q : Measure (Fin n)) [IsFiniteMeasure P] [IsFiniteMeasure Q] : finitePartitionRelativeEntropy P Q = relativeEntropy P Q

The discrete KL of an observation is the exact cell-mass formula.

theorem relativeEntropy_finite_map_eq_if {α : Type*} [MeasurableSpace α] (P Q : Measure α) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {n : ℕ} (f : α → Fin n) (hf : Measurable f) : relativeEntropy (P.map f) (Q.map f) = if ∀ i, Q (f ⁻¹' {i}) = 0 → P (f ⁻¹' {i}) = 0 then ENNReal.ofReal (∑ i, (P (f ⁻¹' {i})).toReal * Real.log ((P (f ⁻¹' {i})).toReal / (Q (f ⁻¹' {i})).toReal)) else (⊤ : ENNReal)

A measurable support mismatch is detected by a two-cell observation.

theorem exists_binary_map_relativeEntropy_eq_top_of_event {α : Type*} [MeasurableSpace α] (P Q : Measure α) {A : Set α} (hA : MeasurableSet A) (hp : P A ≠ 0) (hq : Q A = 0) : ∃ f : α → Fin 2, Measurable f ∧ relativeEntropy (P.map f) (Q.map f) = (⊤ : ENNReal)

Non-absolute-continuity forces infinite finite-partition relative entropy.

theorem finitePartitionRelativeEntropy_eq_top_of_not_absolutelyContinuous {α : Type*} [MeasurableSpace α] (P Q : Measure α) (h : ¬ P ≪ Q) : finitePartitionRelativeEntropy P Q = (⊤ : ENNReal)

The finite-partition and RN definitions agree in the singular branch.

theorem finitePartitionRelativeEntropy_eq_relativeEntropy_of_not_absolutelyContinuous {α : Type*} [MeasurableSpace α] (P Q : Measure α) (h : ¬ P ≪ Q) : finitePartitionRelativeEntropy P Q = relativeEntropy P Q