Lower semicontinuity of relative entropy along density convergence

For a finite reference measure ρ, relative entropy is lower semicontinuous along sequences of measures whose Radon–Nikodym densities with respect to ρ converge ρ-almost everywhere: the measure with the limit density has relative entropy at most the liminf of the entropies. The proof is Fatou's lemma applied to the entropy integrand InformationTheory.klFun of the densities.

Main results

• TauCeti.klDiv_withDensity_le_liminf: if the densities of measures p n converge ρ-almost everywhere to g, then klDiv (ρ.withDensity g) ρ is at most liminf (klDiv (p n) ρ).

theorem TauCeti.klDiv_withDensity_le_liminf {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure α} {p : ℕ → MeasureTheory.Measure α} {g : α → ℝ} [MeasureTheory.IsFiniteMeasure ρ] [MeasureTheory.IsFiniteMeasure (ρ.withDensity fun (z : α) => ENNReal.ofReal (g z))] [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (p n)] (hlim : ∀ᵐ (z : α) ∂ρ, Filter.Tendsto (fun (n : ℕ) => ((p n).rnDeriv ρ z).toReal) Filter.atTop (nhds (g z))) : InformationTheory.klDiv (ρ.withDensity fun (z : α) => ENNReal.ofReal (g z)) ρ ≤ Filter.liminf (fun (n : ℕ) => InformationTheory.klDiv (p n) ρ) Filter.atTop

Lower semicontinuity of relative entropy along density convergence. If the densities (p n).rnDeriv ρ of measures p n converge ρ-almost everywhere to g, then the measure with density g has relative entropy at most the liminf of the relative entropies klDiv (p n) ρ, by Fatou's lemma. A measure which is not absolutely continuous has infinite entropy.