BanditRLProof.LowerBounds.RelativeEntropyFiltration

Trimmed KL as the convex lower integral of the conditional RN density.

theorem relativeEntropy_trim_eq_lintegral_condExp {α : Type*} {m m₀ : MeasurableSpace α} (P Q : @Measure α m₀) [IsFiniteMeasure P] [IsFiniteMeasure Q] (hm : m ≤ m₀) (h : P ≪ Q) : @relativeEntropy α m (P.trim hm) (Q.trim hm) = ∫⁻ x, ENNReal.ofReal (InformationTheory.klFun (Q[fun y => (P.rnDeriv Q y).toReal | m] x)) ∂Q

A measurable observation has the same KL as restriction to its generated sigma-algebra.

theorem relativeEntropy_map_eq_trim_of_absolutelyContinuous {α β : Type*} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) (f : α → β) (hf : Measurable f) : relativeEntropy (P.map f) (Q.map f) = @relativeEntropy α (mβ.comap f) (P.trim hf.comap_le) (Q.trim hf.comap_le)

Resolving the RN density along a filtration recovers KL, including infinite KL.

theorem relativeEntropy_eq_iSup_trim_of_density_measurable {α : Type*} [m₀ : MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) (F : Filtration ℕ m₀) (hDensity : StronglyMeasurable[⨆ n, F n] (fun x => (P.rnDeriv Q x).toReal)) : relativeEntropy P Q = ⨆ n, @relativeEntropy α (F n) (P.trim (F.le n)) (Q.trim (F.le n))

Natural filtration of the finite-valued lower approximations to a density.

def densityApproximationFiltration {α : Type*} [m : MeasurableSpace α] (r : α → ENNReal) : Filtration ℕ m

The limiting sigma-algebra of the approximation filtration resolves the density.

theorem measurable_density_iSup_approximationFiltration {α : Type*} [m : MeasurableSpace α] (r : α → ENNReal) (hr : Measurable r) : Measurable[⨆ n, densityApproximationFiltration r n] r

RN KL is recovered along a concretely constructed simple-approximation filtration.

theorem relativeEntropy_eq_iSup_densityApproximation_trim {α : Type*} [m : MeasurableSpace α] (P Q : Measure α) [IsFiniteMeasure P] [IsFiniteMeasure Q] (h : P ≪ Q) : relativeEntropy P Q = ⨆ n, @relativeEntropy α (densityApproximationFiltration (P.rnDeriv Q) n) (P.trim ((densityApproximationFiltration (P.rnDeriv Q)).le n)) (Q.trim ((densityApproximationFiltration (P.rnDeriv Q)).le n))