`PFR/Kullback.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

21 declarations, 0 contain sorry, 0 declared as axioms

Kullback-Leibler divergence

Definition of Kullback-Leibler divergence and basic facts

Imports (5)

Imported by 2 files

def KLDiv If X, Y are two G-valued random variables, the Kullback--Leibler divergence is defined as KL(X ‖ Y) := ∑ₓ 𝐏(X = x) log (𝐏(X = x) / 𝐏(Y = x)) line 35 source
Source documentation
If X, Y are two G-valued random variables, the Kullback--Leibler divergence is defined as KL(X ‖ Y) := ∑ₓ 𝐏(X = x) log (𝐏(X = x) / 𝐏(Y = x)).
Note that this definition only makes sense when X is absolutely continuous wrt to Y, i.e., ∀ x, 𝐏(Y = x) = 0 → 𝐏(X = x) = 0. Otherwise, the divergence should be infinite, but since we use real numbers for ease of computations, this is not a possible choice.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: tsum, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.log, HDiv.hDiv, SummationFilter.unconditional
12 instances, coercions and auxiliary constants left out.
```
noncomputable def KLDiv (X : Ω → G) (Y : Ω' → G) (μ : Measure Ω := by volume_tac)
…
```
lemma KLDiv_self line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, KLDiv, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, tsum, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.log, HDiv.hDiv, SummationFilter.unconditional, SummationFilter, optParam, funext, Real.log_div_self, MulZeroClass.mul_zero, tsum_zero and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IdentDistrib.KLDiv_eq If X' is a copy of X, and Y' is a copy of Y, then KL(X' ‖ Y') = KL(X ‖ Y) line 46 source
Source documentation
If X' is a copy of X, and Y' is a copy of Y, then KL(X' ‖ Y') = KL(X ‖ Y).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IdentDistrib, Eq, Real, KLDiv
Proof uses: id, AddCommMonoid, TopologicalSpace, Eq.rec, SummationFilter, tsum, Eq.refl, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.log, HDiv.hDiv, funext, HMul, ProbabilityTheory.IdentDistrib.map_eq, HDiv, SummationFilter.unconditional
10 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IdentDistrib.KLDiv_eq (X' : Ω'' → G) (Y' : Ω''' → G)
    (hX : IdentDistrib X X' μ μ'') (hY : IdentDistrib Y Y' μ' μ''') :
    KL[X ; μ # Y ; μ'] = KL[X' ; μ'' # Y' ; μ'''] := by
…
```
lemma KLDiv_eq_sum line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Fintype, Eq, Real, KLDiv, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.log, HDiv.hDiv
Proof uses: tsum_eq_sum, SummationFilter.unconditional, of_eq_true, Not, Membership.mem, Finset, OfNat.ofNat, Eq.trans, True, forall_congr, False, Or, Neg.neg, implies_congr, congrArg, not_true_eq_false, congrFun', implies_true
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma KLDiv_eq_sum_negMulLog line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Fintype, Eq, Real, KLDiv, Finset.sum, Finset.univ, HMul.hMul, Neg.neg, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.negMulLog, HDiv.hDiv
Proof uses: Eq.mpr, Real.log, id, congrArg, KLDiv_eq_sum, AddCommMonoid, Finset, Eq.rec, Eq.refl, funext, OfNat.ofNat, Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congr, congrFun', zero_div and 48 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma KLDiv_nonneg KL(X ‖ Y) ≥ 0 line 74 source
Source documentation
KL(X ‖ Y) ≥ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, MeasurableSingletonClass, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, ENNReal, Set, MeasureTheory.Measure.map, Singleton.singleton, OfNat.ofNat, LE.le, Real, KLDiv
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Real.log, HDiv.hDiv, id, congrArg, KLDiv_eq_sum, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True and 32 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma KLDiv_nonneg [Finite G] [MeasurableSingletonClass G] [IsZeroOrProbabilityMeasure μ]
    [IsZeroOrProbabilityMeasure μ']
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) : 0 ≤ KL[X ; μ # Y ; μ'] := by
…
```
lemma KLDiv_eq_zero_iff_identDistrib KL(X ‖ Y) = 0 if and only if Y is a copy of X line 91 source
Source documentation
KL(X ‖ Y) = 0 if and only if Y is a copy of X.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, OfNat.ofNat, Iff, KLDiv, ProbabilityTheory.IdentDistrib
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Iff.intro, Membership.mem, Finset, Finset.univ, HMul.hMul, Exists, Real.sum_mul_log_div_eq_iff, of_eq_true, LE.le, Eq.trans, True, forall_congr, implies_congr, implies_true, congrFun', congrArg and 41 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma KLDiv_eq_zero_iff_identDistrib [Finite G] [MeasurableSingletonClass G]
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y)
    (habs : ∀ x, (μ'.map Y).real {x} = 0 → (μ.map X).real {x} = 0) :
    KL[X ; μ # Y ; μ'] = 0 ↔ IdentDistrib X Y μ μ' := by
…
```
lemma KLDiv_of_convex Documented declaration: KLDiv_of_convex line 116 source
Source documentation
If $S$ is a finite set, $w_s$ is non-negative, and ${\bf P}(X=x) = \sum_{s\in S} w_s {\bf P}(X_s=x)$, ${\bf P}(Y=x) = \sum_{s\in S} w_s {\bf P}(Y_s=x)$ for all $x$, then $$D_{KL}(X\Vert Y) \le \sum_{s\in S} w_s D_{KL}(X_s\Vert Y_s).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, Finset, Real, Membership.mem, LE.le, OfNat.ofNat, Eq, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Finset.sum, HMul.hMul, KLDiv
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.univ, Real.log, HDiv.hDiv, id, Eq.rec, Eq.refl, Eq.trans, congrArg, KLDiv_eq_sum, Real.sum_mul_log_div_leq, mul_nonneg, of_eq_true, Or, Iff.mp, mul_eq_zero and 18 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma KLDiv_of_convex [Finite G]
    {ι : Type*} {S : Finset ι} {w : ι → ℝ} (hw : ∀ s ∈ S, 0 ≤ w s)
    (X' : ι → Ω'' → G) (Y' : ι → Ω''' → G)
    (hconvex : ∀ x, (μ.map X).real {x} = ∑ s ∈ S, w s * (μ''.map (X' s)).real {x})
    (hconvex' : ∀ x, (μ'.map Y).real {x} = ∑ s ∈ S, w s * (μ'''.map (Y' s)).real {x})
    (habs : ∀ s ∈ S, ∀ x, (μ'''.map (Y' s)).real {x} = 0 → (μ''.map (X' s)).real {x} = 0) :
    KL[X ; μ # Y ; μ'] ≤ ∑ s ∈ S, w s * KL[X' s ; μ'' # Y' s ; μ'''] := by
…
```
lemma KLDiv_of_comp_inj If $f:G \to H$ is an injection, then $D_{KL}(f(X)\Vert f(Y)) = D_{KL}(X\Vert Y)$ line 149 source
Source documentation
If $f:G \to H$ is an injection, then $D_{KL}(f(X)\Vert f(Y)) = D_{KL}(X\Vert Y)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, DiscreteMeasurableSpace, MeasurableSingletonClass, Function.Injective, Measurable, Eq, Real, KLDiv, Function.comp
Proof uses: id, Eq.mpr, tsum, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.log, HDiv.hDiv, SummationFilter.unconditional, congrArg, Eq.symm, Function.Injective.tsum_eq, Membership.mem, Function.support, Ne, OfNat.ofNat, False.elim, False and 49 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma KLDiv_of_comp_inj {H : Type*} [MeasurableSpace H] [DiscreteMeasurableSpace G]
    [MeasurableSingletonClass H] {f : G → H}
    (hf : Function.Injective f) (hX : Measurable X) (hY : Measurable Y) :
    KL[f ∘ X ; μ # f ∘ Y ; μ'] = KL[X ; μ # Y ; μ'] := by
…
```
lemma KLDiv_add_const line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, DiscreteMeasurableSpace, Measurable, Eq, Real, KLDiv, HAdd.hAdd
Proof uses: KLDiv_of_comp_inj, add_left_injective
16 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.IndepFun.map_add_eq_sum The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent line 197 source
Source documentation
The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent. Probably already available somewhere in some form, but I couldn't locate it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Fintype, AddCommGroup, DiscreteMeasurableSpace, ProbabilityTheory.IndepFun, Measurable, Set, Eq, ENNReal, MeasureTheory.Measure.map, HAdd.hAdd, Finset.sum, Finset.univ, HMul.hMul, Singleton.singleton, Neg.neg
Proof uses: Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, Measurable.add, Prod, DiscreteMeasurableSpace.forall_measurableSet, Set.iUnion, Inter.inter, Set.Subset.antisymm, Membership.mem, Exists, And, Eq.trans, funext, congr, Exists.intro, And.intro, congrFun' and 36 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IndepFun.map_add_eq_sum
    [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G]
    {X Z : Ω → G} (h_indep : IndepFun X Z μ)
    (hX : Measurable X) (hZ : Measurable Z) (S : Set G) :
    μ.map (X + Z) S = ∑ s, μ.map Z {s} * μ.map X ({-s} + S) := by
…
```
lemma ProbabilityTheory.IndepFun.map_add_singleton_eq_sum The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent line 233 source
Source documentation
The distribution of X + Z is the convolution of the distributions of Z and X when these random variables are independent. Probably already available somewhere in some form, but I couldn't locate it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Fintype, AddCommGroup, DiscreteMeasurableSpace, ProbabilityTheory.IndepFun, Measurable, Eq, ENNReal, Set, MeasureTheory.Measure.map, HAdd.hAdd, Singleton.singleton, Finset.sum, Finset.univ, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, Neg.neg, id, congrArg, ProbabilityTheory.IndepFun.map_add_eq_sum, AddCommMonoid, Finset, Eq.rec, Eq.refl, funext, HMul, eq_of_heq, HEq, DFunLike, HEq.refl, heq_of_eq, Eq.trans, congrFun', Set.image, Set.add_singleton and 1 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IndepFun.map_add_singleton_eq_sum
    [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G]
    {X Z : Ω → G} (h_indep : IndepFun X Z μ)
    (hX : Measurable X) (hZ : Measurable Z) (x : G) :
    μ.map (X + Z) {x} = ∑ s, μ.map Z {s} * μ.map X {x - s} := by
…
```
lemma ProbabilityTheory.IndepFun.real_map_add_eq_sum line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Fintype, AddCommGroup, DiscreteMeasurableSpace, ProbabilityTheory.IndepFun, Measurable, Set, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.map, HAdd.hAdd, Finset.sum, Finset.univ, HMul.hMul, Singleton.singleton, Neg.neg
Proof uses: Eq.mpr, ENNReal.toReal, ENNReal, id, congrArg, MeasureTheory.measureReal_def, ProbabilityTheory.IndepFun.map_add_eq_sum, ENNReal.toReal_sum, Membership.mem, Finset, ENNReal.mul_ne_top, MeasureTheory.measure_ne_top, AddCommMonoid, Eq.rec, Eq.refl, funext, Set.preimage, congr, Eq.trans, Set.image and 5 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IndepFun.real_map_add_singleton_eq_sum line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Fintype, AddCommGroup, DiscreteMeasurableSpace, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.IndepFun, Measurable, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.map, HAdd.hAdd, Singleton.singleton, Set, Finset.sum, Finset.univ, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, ENNReal.toReal, ENNReal, id, congrArg, MeasureTheory.measureReal_def, ProbabilityTheory.IndepFun.map_add_singleton_eq_sum, ENNReal.toReal_sum, Membership.mem, Finset, ENNReal.mul_ne_top, MeasureTheory.measure_ne_top, AddCommMonoid, Eq.rec, Eq.refl, funext, ENNReal.toReal_mul
38 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma absolutelyContinuous_add_of_indep line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, AddCommGroup, DiscreteMeasurableSpace, ProbabilityTheory.IndepFun, Prod, prod, Measurable, Eq, ENNReal, Set, MeasureTheory.Measure.map, Singleton.singleton, OfNat.ofNat, HAdd.hAdd
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, ProbabilityTheory.IndepFun.comp, Prod.fst, id, measurable_fst, measurable_id, Prod.snd, measurable_snd, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, HSub.hSub, congrArg, ProbabilityTheory.IndepFun.map_add_singleton_eq_sum, Membership.mem, Finset and 15 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma KLDiv_add_le_KLDiv_of_indep If $X, Y, Z$ are independent $G$-valued random variables, then $$D_{KL}(X+Z\Vert Y+Z) \leq D_{KL}(X\Vert Y).$$ line 284 source
Source documentation
If $X, Y, Z$ are independent $G$-valued random variables, then $$D_{KL}(X+Z\Vert Y+Z) \leq D_{KL}(X\Vert Y).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, AddCommGroup, DiscreteMeasurableSpace, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.IndepFun, Prod, prod, Measurable, Eq, ENNReal, Set, MeasureTheory.Measure.map, Singleton.singleton, OfNat.ofNat, LE.le, Real, KLDiv, HAdd.hAdd
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, tsum, HMul.hMul, MeasureTheory.Measure.real, Real.log, HDiv.hDiv, SummationFilter.unconditional, Finset.sum, Finset.univ and 64 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma KLDiv_add_le_KLDiv_of_indep [Finite G] [AddCommGroup G] [DiscreteMeasurableSpace G]
    {X Y Z : Ω → G} [IsZeroOrProbabilityMeasure μ]
    (h_indep : IndepFun (⟨X, Y⟩) Z μ)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (habs : ∀ x, μ.map Y {x} = 0 → μ.map X {x} = 0) :
    KL[X + Z ; μ # Y + Z ; μ] ≤ KL[X ; μ # Y ; μ] := by
…
```
def condKLDiv If $X,Y,Z$ are random variables, with $X,Z$ defined on the same sample space, we define $$ D_{KL}(X|Z \Vert Y) := \sum_z \mathbf{P}(Z=z) D_{KL}( (X|Z=z) \Vert Y).$$ line 335 source
Source documentation
If $X,Y,Z$ are random variables, with $X,Z$ defined on the same sample space, we define $$ D_{KL}(X|Z \Vert Y) := \sum_z \mathbf{P}(Z=z) D_{KL}( (X|Z=z) \Vert Y).$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, KLDiv, ProbabilityTheory.cond, SummationFilter.unconditional
9 instances, coercions and auxiliary constants left out.
```
noncomputable def condKLDiv {S : Type*} (X : Ω → G) (Y : Ω' → G) (Z : Ω → S)
    (μ : Measure Ω := by volume_tac) (μ' : Measure Ω' := by volume_tac) : ℝ :=
…
```
lemma condKLDiv_eq Documented declaration: condKLDiv_eq line 348 source
Source documentation
If $X, Y$ are $G$-valued random variables, and $Z$ is another random variable defined on the same sample space as $X$, then $$D_{KL}((X|Z)\Vert Y) = D_{KL}(X\Vert Y) + \bbH[X] - \bbH[X|Z].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, MeasurableSingletonClass, MeasureTheory.IsZeroOrProbabilityMeasure, MeasureTheory.IsFiniteMeasure, Measurable, Eq, ENNReal, Set, MeasureTheory.Measure.map, Singleton.singleton, OfNat.ofNat, Real, condKLDiv, HSub.hSub, HAdd.hAdd, KLDiv, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, ProbabilityTheory.cond, SummationFilter.unconditional, Finset.sum, Finset.univ and 82 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma condKLDiv_eq {S : Type*} [MeasurableSpace S] [Finite S] [MeasurableSingletonClass S]
    [Finite G] [IsZeroOrProbabilityMeasure μ] [IsFiniteMeasure μ']
    {X : Ω → G} {Y : Ω' → G} {Z : Ω → S}
    (hX : Measurable X) (hZ : Measurable Z)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) :
    KL[ X | Z ; μ # Y ; μ'] = KL[X ; μ # Y ; μ'] + H[X ; μ] - H[ X | Z ; μ] := by
…
```
lemma condKLDiv_nonneg KL(X|Z ‖ Y) ≥ 0 line 398 source
Source documentation
KL(X|Z ‖ Y) ≥ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Finite, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Eq, ENNReal, Set, MeasureTheory.Measure.map, Singleton.singleton, OfNat.ofNat, LE.le, Real, condKLDiv
Proof uses: Eq.mpr, tsum, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, KLDiv, ProbabilityTheory.cond, SummationFilter.unconditional, id, congrArg, condKLDiv.eq_1, tsum_nonneg, mul_nonneg, of_eq_true, KLDiv_nonneg, MeasureTheory.Measure.map_apply, MeasurableSingletonClass.measurableSet_singleton, ProbabilityTheory.cond_absolutelyContinuous, Eq.mp
33 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma condKLDiv_nonneg {S : Type*} [MeasurableSingletonClass G] [Finite G]
    {X : Ω → G} {Y : Ω' → G} {Z : Ω → S}
    [IsZeroOrProbabilityMeasure μ'] (hX : Measurable X)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) :
    0 ≤ KL[X | Z; μ # Y ; μ'] := by
…
```
lemma tendsto_KLDiv_id_right line 411 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, TopologicalSpace, DiscreteTopology, Finite, DiscreteMeasurableSpace, MeasureTheory.IsFiniteMeasure, Filter, MeasureTheory.ProbabilityMeasure, Filter.Tendsto, nhds, Eq, NNReal, Set, Singleton.singleton, OfNat.ofNat, ENNReal, MeasureTheory.Measure.map, Real, KLDiv and 1 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Real.log, HDiv.hDiv, congr, congrFun', congrArg, funext, KLDiv_eq_sum, tendsto_finsetSum, Membership.mem, Finset, Ne and 33 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma tendsto_KLDiv_id_left line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, DiscreteTopology, Finite, DiscreteMeasurableSpace, MeasureTheory.Measure, Filter, MeasureTheory.ProbabilityMeasure, Filter.Tendsto, nhds, Real, KLDiv, id
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, Neg.neg, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.negMulLog, HDiv.hDiv, congr, congrFun', congrArg, funext and 27 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.