Source indexedlemma · leanprover/lean4:v4.33.0-rc1

KLDiv_nonneg

PFR.Kullback · PFR/Kullback.lean:74 to 89

Source documentation

KL(X ‖ Y) ≥ 0.

Exact Lean statement

lemma KLDiv_nonneg [Finite G] [MeasurableSingletonClass G] [IsZeroOrProbabilityMeasure μ]
    [IsZeroOrProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y)
    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) : 0 ≤ KL[X ; μ # Y ; μ']

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma KLDiv_nonneg [Finite G] [MeasurableSingletonClass G] [IsZeroOrProbabilityMeasure μ]    [IsZeroOrProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y)    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) : 0 ≤ KL[X ; μ # Y ; μ'] := by  cases nonempty_fintype G  rw [KLDiv_eq_sum]  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  rcases eq_zero_or_isProbabilityMeasure μ' with rfl | hμ'  · simp  apply le_trans ?_ (sum_mul_log_div_leq (by simp) (by simp) ?_)  · have : IsProbabilityMeasure (μ'.map Y) := Measure.isProbabilityMeasure_map hY.aemeasurable    have : IsProbabilityMeasure (μ.map X) := Measure.isProbabilityMeasure_map hX.aemeasurable    simp  · intro i _ hi    simp only [Measure.real, ENNReal.toReal_eq_zero_iff, measure_ne_top, or_false] at hi    simp [Measure.real, habs i hi]