InformationTheory.klDiv_restrict_le
From the authors
Restricting both measures to a measurable set does not increase the divergence.
-
α : Type u_1mα : MeasurableSpace αA measurable space is a space equipped with a σ-algebra.
-
μ : MeasureTheory.Measure αA measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsFiniteMeasure μA measureμis called finite ifμ univ < ∞. -
ν : MeasureTheory.Measure αMeasureTheory.IsFiniteMeasure ν -
s : Set αA set is a collection of elements of some typeα.
-
hs : MeasurableSet sMeasurableSet smeans thatsis measurable (in the ambient measure space onα)
klDiv (μ.restrict s) (ν.restrict s) ≤ klDiv μ νMeasurableSpace : Type u_6 → Type u_6A measurable space is a space equipped with a σ-algebra.
MeasureTheory.IsFiniteMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → PropA measure `μ` is called finite if `μ univ < ∞`.
MeasureTheory.Measure : (α : Type u_5) → [MeasurableSpace α] → Type u_5A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure. The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version is written `μ.real s`.
Set : Type u → Type uA set is a collection of elements of some type `α`.
Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `Set.ofPred` (also written `{x | p x}`) and membership of a set (`∈`) should be
used to convert between sets and predicates.MeasurableSet : {α : Type u_1} → [MeasurableSpace α] → Set α → Prop`MeasurableSet s` means that `s` is measurable (in the ambient measure space on `α`)
LE.le : {α : Type u} → [self : LE α] → α → α → PropThe less-equal relation: `x ≤ y` Conventions for notations in identifiers: * The recommended spelling of `≤` in identifiers is `le`.
InformationTheory.klDiv : {α : Type u_2} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → ENNRealKullback-Leibler divergence between two measures.
MeasureTheory.Measure.restrict : {α : Type u_2} → {_m0 : MeasurableSpace α} → MeasureTheory.Measure α → Set α → MeasureTheory.Measure αRestrict a measure `μ` to a set `s`.
Code
lemma klDiv_restrict_le (hs : MeasurableSet s) :
klDiv (μ.restrict s) (ν.restrict s) ≤ klDiv μ νProof
by rw [← klDiv_restrict_add_restrict_compl (μ := μ) (ν := ν) hs] exact le_add_right le_rfl
Meaning last changed in v4.34.0-rc2-76-g565f652 (2026-09-10).
Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.
Dependency graph
Nothing to draw. Its statement rests on no other declaration in this project, and names nothing from a package left unaudited — so the graph is this declaration alone. That is the answer, not a missing picture.
Audit surface: 0 project declarations, 10 external constants
✓ Proved: no sorry anywhere in its closure
This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.