Mathlib.Information­Theory

Information-theoretic helpers staged for Mathlib: KL divergence under binding/composition, common-statistic Bernoulli kernels, and the product-KL ingredients of Le Cam two-point arguments.

Kullback­Leibler 6 core · 3 supporting · 1 submodule Density-tilt expansions for Kullback–Leibler divergence.
Entropy 3 core · 3 supporting This module builds the Shannon entropy of a (probability) mass function on a finite alphabet α together with its maximum-entropy / Gibbs bound H(p) ≤ log (card α), which Mathlib does not provide for general Fintype α (it ★ entropy_le_log_card★ entropy_const_eq_log_card

Finite-alphabet Shannon entropy and the maximum-entropy bound

This module builds the Shannon entropy of a (probability) mass function on a finite alphabet α together with its maximum-entropy / Gibbs bound H(p) ≤ log (card α), which Mathlib does not provide for general Fintype α (it only has the binary case Real.binEntropy_le_log_two).

The entropy is defined in nats as entropy p = ∑ i, Real.negMulLog (p i) for any real-valued p : α → ℝ; the probability-mass hypotheses (0 ≤ p i, ∑ i, p i = 1) enter only the lemmas, never the definition.

Main results: * entropy_nonneg — entropy of a sub-probability vector is nonnegative. * entropy_le_log_card — the maximum-entropy (Gibbs) bound H(p) ≤ log (card α), proved elementarily from Real.log_le_sub_one_of_pos (no Jensen/Gibbs black box). * entropy_const_eq_log_card — the uniform pmf attains the bound, witnessing that the bound is sharp (and the statement non-vacuous).

This is the finite-entropy core meant to be reused by information-theoretic arguments (Fano's inequality, max-entropy priors, mutual-information / capacity bounds). It is stated generically over an arbitrary Fintype α.

Reference: Cover & Thomas, Elements of Information Theory (2e), §2.1 and Thm 2.6.4.

def entropy reviewed
Causalean.Mathlib.InformationTheory

For a finite alphabet and a real-valued mass function on it, the Shannon entropy in nats is ∑i−p(i)log⁡p(i)\sum_i -p(i)\log p(i), with the standard zero-continuous convention for the summands.

Definition (Lean source)
parameters
α :
Type u_1
shared
p :
α → ℝ
def
entropy p :
ℝ
given by
∑ i, negMulLog (p i)
Causalean.Mathlib.InformationTheory.entropy · Causalean/Mathlib/InformationTheory/Entropy.lean:45
theorem entropy_le_log_card reviewed
Causalean.Mathlib.InformationTheory

Maximum-entropy (Gibbs) bound. For a nonnegative function p on a finite alphabet α that sums to one (∑ i, p i = 1, i.e. p is a probability mass function) with n = Fintype.card α, the Shannon entropy of p is at most log n: entropy p ≤ Real.log (Fintype.card α).

Formal statement
hypotheses
α :
Type u_1
α → ℝ
shared
h0 :
∀ i, 0 ≤ p i
hsum :
∑ i, p i = 1
conclusion
entropy p ≤ log (card α)
Proof (Lean source)
theorem entropy_le_log_card {p : α → ℝ} (h0 : ∀ i, 0 ≤ p i) (hsum : ∑ i, p i = 1) : entropy p ≤ log (Fintype.card α) := by letI : Nonempty α := by by_contra h letI : IsEmpty α := not_nonempty_iff.mp h simp at hsum let n := Fintype.card α have hn : 0 < n := Fintype.card_pos have hterm : (∑ i, (negMulLog (p i) - p i * log (n : ℝ))) ≤ ∑ i, ((n : ℝ)⁻¹ - p i) := by exact Finset.sum_le_sum (fun i _ => negMulLog_sub_mul_log_le (by exact_mod_cast hn) (h0 i)) have hleft : (∑ i, (negMulLog (p i) - p i * log (n : ℝ))) = entropy p - log (n : ℝ) := by calc (∑ i, (negMulLog (p i) - p i * log (n : ℝ))) = (∑ i, negMulLog (p i)) - (∑ i, p i * log (n : ℝ)) := by rw [Finset.sum_sub_distrib] _ = entropy p - (∑ i, p i) * log (n : ℝ) := by rw [entropy] rw [Finset.sum_mul] _ = entropy p - log (n : ℝ) := by rw [hsum] ring have hright : (∑ i, ((n : ℝ)⁻¹ - p i)) = 0 := by calc (∑ i, ((n : ℝ)⁻¹ - p i)) = (∑ i : α, (n : ℝ)⁻¹) - ∑ i, p i := by rw [Finset.sum_sub_distrib] _ = (n : ℝ) * (n : ℝ)⁻¹ - 1 := by rw [Finset.sum_const, Finset.card_univ, hsum] simp [n] _ = 0 := by have hnR : (n : ℝ) ≠ 0 := by positivity field_simp [hnR] ring have : entropy p - log (n : ℝ) ≤ 0 := by linarith have : entropy p ≤ log (n : ℝ) := by linarith simpa [n] using this
Causalean.Mathlib.InformationTheory.entropy_le_log_card · Causalean/Mathlib/InformationTheory/Entropy.lean:93 · uses entropy
theorem entropy_const_eq_log_card reviewed
Causalean.Mathlib.InformationTheory

Sharpness of the maximum-entropy bound. The uniform probability mass function on a nonempty finite alphabet — assigning every outcome probability equal to the reciprocal of the alphabet's cardinality — attains entropy exactly equal to the natural logarithm of that cardinality.

Formal statement
hypotheses
α :
Type u_1
Nonempty α
shared
conclusion
entropy (fun _ : α => (Fintype.card α : ℝ)⁻¹) = log (Fintype.card α)
Proof (Lean source)
theorem entropy_const_eq_log_card [Nonempty α] : entropy (fun _ : α => (Fintype.card α : ℝ)⁻¹) = log (Fintype.card α) := by let n := Fintype.card α have hn : 0 < n := Fintype.card_pos have hnR : (n : ℝ) ≠ 0 := by positivity have hneg : negMulLog ((n : ℝ)⁻¹) = (n : ℝ)⁻¹ * log (n : ℝ) := by simp [Real.negMulLog_def, Real.log_inv] have hmain : entropy (fun _ : α => (n : ℝ)⁻¹) = log (n : ℝ) := by calc entropy (fun _ : α => (n : ℝ)⁻¹) = (n : ℝ) * negMulLog ((n : ℝ)⁻¹) := by simp [entropy, Finset.sum_const, Finset.card_univ, n] _ = (n : ℝ) * ((n : ℝ)⁻¹ * log (n : ℝ)) := by rw [hneg] _ = log (n : ℝ) := by field_simp [hnR] simpa [n] using hmain
Causalean.Mathlib.InformationTheory.entropy_const_eq_log_card · Causalean/Mathlib/InformationTheory/Entropy.lean:146 · uses entropy
3 supporting declarations (lemmas, instances)
  • entropy_def lemma — The finite-alphabet entropy definition unfolds to the sum of Real.negMulLog over the alphabet.
    hypotheses
    α :
    Type u_1
    shared
    p :
    α → ℝ
    conclusion
    entropy p = ∑ i, negMulLog (p i)
    Proof (Lean source)
    @[simp] lemma entropy_def (p : α → ℝ) : entropy p = ∑ i, negMulLog (p i) := rfl
    Causalean.Mathlib.InformationTheory.entropy_def · Causalean/Mathlib/InformationTheory/Entropy.lean:51
  • entropy_nonneg lemma — Entropy is nonnegative for any sub-probability vector: if 0 ≤ p i ≤ 1 for every i, then 0 ≤ entropy p. Each summand Real.negMulLog (p i) is nonnegative on [0,1] (Real.negMulLog_nonneg), so the finite sum is nonnegative.
    hypotheses
    α :
    Type u_1
    α → ℝ
    shared
    h0 :
    ∀ i, 0 ≤ p i
    h1 :
    ∀ i, p i ≤ 1
    conclusion
    0 ≤ entropy p
    Proof (Lean source)
    lemma entropy_nonneg {p : α → ℝ} (h0 : ∀ i, 0 ≤ p i) (h1 : ∀ i, p i ≤ 1) : 0 ≤ entropy p := by rw [entropy_def] refine Finset.sum_nonneg ?_ intro i _ exact Real.negMulLog_nonneg (h0 i) (h1 i)
    Causalean.Mathlib.InformationTheory.entropy_nonneg · Causalean/Mathlib/InformationTheory/Entropy.lean:55
  • negMulLog_sub_mul_log_le lemma — Per-coordinate Gibbs lever. At any positive real scale c, the entropy summand minus x · log c is bounded by 1/c - x: Real.negMulLog x - x * Real.log c ≤ c⁻¹ - x.
    hypotheses
    c :
    ℝ
    hc :
    0 < c
    x :
    ℝ
    hx :
    0 ≤ x
    conclusion
    negMulLog x - x * log c ≤ c⁻¹ - x
    Proof (Lean source)
    lemma negMulLog_sub_mul_log_le {c : ℝ} (hc : 0 < c) {x : ℝ} (hx : 0 ≤ x) : negMulLog x - x * log c ≤ c⁻¹ - x := by rcases eq_or_lt_of_le hx with rfl | hxpos · simpa [negMulLog] using le_of_lt hc · have hcR : (0 : ℝ) < c := hc have hlog := Real.log_le_sub_one_of_pos (show (0 : ℝ) < (c * x)⁻¹ by positivity) have hlogeq : log ((c * x)⁻¹) = -(log c + log x) := by rw [Real.log_inv] rw [Real.log_mul hcR.ne' hxpos.ne'] have hid : negMulLog x - x * log c = x * log ((c * x)⁻¹) := by rw [Real.negMulLog_def] rw [hlogeq] ring have hmul := mul_le_mul_of_nonneg_left hlog (le_of_lt hxpos) calc negMulLog x - x * log c = x * log ((c * x)⁻¹) := hid _ ≤ x * ((c * x)⁻¹ - 1) := hmul _ = c⁻¹ - x := by field_simp [hcR.ne', hxpos.ne']
    Causalean.Mathlib.InformationTheory.negMulLog_sub_mul_log_le · Causalean/Mathlib/InformationTheory/Entropy.lean:65
Conditional­Entropy 4 core · 10 supporting This module sets up the finite-alphabet objects feeding Fano's inequality and proves the single information-theoretic inequality the Fano proof rests on. ★ entropy_le_crossEntropy

Conditional Shannon entropy and the Gibbs (cross-entropy) inequality

This module sets up the finite-alphabet objects feeding Fano's inequality and proves the single information-theoretic inequality the Fano proof rests on.

For a joint mass function p : α × β → ℝ we define the β-marginal yMarginal p y = ∑ x, p (x, y) and the conditional entropy via the chain rule condEntropy p = entropy p − entropy (yMarginal p) (i.e. H(X ∣ Y) = H(X,Y) − H(Y)), reusing the entropy core Causalean.Mathlib.InformationTheory.entropy.

The crux fact is the Gibbs / cross-entropy inequality entropy_le_crossEntropy: for a pmf p and any sub-pmf g that dominates the support of p, entropy p ≤ −∑ i, p i · log (g i). Specialising g to a cleverly chosen reference distribution turns this single inequality into Fano's bound (see Fano.lean); this mirrors the entropy core's entropy_le_log_card (which is the case g ≡ 1 / card).

Main definitions: * yMarginal p — the β-marginal of a joint mass function on α × β. * condEntropy p — conditional entropy H(X ∣ Y) = entropy p − entropy (yMarginal p). * errorProb p decode — the error probability ∑_{x ≠ decode y} p (x, y) of a deterministic decoder decode : β → α.

Main results: * negMulLog_add_mul_log_le — the per-coordinate Gibbs lever. * entropy_le_crossEntropy — the Gibbs / cross-entropy inequality. * yMarginal_sum, errorProb_nonneg, errorProb_le_one — supporting pmf facts.

Reference: Cover & Thomas, Elements of Information Theory (2e), §2.10, Thm 2.10.1.

def yMarginal reviewed
Causalean.Mathlib.InformationTheory

For a finite outcome alphabet and an arbitrary conditioning-value space, a joint real-valued mass function on their product, and a chosen conditioning value, the marginal mass at that conditioning value is the finite sum of the joint masses over all outcome values.

Definition (Lean source)
parameters
α :
Type u_1
shared
β :
Type u_2
shared
p :
α × β → ℝ
y :
β
def
yMarginal p y :
ℝ
given by
∑ x, p (x, y)
Causalean.Mathlib.InformationTheory.yMarginal · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:51
def condEntropy reviewed
Causalean.Mathlib.InformationTheory

For finite outcome and conditioning alphabets and a joint real-valued mass function on their product, the conditional Shannon entropy is the Shannon entropy of the joint mass function minus the Shannon entropy of its conditioning-variable marginal.

Definition (Lean source)
parameters
α :
Type u_1
shared
β :
Type u_2
shared
p :
α × β → ℝ
def
condEntropy p :
ℝ
given by
entropy p - entropy (yMarginal p)
Causalean.Mathlib.InformationTheory.condEntropy · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:54
def errorProb reviewed
Causalean.Mathlib.InformationTheory

For finite outcome and observation alphabets, with equality decidable for outcomes, a joint real-valued mass function on their product, and a deterministic decoder from observations to outcomes, the decoder's error mass is the sum of the joint masses of all outcome--observation pairs for which the decoder's output differs from the outcome.

Definition (Lean source)
parameters
α :
Type u_1
shared
β :
Type u_2
shared
p :
α × β → ℝ
decode :
β → α
def
errorProb p decode :
ℝ
given by
by classical exact ∑ xy : α × β, (if xy.1 = decode xy.2 then 0 else p xy)
Causalean.Mathlib.InformationTheory.errorProb · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:59
theorem entropy_le_crossEntropy reviewed
Causalean.Mathlib.InformationTheory

Gibbs / cross-entropy inequality. For a nonnegative mass function p and a nonnegative reference mass function g on a finite type γ, if the total mass of g is at most the total mass of p (∑ g ≤ ∑ p) and g dominates the support of p (p i ≠ 0 → 0 < g i), then the Shannon entropy of p is bounded by the cross-entropy of p relative to g: entropy p ≤ −∑ i, p i * Real.log (g i).

Formal statement
hypotheses
γ :
Type*
Fintype γ
γ → ℝ
hp0 :
∀ i, 0 ≤ p i
hg0 :
∀ i, 0 ≤ g i
hgsum :
∑ i, g i ≤ ∑ i, p i
hac :
∀ i
if
p i ≠ 0
then
0 < g i
conclusion
entropy p ≤ - ∑ i, p i * log (g i)
Proof (Lean source)
theorem entropy_le_crossEntropy {γ : Type*} [Fintype γ] {p g : γ → ℝ} (hp0 : ∀ i, 0 ≤ p i) (hg0 : ∀ i, 0 ≤ g i) (hgsum : ∑ i, g i ≤ ∑ i, p i) (hac : ∀ i, p i ≠ 0 → 0 < g i) : entropy p ≤ - ∑ i, p i * log (g i) := by have hterm : (∑ i, (negMulLog (p i) + p i * log (g i))) ≤ ∑ i, (g i - p i) := by exact Finset.sum_le_sum (fun i _ => negMulLog_add_mul_log_le (hp0 i) (hg0 i) (hac i)) have hleft : (∑ i, (negMulLog (p i) + p i * log (g i))) = entropy p + ∑ i, p i * log (g i) := by calc (∑ i, (negMulLog (p i) + p i * log (g i))) = (∑ i, negMulLog (p i)) + ∑ i, p i * log (g i) := by rw [Finset.sum_add_distrib] _ = entropy p + ∑ i, p i * log (g i) := by rw [entropy_def] have hright : (∑ i, (g i - p i)) ≤ 0 := by calc (∑ i, (g i - p i)) = (∑ i, g i) - ∑ i, p i := by rw [Finset.sum_sub_distrib] _ ≤ 0 := by exact sub_nonpos.mpr hgsum have : entropy p + ∑ i, p i * log (g i) ≤ 0 := by linarith linarith
Causalean.Mathlib.InformationTheory.entropy_le_crossEntropy · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:109 · uses entropy
10 supporting declarations (lemmas, instances)
  • yMarginal_def lemma — The β-marginal is the finite sum of joint masses over the α coordinate at the chosen value of β.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    shared
    p :
    α × β → ℝ
    y :
    β
    conclusion
    yMarginal p y = ∑ x, p (x, y)
    Proof (Lean source)
    @[simp] lemma yMarginal_def (p : α × β → ℝ) (y : β) : yMarginal p y = ∑ x, p (x, y) := rfl
    Causalean.Mathlib.InformationTheory.yMarginal_def · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:67
  • condEntropy_def lemma — Conditional entropy unfolds to total joint entropy minus the entropy of the conditioning marginal.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    shared
    p :
    α × β → ℝ
    conclusion
    condEntropy p = entropy p - entropy (yMarginal p)
    Proof (Lean source)
    @[simp] lemma condEntropy_def (p : α × β → ℝ) : condEntropy p = entropy p - entropy (yMarginal p) := rfl
    Causalean.Mathlib.InformationTheory.condEntropy_def · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:73
  • errorProb_def lemma — The decoder error probability unfolds to the sum of the joint masses on incorrect decoding cells.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    shared
    p :
    α × β → ℝ
    decode :
    β → α
    conclusion
    errorProb p decode = ∑ xy : α × β, (if xy.1 = decode xy.2 then 0 else p xy)
    Proof (Lean source)
    @[simp] lemma errorProb_def (p : α × β → ℝ) (decode : β → α) : errorProb p decode = ∑ xy : α × β, (if xy.1 = decode xy.2 then 0 else p xy) := rfl
    Causalean.Mathlib.InformationTheory.errorProb_def · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:78
  • negMulLog_add_mul_log_le lemma — Per-coordinate Gibbs lever. For 0 ≤ x and 0 ≤ g, with g positive whenever x is nonzero (absolute continuity), the cross-entropy summand is controlled: Real.negMulLog x + x * Real.log g ≤ g - x.
    hypotheses
    x g :
    ℝ
    hx :
    0 ≤ x
    hg :
    0 ≤ g
    hac :
    x ≠ 0 → 0 < g
    conclusion
    negMulLog x + x * log g ≤ g - x
    Proof (Lean source)
    lemma negMulLog_add_mul_log_le {x g : ℝ} (hx : 0 ≤ x) (hg : 0 ≤ g) (hac : x ≠ 0 → 0 < g) : negMulLog x + x * log g ≤ g - x := by rcases eq_or_lt_of_le hx with rfl | hxpos · simpa [negMulLog] using hg · have hgpos : 0 < g := hac hxpos.ne' have hlog := Real.log_le_sub_one_of_pos (show (0 : ℝ) < g / x by positivity) have hid : negMulLog x + x * log g = x * log (g / x) := by rw [Real.negMulLog_def] rw [Real.log_div hgpos.ne' hxpos.ne'] ring have hmul := mul_le_mul_of_nonneg_left hlog (le_of_lt hxpos) calc negMulLog x + x * log g = x * log (g / x) := hid _ ≤ x * (g / x - 1) := hmul _ = g - x := by field_simp [hxpos.ne']
    Causalean.Mathlib.InformationTheory.negMulLog_add_mul_log_le · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:83
  • yMarginal_sum lemma — The β-marginal of a pmf is itself a pmf summing to one: if ∑ xy, p xy = 1 then ∑ y, yMarginal p y = 1.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hsum :
    ∑ xy : α × β, p xy = 1
    conclusion
    ∑ y, yMarginal p y = 1
    Proof (Lean source)
    lemma yMarginal_sum {p : α × β → ℝ} (hsum : ∑ xy : α × β, p xy = 1) : ∑ y, yMarginal p y = 1 := by simp only [yMarginal_def] rw [← Fintype.sum_prod_type_right] exact hsum
    Causalean.Mathlib.InformationTheory.yMarginal_sum · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:149
  • yMarginal_nonneg lemma — The β-marginal of a nonnegative mass function is nonnegative.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    y :
    β
    conclusion
    0 ≤ yMarginal p y
    Proof (Lean source)
    lemma yMarginal_nonneg {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (y : β) : 0 ≤ yMarginal p y := by rw [yMarginal_def] exact Finset.sum_nonneg (fun x _ => hp0 (x, y))
    Causalean.Mathlib.InformationTheory.yMarginal_nonneg · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:158
  • le_yMarginal lemma — A joint mass is dominated by its β-marginal: p (x, y) ≤ yMarginal p y for nonnegative p.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    x :
    α
    y :
    β
    conclusion
    p (x, y) ≤ yMarginal p y
    Proof (Lean source)
    lemma le_yMarginal {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (x : α) (y : β) : p (x, y) ≤ yMarginal p y := by rw [yMarginal_def] exact Finset.single_le_sum (fun x' _ => hp0 (x', y)) (Finset.mem_univ x)
    Causalean.Mathlib.InformationTheory.le_yMarginal · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:165
  • errorProb_nonneg lemma — The error probability is nonnegative.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    decode :
    β → α
    conclusion
    0 ≤ errorProb p decode
    Proof (Lean source)
    lemma errorProb_nonneg {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (decode : β → α) : 0 ≤ errorProb p decode := by rw [errorProb_def] refine Finset.sum_nonneg ?_ intro xy _ split_ifs · exact le_refl 0 · exact hp0 xy
    Causalean.Mathlib.InformationTheory.errorProb_nonneg · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:172
  • errorProb_le_one lemma — The error probability is at most one (it is a sub-sum of the total mass = 1).
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    hsum :
    ∑ xy : α × β, p xy = 1
    decode :
    β → α
    conclusion
    errorProb p decode ≤ 1
    Proof (Lean source)
    lemma errorProb_le_one {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (hsum : ∑ xy : α × β, p xy = 1) (decode : β → α) : errorProb p decode ≤ 1 := by rw [errorProb_def, ← hsum] refine Finset.sum_le_sum ?_ intro xy _ split_ifs · exact hp0 xy · exact le_refl (p xy)
    Causalean.Mathlib.InformationTheory.errorProb_le_one · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:182
  • correctMass_eq lemma — The correct-decision mass equals 1 − errorProb: splitting the total mass = 1 into the correct cells (x = decode y) and the error cells gives ∑_{x = decode y} p (x, y) = 1 − errorProb p decode.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hsum :
    ∑ xy : α × β, p xy = 1
    decode :
    β → α
    conclusion
    (∑ xy : α × β, (if xy.1 = decode xy.2 then p xy else 0)) = 1 - errorProb p decode
    Proof (Lean source)
    lemma correctMass_eq {p : α × β → ℝ} (hsum : ∑ xy : α × β, p xy = 1) (decode : β → α) : (∑ xy : α × β, (if xy.1 = decode xy.2 then p xy else 0)) = 1 - errorProb p decode := by have hterm : (∑ xy : α × β, (if xy.1 = decode xy.2 then p xy else 0)) = ∑ xy : α × β, (p xy - (if xy.1 = decode xy.2 then 0 else p xy)) := by refine Finset.sum_congr rfl ?_ intro xy _ split_ifs <;> ring rw [hterm, Finset.sum_sub_distrib, hsum, errorProb_def]
    Causalean.Mathlib.InformationTheory.correctMass_eq · Causalean/Mathlib/InformationTheory/ConditionalEntropy.lean:193
Common­Statistic­Bernoulli 5 core · 14 supporting This module constructs conditional Bernoulli success parameters by Radon–Nikodym differentiation, identifies the associated composition-product law, and bounds its KL divergence under localized parameter changes. ★ statisticBernoulliOutcome_klDiv_le_of_localized_success_bound

Bernoulli disintegration over a common measurable statistic

This module constructs conditional Bernoulli success parameters by Radon–Nikodym differentiation, identifies the associated composition-product law, and bounds its KL divergence under localized parameter changes.

def commonStatisticBernoulliKernel reviewed
Causalean.Mathlib.InformationTheory

For a measurable input space, a real-valued function of the input, and the hypothesis that this function is measurable, the common-statistic Bernoulli kernel assigns to every input the two-point Bernoulli law on the real line with success weight given by that function at the input. It is a probability measure at inputs where that value lies between zero and one (see commonStatisticBernoulliKernel_isMarkovKernel); elsewhere the weights are clipped to be nonnegative and need not sum to one.

Definition (Lean source)
parameters
S :
Type*
MeasurableSpace S
p :
S → ℝ
hp :
Measurable p
def
commonStatisticBernoulliKernel p hp :
Kernel S ℝ
given by
clause 1
toFun r := bernoulliLaw (p r)
clause 2
measurable' := by unfold bernoulliLaw fun_prop
Causalean.Mathlib.InformationTheory.commonStatisticBernoulliKernel · Causalean/Mathlib/InformationTheory/CommonStatisticBernoulli.lean:41
def statisticSuccessMeasure reviewed
Causalean.Mathlib.InformationTheory

For a measurable sample space, a measure on that space, a real-valued success-weight function, and a real-valued statistic, the success-weighted statistic law is the pushforward along the statistic of the base measure weighted by max⁡{p(x),0}\max\{p(x),0\}. No measurability of the statistic is assumed: if it is not almost-everywhere measurable the pushforward is the zero measure by convention, so this is the statistic law only for a measurable statistic.

Definition (Lean source)
parameters
A :
Type*
MeasurableSpace A
nu :
Measure A
p :
A → ℝ
stat :
A → ℝ
def
statisticSuccessMeasure nu p stat :
Measure ℝ
given by
Measure.map stat (nu.withDensity fun x => ofReal (p x))
Causalean.Mathlib.InformationTheory.statisticSuccessMeasure · Causalean/Mathlib/InformationTheory/CommonStatisticBernoulli.lean:159
def statisticSuccessParameter reviewed
Causalean.Mathlib.InformationTheory

For a measurable sample space, a measure on that space, a real-valued success-weight function, and a real-valued statistic, the statistic-level success parameter is the Radon--Nikodym derivative of the success-weighted statistic law with respect to the statistic's pushforward law under the base measure, converted to a real number. Each pushforward is the zero measure when the statistic is not almost-everywhere measurable for its own source measure (the weighted measure for the numerator, the base measure for the denominator), so this is the conditional success parameter only for a measurable statistic.

Definition (Lean source)
parameters
A :
Type*
MeasurableSpace A
nu :
Measure A
p :
A → ℝ
stat :
A → ℝ
def
statisticSuccessParameter nu p stat :
ℝ → ℝ
given by
fun r => ((statisticSuccessMeasure nu p stat).rnDeriv (Measure.map stat nu) r).toReal
Causalean.Mathlib.InformationTheory.statisticSuccessParameter · Causalean/Mathlib/InformationTheory/CommonStatisticBernoulli.lean:164
def clippedStatisticSuccessParameter reviewed
Causalean.Mathlib.InformationTheory

For a measurable sample space, a measure on that space, a real-valued success-weight function, and a real-valued statistic, the clipped statistic-level success parameter is the statistic-level success parameter truncated below at 1/41/4 and above at 3/43/4.

Definition (Lean source)
parameters
A :
Type*
MeasurableSpace A
nu :
Measure A
p :
A → ℝ
stat :
A → ℝ
def
clippedStatisticSuccessParameter nu p stat :
ℝ → ℝ
given by
fun r => max (1 / 4 : ℝ) (min (3 / 4 : ℝ) (statisticSuccessParameter nu p stat r))
Causalean.Mathlib.InformationTheory.clippedStatisticSuccessParameter · Causalean/Mathlib/InformationTheory/CommonStatisticBernoulli.lean:311
lemma statisticBernoulliOutcome_klDiv_le_of_localized_success_bound reviewed
Causalean.Mathlib.InformationTheory

For a measurable space A, two finite measures nu and nu' on it, and success-probability functions p, p' on A, suppose p, p', and a statistic stat are all measurable, p takes values in [1/4, 3/4] and p' likewise takes values in [1/4, 3/4], and stat pushes nu and nu' forward to the same marginal law. Given a nonnegative discrepancy bound D and a measurable exceptional set E such that for every measurable set B of statistic values, the setwise success-mass discrepancy |∫_{stat∈B} p dnu − ∫_{stat∈B} p' dnu'| is at most D times the stat-pushforward mass of nu on B ∩ E, then the Kullback–Leibler divergence between the compressed Bernoulli-outcome laws obtained by pairing the outcome with stat under nu and under nu' is at most 4·D² times the stat-pushforward mass of E under nu.

Formal statement
hypotheses
A :
Type*
MeasurableSpace A
nu nu' :
Measure A
IsFiniteMeasure nu
IsFiniteMeasure nu'
p p' :
A → ℝ
stat :
A → ℝ
hp :
Measurable p
hp' :
Measurable p'
hstat :
Measurable stat
hp0 :
∀ x, 1 / 4 ≤ p x
hp1 :
∀ x, p x ≤ 3 / 4
hp0' :
∀ x, 1 / 4 ≤ p' x
hp1' :
∀ x, p' x ≤ 3 / 4
hmap :
Measure.map stat nu = Measure.map stat nu'
D :
ℝ
hD :
0 ≤ D
E :
Set ℝ
hE :
MeasurableSet E
hdiff :
∀ B : Set ℝ
if
MeasurableSet B
then
|(∫ x in {x | stat x ∈ B}, p x ∂nu) - ∫ x in {x | stat x ∈ B}, p' x ∂nu'|
≤ D * (Measure.map stat nu (B ∩ E)).toReal
conclusion
klDiv (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp))) (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu' (commonStatisticBernoulliKernel p' hp')))
≤ ofReal (4 * D ^ 2) * Measure.map stat nu E
Proof (Lean source)
lemma statisticBernoulliOutcome_klDiv_le_of_localized_success_bound {A : Type*} [MeasurableSpace A] (nu nu' : Measure A) [IsFiniteMeasure nu] [IsFiniteMeasure nu'] (p p' : A → ℝ) (stat : A → ℝ) (hp : Measurable p) (hp' : Measurable p') (hstat : Measurable stat) (hp0 : ∀ x, 1 / 4 ≤ p x) (hp1 : ∀ x, p x ≤ 3 / 4) (hp0' : ∀ x, 1 / 4 ≤ p' x) (hp1' : ∀ x, p' x ≤ 3 / 4) (hmap : Measure.map stat nu = Measure.map stat nu') {D : ℝ} (hD : 0 ≤ D) {E : Set ℝ} (hE : MeasurableSet E) (hdiff : ∀ B : Set ℝ, MeasurableSet B → |(∫ x in {x | stat x ∈ B}, p x ∂nu) - ∫ x in {x | stat x ∈ B}, p' x ∂nu'| ≤ D * (Measure.map stat nu (B ∩ E)).toReal) : klDiv (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp))) (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu' (commonStatisticBernoulliKernel p' hp'))) ≤ ofReal (4 * D ^ 2) * Measure.map stat nu E := by rw [statisticBernoulliOutcomeLaw_eq_map_swap_compProd nu p stat hp hstat hp0 hp1, statisticBernoulliOutcomeLaw_eq_map_swap_compProd nu' p' stat hp' hstat hp0' hp1'] rw [← hmap] apply commonStatisticBernoulliOutcome_klDiv_le_of_localized_parameter · exact fun r => (clippedStatisticSuccessParameter_mem_Icc nu p stat r).1 · exact fun r => (clippedStatisticSuccessParameter_mem_Icc nu p stat r).2 · exact fun r => (clippedStatisticSuccessParameter_mem_Icc nu' p' stat r).1 · exact fun r => (clippedStatisticSuccessParameter_mem_Icc nu' p' stat r).2 · exact hD · exact hE · exact clippedStatisticSuccessParameter_abs_sub_le_ae nu nu' p p' stat hp hp' hstat hp0 hp1 hp0' hp1' hmap hE hdiff
Causalean.Mathlib.InformationTheory.statisticBernoulliOutcome_klDiv_le_of_localized_success_bound · Causalean/Mathlib/InformationTheory/CommonStatisticBernoulli.lean:604 · uses commonStatisticBernoulliKernel
14 supporting declarations (lemmas, instances)
Fano 3 core · 5 supporting This module proves the classical Fano inequality (Cover & Thomas, *Elements of Information Theory* (2e), Thm 2.10.1): for a joint mass function p : α × β → ℝ over finite alphabets, a deterministic decoder decode : β → α, ★ fano_inequality★ fano_error_lower_bound

Fano's inequality

This module proves the classical Fano inequality (Cover & Thomas, Elements of Information Theory (2e), Thm 2.10.1): for a joint mass function p : α × β → ℝ over finite alphabets, a deterministic decoder decode : β → α, and the error probability Pe = errorProb p decode, the conditional entropy obeys

condEntropy p ≤ Real.binEntropy Pe + Pe * Real.log (Fintype.card α − 1).

The proof applies the single Gibbs inequality entropy_le_crossEntropy from ConditionalEntropy.lean to the reference distribution fanoRef, which on each column y spreads mass 1 − Pe on the decoded symbol decode y and the remaining mass Pe uniformly over the card α − 1 incorrect symbols. Computing the resulting cross-entropy yields exactly entropy (yMarginal p) + binEntropy Pe + Pe · log (card α − 1), and subtracting entropy (yMarginal p) gives Fano's bound. The card α − 1 (rather than card α) is the crux of the theorem and comes from the size of the error block.

Main results: * fano_inequality — Fano's inequality in its sharp form. * fano_error_lower_bound — the standard weakened corollary lower-bounding Pe.

Reference: Cover & Thomas, Elements of Information Theory (2e), §2.10, Thm 2.10.1.

def fanoRef reviewed
Causalean.Mathlib.InformationTheory

For finite outcome and observation alphabets, with equality decidable for outcomes, a joint real-valued mass function on their product, a deterministic decoder from observations to outcomes, and an outcome--observation pair, the Fano reference mass at that pair equals the marginal mass of its observation multiplied by 1−Pe1-P_e when its outcome is the decoded outcome, and by Pe/(∣A∣−1)P_e/(|\mathcal A|-1) otherwise, where PeP_e is the decoder's error mass and ∣A∣|\mathcal A| is the number of outcome values.

Definition (Lean source)
parameters
α :
Type u_1
shared
β :
Type u_2
shared
p :
α × β → ℝ
decode :
β → α
xy :
α × β
def
fanoRef p decode xy :
ℝ
given by
yMarginal p xy.2 * (if xy.1 = decode xy.2 then 1 - errorProb p decode else errorProb p decode / ((Fintype.card α : ℝ) - 1))
Causalean.Mathlib.InformationTheory.fanoRef · Causalean/Mathlib/InformationTheory/Fano.lean:45
theorem fano_inequality reviewed
Causalean.Mathlib.InformationTheory

Fano's inequality (Cover & Thomas, Thm 2.10.1). For a nonnegative function p on α × β that sums to one, i.e. a joint probability mass function, with at least two symbols in the alphabet α (2 ≤ Fintype.card α), and a decoder decode : β → α, the conditional entropy of p is bounded by the binary entropy of the error probability Pe = errorProb p decode plus Pe times the log of one less than the alphabet size: condEntropy p ≤ Real.binEntropy Pe + Pe * Real.log (Fintype.card α − 1).

Formal statement
hypotheses
α :
Type u_1
shared
β :
Type u_2
α × β → ℝ
shared
hp0 :
∀ xy, 0 ≤ p xy
hsum :
∑ xy : α × β, p xy = 1
hcard :
2 ≤ Fintype.card α
decode :
β → α
conclusion
condEntropy p
≤ binEntropy (errorProb p decode)
+ errorProb p decode * log ((Fintype.card α : ℝ) - 1)
Proof (Lean source)
theorem fano_inequality {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (hsum : ∑ xy : α × β, p xy = 1) (hcard : 2 ≤ Fintype.card α) (decode : β → α) : condEntropy p ≤ binEntropy (errorProb p decode) + errorProb p decode * log ((Fintype.card α : ℝ) - 1) := by have hcross := entropy_le_crossEntropy (p := p) (g := fanoRef p decode) hp0 (fun xy => fanoRef_nonneg hp0 hsum decode xy) (by rw [fanoRef_sum_eq_one hsum hcard decode, hsum]) (fun xy h => fanoRef_ac hp0 hsum hcard decode xy h) rw [neg_crossEntropy_fanoRef hp0 hsum hcard decode] at hcross rw [condEntropy_def] linarith
Causalean.Mathlib.InformationTheory.fano_inequality · Causalean/Mathlib/InformationTheory/Fano.lean:288 · uses condEntropy , errorProb
theorem fano_error_lower_bound reviewed
Causalean.Mathlib.InformationTheory

Fano error lower bound (the standard weakened corollary). For a nonnegative function p on α × β that sums to one, with at least two symbols in the alphabet α (2 ≤ Fintype.card α) and a decoder decode : β → α, the error probability Pe = errorProb p decode is bounded below: Pe ≥ (condEntropy p − Real.log 2) / Real.log (Fintype.card α).

Formal statement
hypotheses
α :
Type u_1
shared
β :
Type u_2
α × β → ℝ
shared
hp0 :
∀ xy, 0 ≤ p xy
hsum :
∑ xy : α × β, p xy = 1
hcard :
2 ≤ card α
decode :
β → α
conclusion
(condEntropy p - log 2) / log (card α) ≤ errorProb p decode
Proof (Lean source)
theorem fano_error_lower_bound {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (hsum : ∑ xy : α × β, p xy = 1) (hcard : 2 ≤ card α) (decode : β → α) : (condEntropy p - log 2) / log (card α) ≤ errorProb p decode := by let Pe : ℝ := errorProb p decode let M : ℝ := card α have hfano := fano_inequality hp0 hsum hcard decode have hPe_nonneg : 0 ≤ Pe := by simpa [Pe] using errorProb_nonneg hp0 decode have hMgt : (1 : ℝ) < M := by dsimp [M] exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 2) hcard) have hMminus_pos : 0 < M - 1 := by linarith have hMminus_le : M - 1 ≤ M := by linarith have hlog_mono : log (M - 1) ≤ log M := Real.log_le_log hMminus_pos hMminus_le have hmul_log : Pe * log (M - 1) ≤ Pe * log M := mul_le_mul_of_nonneg_left hlog_mono hPe_nonneg have hbin : binEntropy Pe ≤ log 2 := Real.binEntropy_le_log_two have hfano' : condEntropy p ≤ binEntropy Pe + Pe * log (M - 1) := by simpa [Pe, M] using hfano have hmain : condEntropy p - log 2 ≤ Pe * log M := by linarith have hlogM_pos : 0 < log M := Real.log_pos hMgt have hdiv : (condEntropy p - log 2) / log M ≤ Pe := by rw [div_le_iff₀ hlogM_pos] exact hmain simpa [Pe, M] using hdiv
Causalean.Mathlib.InformationTheory.fano_error_lower_bound · Causalean/Mathlib/InformationTheory/Fano.lean:312 · uses condEntropy , errorProb
5 supporting declarations (lemmas, instances)
  • fanoRef_def lemma — The Fano reference mass unfolds to the observation marginal times the decoder-dependent correct-or-error weight used in its definition.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    shared
    p :
    α × β → ℝ
    decode :
    β → α
    xy :
    α × β
    conclusion
    fanoRef p decode xy
    = yMarginal p xy.2 * (if xy.1 = decode xy.2 then 1 - errorProb p decode else errorProb p decode / ((Fintype.card α : ℝ) - 1))
    Proof (Lean source)
    @[simp] lemma fanoRef_def (p : α × β → ℝ) (decode : β → α) (xy : α × β) : fanoRef p decode xy = yMarginal p xy.2 * (if xy.1 = decode xy.2 then 1 - errorProb p decode else errorProb p decode / ((Fintype.card α : ℝ) - 1)) := rfl
    Causalean.Mathlib.InformationTheory.fanoRef_def · Causalean/Mathlib/InformationTheory/Fano.lean:53
  • fanoRef_nonneg lemma — The Fano reference distribution is nonnegative.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    hsum :
    ∑ xy : α × β, p xy = 1
    decode :
    β → α
    xy :
    α × β
    conclusion
    0 ≤ fanoRef p decode xy
    Proof (Lean source)
    lemma fanoRef_nonneg {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (hsum : ∑ xy : α × β, p xy = 1) (decode : β → α) (xy : α × β) : 0 ≤ fanoRef p decode xy := by rw [fanoRef_def] refine mul_nonneg (yMarginal_nonneg hp0 xy.2) ?_ split_ifs · exact sub_nonneg.mpr (errorProb_le_one hp0 hsum decode) · exact div_nonneg (errorProb_nonneg hp0 decode) (by have hMge1 : (1 : ℝ) ≤ (Fintype.card α : ℝ) := by exact_mod_cast Fintype.card_pos_iff.mpr ⟨xy.1⟩ linarith)
    Causalean.Mathlib.InformationTheory.fanoRef_nonneg · Causalean/Mathlib/InformationTheory/Fano.lean:61
  • fanoRef_sum_eq_one lemma — The Fano reference distribution is a probability mass function: ∑ xy, fanoRef = 1. On each column the inner weights sum to (1 − Pe) + (card α − 1) · Pe/(card α − 1) = 1, so the total is ∑ y, yMarginal p y = 1.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hsum :
    ∑ xy : α × β, p xy = 1
    hcard :
    2 ≤ card α
    decode :
    β → α
    conclusion
    ∑ xy : α × β, fanoRef p decode xy = 1
    Proof (Lean source)
    lemma fanoRef_sum_eq_one {p : α × β → ℝ} (hsum : ∑ xy : α × β, p xy = 1) (hcard : 2 ≤ Fintype.card α) (decode : β → α) : ∑ xy : α × β, fanoRef p decode xy = 1 := by classical let Pe : ℝ := errorProb p decode let M : ℝ := Fintype.card α have hMne : M - 1 ≠ 0 := by have hMgt : 1 < M := by dsimp [M] exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 2) hcard) linarith have hinner : ∀ y : β, (∑ x : α, (if x = decode y then 1 - Pe else Pe / (M - 1))) = 1 := by intro y calc (∑ x : α, (if x = decode y then 1 - Pe else Pe / (M - 1))) = ∑ x : α, ((if x = decode y then (1 - Pe) - Pe / (M - 1) else 0) + Pe / (M - 1)) := by refine Finset.sum_congr rfl ?_ intro x hx by_cases h : x = decode y <;> simp [h] _ = (∑ x : α, (if x = decode y then (1 - Pe) - Pe / (M - 1) else 0)) + ∑ x : α, Pe / (M - 1) := by simp [Finset.sum_add_distrib] _ = ((1 - Pe) - Pe / (M - 1)) + (Fintype.card α : ℝ) * (Pe / (M - 1)) := by have hsingle : (∑ x : α, (if x = decode y then (1 - Pe) - Pe / (M - 1) else 0)) = (1 - Pe) - Pe / (M - 1) := by rw [Finset.sum_ite_eq' univ (decode y)] simp rw [hsingle] simp _ = 1 := by dsimp [M] at hMne ⊢ field_simp [hMne] ring rw [Fintype.sum_prod_type] calc (∑ x : α, ∑ y : β, fanoRef p decode (x, y)) = ∑ y : β, ∑ x : α, fanoRef p decode (x, y) := by rw [Finset.sum_comm] _ = ∑ y : β, yMarginal p y * 1 := by refine Finset.sum_congr rfl ?_ intro y hy simp_rw [fanoRef_def] rw [← Finset.mul_sum] simpa [Pe, M] using congrArg (fun z => yMarginal p y * z) (hinner y) _ = 1 := by simpa using yMarginal_sum (α := α) (β := β) hsum
    Causalean.Mathlib.InformationTheory.fanoRef_sum_eq_one · Causalean/Mathlib/InformationTheory/Fano.lean:74
  • fanoRef_ac lemma — The Fano reference distribution dominates the support of p: p xy ≠ 0 → 0 < fanoRef xy. A nonzero p (x, y) forces yMarginal p y > 0; on a correct cell the complementary mass 1 − Pe ≥ p (x,y) > 0 and on an error cell Pe ≥ p (x,y) > 0, so the inner weight is positive. This is the absolute-continuity hypothesis of the Gibbs inequality.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    hsum :
    ∑ xy : α × β, p xy = 1
    hcard :
    2 ≤ card α
    decode :
    β → α
    xy :
    α × β
    hxy :
    p xy ≠ 0
    conclusion
    0 < fanoRef p decode xy
    Proof (Lean source)
    lemma fanoRef_ac {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (hsum : ∑ xy : α × β, p xy = 1) (hcard : 2 ≤ Fintype.card α) (decode : β → α) (xy : α × β) (hxy : p xy ≠ 0) : 0 < fanoRef p decode xy := by classical have hpxy_pos : 0 < p xy := lt_of_le_of_ne (hp0 xy) (Ne.symm hxy) have hy_pos : 0 < yMarginal p xy.2 := lt_of_lt_of_le hpxy_pos (by simpa [xy.eta] using le_yMarginal hp0 xy.1 xy.2) have hMpos : 0 < (Fintype.card α : ℝ) - 1 := by have hMgt : (1 : ℝ) < Fintype.card α := by exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 2) hcard) linarith rw [fanoRef_def] refine mul_pos hy_pos ?_ split_ifs with hc · have hterm_nonneg : ∀ z : α × β, z ∈ univ → 0 ≤ (if z.1 = decode z.2 then p z else 0) := by intro z hz split_ifs <;> simp [hp0] have hle : p xy ≤ ∑ z : α × β, (if z.1 = decode z.2 then p z else 0) := by simpa [hc] using (Finset.single_le_sum (f := fun z : α × β => if z.1 = decode z.2 then p z else 0) hterm_nonneg (Finset.mem_univ xy)) rw [correctMass_eq hsum decode] at hle exact lt_of_lt_of_le hpxy_pos hle · have hterm_nonneg : ∀ z : α × β, z ∈ univ → 0 ≤ (if z.1 = decode z.2 then 0 else p z) := by intro z hz split_ifs <;> simp [hp0] have hle : p xy ≤ ∑ z : α × β, (if z.1 = decode z.2 then 0 else p z) := by simpa [hc] using (Finset.single_le_sum (f := fun z : α × β => if z.1 = decode z.2 then 0 else p z) hterm_nonneg (Finset.mem_univ xy)) rw [← errorProb_def p decode] at hle exact div_pos (lt_of_lt_of_le hpxy_pos hle) hMpos
    Causalean.Mathlib.InformationTheory.fanoRef_ac · Causalean/Mathlib/InformationTheory/Fano.lean:128
  • neg_crossEntropy_fanoRef lemma — The cross-entropy of p against the Fano reference splits, via the chain rule for log on the support of p, into the marginal entropy plus the binary-entropy/error terms: −∑ xy, p xy · log (fanoRef p decode xy) = entropy (yMarginal p) + Real.binEntropy Pe + Pe · Real.log (card α − 1), where Pe = errorProb p decode. This is the key algebraic computation behind Fano.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    α × β → ℝ
    shared
    hp0 :
    ∀ xy, 0 ≤ p xy
    hsum :
    ∑ xy : α × β, p xy = 1
    hcard :
    2 ≤ Fintype.card α
    decode :
    β → α
    conclusion
    (- ∑ xy : α × β, p xy * log (fanoRef p decode xy))
    = entropy (yMarginal p)
    + binEntropy (errorProb p decode)
    + errorProb p decode * log ((Fintype.card α : ℝ) - 1)
    Proof (Lean source)
    lemma neg_crossEntropy_fanoRef {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (hsum : ∑ xy : α × β, p xy = 1) (hcard : 2 ≤ Fintype.card α) (decode : β → α) : (- ∑ xy : α × β, p xy * log (fanoRef p decode xy)) = entropy (yMarginal p) + binEntropy (errorProb p decode) + errorProb p decode * log ((Fintype.card α : ℝ) - 1) := by classical let Pe : ℝ := errorProb p decode let M : ℝ := Fintype.card α let inner : α × β → ℝ := fun xy => if xy.1 = decode xy.2 then 1 - Pe else Pe / (M - 1) have hMpos : 0 < M - 1 := by have hMgt : (1 : ℝ) < M := by dsimp [M] exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 2) hcard) linarith have hMne : M - 1 ≠ 0 := ne_of_gt hMpos have hsum_split : (∑ xy : α × β, p xy * log (fanoRef p decode xy)) = (∑ xy : α × β, p xy * log (yMarginal p xy.2)) + ∑ xy : α × β, p xy * log (inner xy) := by calc (∑ xy : α × β, p xy * log (fanoRef p decode xy)) = ∑ xy : α × β, (p xy * log (yMarginal p xy.2) + p xy * log (inner xy)) := by refine Finset.sum_congr rfl ?_ intro xy hxy_mem by_cases hpz : p xy = 0 · simp [hpz] · have hpxy_pos : 0 < p xy := lt_of_le_of_ne (hp0 xy) (Ne.symm hpz) have hy_pos : 0 < yMarginal p xy.2 := lt_of_lt_of_le hpxy_pos (by simpa [xy.eta] using le_yMarginal hp0 xy.1 xy.2) have hfr_pos := fanoRef_ac hp0 hsum hcard decode xy hpz have hfr_eq : fanoRef p decode xy = yMarginal p xy.2 * inner xy := by simp [fanoRef_def, inner, Pe, M] have hinner_pos : 0 < inner xy := by rw [hfr_eq] at hfr_pos exact pos_of_mul_pos_right hfr_pos (le_of_lt hy_pos) calc p xy * log (fanoRef p decode xy) = p xy * (log (yMarginal p xy.2) + log (inner xy)) := by rw [hfr_eq, Real.log_mul hy_pos.ne' hinner_pos.ne'] _ = p xy * log (yMarginal p xy.2) + p xy * log (inner xy) := by ring _ = (∑ xy : α × β, p xy * log (yMarginal p xy.2)) + ∑ xy : α × β, p xy * log (inner xy) := by rw [Finset.sum_add_distrib] have hYlog : (∑ xy : α × β, p xy * log (yMarginal p xy.2)) = - entropy (yMarginal p) := by calc (∑ xy : α × β, p xy * log (yMarginal p xy.2)) = ∑ x : α, ∑ y : β, p (x, y) * log (yMarginal p y) := by rw [Fintype.sum_prod_type] _ = ∑ y : β, ∑ x : α, p (x, y) * log (yMarginal p y) := by rw [Finset.sum_comm] _ = ∑ y : β, yMarginal p y * log (yMarginal p y) := by refine Finset.sum_congr rfl ?_ intro y hy rw [← Finset.sum_mul] rfl _ = - entropy (yMarginal p) := by rw [entropy_def] simp [Real.negMulLog_def, Finset.sum_neg_distrib] have hInnerLog : (∑ xy : α × β, p xy * log (inner xy)) = (1 - Pe) * log (1 - Pe) + Pe * log (Pe / (M - 1)) := by calc (∑ xy : α × β, p xy * log (inner xy)) = ∑ xy : α × β, ((if xy.1 = decode xy.2 then p xy else 0) * log (1 - Pe) + (if xy.1 = decode xy.2 then 0 else p xy) * log (Pe / (M - 1))) := by refine Finset.sum_congr rfl ?_ intro xy hxy_mem by_cases hc : xy.1 = decode xy.2 <;> simp [inner, hc] _ = (∑ xy : α × β, (if xy.1 = decode xy.2 then p xy else 0)) * log (1 - Pe) + (∑ xy : α × β, (if xy.1 = decode xy.2 then 0 else p xy)) * log (Pe / (M - 1)) := by rw [Finset.sum_add_distrib] rw [← Finset.sum_mul, ← Finset.sum_mul] _ = (1 - Pe) * log (1 - Pe) + Pe * log (Pe / (M - 1)) := by rw [correctMass_eq hsum decode] rw [← errorProb_def p decode] have hlog_total : (∑ xy : α × β, p xy * log (fanoRef p decode xy)) = - entropy (yMarginal p) + ((1 - Pe) * log (1 - Pe) + Pe * log (Pe / (M - 1))) := by rw [hsum_split, hYlog, hInnerLog] have hlog_div : Pe * log (Pe / (M - 1)) = Pe * log Pe - Pe * log (M - 1) := by by_cases hPe : Pe = 0 · simp [hPe] · rw [Real.log_div hPe hMne] ring calc (- ∑ xy : α × β, p xy * log (fanoRef p decode xy)) = - (- entropy (yMarginal p) + ((1 - Pe) * log (1 - Pe) + Pe * log (Pe / (M - 1)))) := by rw [hlog_total] _ = entropy (yMarginal p) + binEntropy Pe + Pe * log (M - 1) := by rw [hlog_div, Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub] simp [Real.negMulLog_def] ring _ = entropy (yMarginal p) + binEntropy (errorProb p decode) + errorProb p decode * log ((Fintype.card α : ℝ) - 1) := by simp [Pe, M]
    Causalean.Mathlib.InformationTheory.neg_crossEntropy_fanoRef · Causalean/Mathlib/InformationTheory/Fano.lean:174
Finite­KL 1 core · 0 supporting This file identifies measure-theoretic Kullback--Leibler divergence on a finite discrete space with the familiar finite sum of mass ratios. ★ klDiv_toReal_eq_sum_measureReal

Kullback--Leibler divergence on finite measurable spaces

This file identifies measure-theoretic Kullback--Leibler divergence on a finite discrete space with the familiar finite sum of mass ratios. It is the bridge between Mathlib's general-measure KL API and finite-alphabet entropy arguments.

theorem klDiv_toReal_eq_sum_measureReal reviewed
Causalean.Mathlib.InformationTheory

For probability measures μ and ν on a finite discrete space, if μ is absolutely continuous with respect to ν, then their real-valued Kullback--Leibler divergence is the sum of each μ-mass times the logarithm of its ratio to the corresponding ν-mass.

Formal statement
hypotheses
α :
Type*
Fintype α
MeasurableSpace α
MeasurableSingletonClass α
μ ν :
Measure α
IsProbabilityMeasure μ
IsProbabilityMeasure ν
hμν :
μ ≪ ν
conclusion
(_root_.InformationTheory.klDiv μ ν).toReal
= ∑ x : α, μ.real {x} * log (μ.real {x} / ν.real {x})
Proof (Lean source)
theorem klDiv_toReal_eq_sum_measureReal {α : Type*} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hμν : μ ≪ ν) : (_root_.InformationTheory.klDiv μ ν).toReal = ∑ x : α, μ.real {x} * log (μ.real {x} / ν.real {x}) := by rw [_root_.InformationTheory.toReal_klDiv_of_measure_eq hμν (by simp)] rw [integral_fintype .of_finite] apply Finset.sum_congr rfl intro x _hx by_cases hμx : μ {x} = 0 · simp [measureReal_def, hμx] have hνx : ν {x} ≠ 0 := fun h => hμx (hμν h) have hrn : μ.rnDeriv ν x = μ {x} / ν {x} := by have hae := Measure.withDensity_rnDeriv_eq μ ν hμν have happ := congrArg (fun m : Measure α => m {x}) hae simp only [MeasurableSet.singleton, withDensity_apply, Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul] at happ exact (ENNReal.eq_div_iff hνx (measure_ne_top ν {x})).2 happ simp only [llr_def, hrn] rw [ENNReal.toReal_div] rfl
Causalean.Mathlib.InformationTheory.klDiv_toReal_eq_sum_measureReal · Causalean/Mathlib/InformationTheory/FiniteKL.lean:21
Finite­Mutual­Information 2 core · 0 supporting This file gives the finite-sum identity equating information gained from a uniformly chosen finite hypothesis with the entropy drop after observing a finite output. ★ uniform_condEntropy_kl_identity★ uniform_information_le_average_logRatio

Mutual information of a uniform finite experiment

This file gives the finite-sum identity equating information gained from a uniformly chosen finite hypothesis with the entropy drop after observing a finite output. It supplies the algebraic bridge used by general-experiment forms of Fano's inequality.

theorem uniform_condEntropy_kl_identity reviewed
Causalean.Mathlib.InformationTheory

Given finite input and output alphabets, a nonnegative stochastic matrix r whose rows each sum to one, and a uniform input, the input entropy minus the conditional entropy equals the uniform average of the row-wise logarithmic density ratios against the output marginal.

Formal statement
hypotheses
α β :
Type*
Fintype α
Fintype β
Nonempty α
r :
α → β → ℝ
hr0 :
∀ i y, 0 ≤ r i y
hrsum :
∀ i, ∑ y, r i y = 1
conclusion
log (Fintype.card α)
- condEntropy (fun z : α × β => (Fintype.card α : ℝ)⁻¹ * r z.1 z.2)
= (Fintype.card α : ℝ)⁻¹ * ∑ i, ∑ y, r i y * log (r i y / ((Fintype.card α : ℝ)⁻¹ * ∑ k, r k y))
Proof (Lean source)
theorem uniform_condEntropy_kl_identity {α β : Type*} [Fintype α] [Fintype β] [Nonempty α] (r : α → β → ℝ) (hr0 : ∀ i y, 0 ≤ r i y) (hrsum : ∀ i, ∑ y, r i y = 1) : log (Fintype.card α) - condEntropy (fun z : α × β => (Fintype.card α : ℝ)⁻¹ * r z.1 z.2) = (Fintype.card α : ℝ)⁻¹ * ∑ i, ∑ y, r i y * log (r i y / ((Fintype.card α : ℝ)⁻¹ * ∑ k, r k y)) := by classical let N : ℝ := Fintype.card α let u : ℝ := N⁻¹ let p : α × β → ℝ := fun z => u * r z.1 z.2 let q : β → ℝ := fun y => u * ∑ i, r i y have hNpos : 0 < N := by dsimp [N] exact_mod_cast Fintype.card_pos have hu : 0 < u := inv_pos.mpr hNpos have hsumr : ∑ z : α × β, r z.1 z.2 = N := by rw [Fintype.sum_prod_type] simp_rw [hrsum] simp [N] have hsump : ∑ z : α × β, p z = 1 := by simp only [p] rw [← Finset.mul_sum, hsumr] simp [u, N, ne_of_gt hNpos] have hq : yMarginal p = q := by funext y simp [yMarginal, p, q, ← Finset.mul_sum] have hlogN : log N + log u = 0 := by rw [show u = N⁻¹ by rfl, Real.log_inv] ring have hcell : ∀ i y, u * r i y * log (r i y / q y) = p (i, y) * log N + p (i, y) * log (p (i, y)) - u * r i y * log (q y) := by intro i y by_cases hri : r i y = 0 · simp [hri, p] have hrpos : 0 < r i y := lt_of_le_of_ne (hr0 i y) (Ne.symm hri) have hqpos : 0 < q y := by dsimp [q] exact mul_pos hu (lt_of_lt_of_le hrpos (Finset.single_le_sum (fun j _ => hr0 j y) (Finset.mem_univ i))) rw [Real.log_div hrpos.ne' hqpos.ne', show p (i, y) = u * r i y by rfl, Real.log_mul hu.ne' hrpos.ne'] calc u * r i y * (log (r i y) - log (q y)) = u * r i y * (log N + log u + log (r i y) - log (q y)) := by rw [hlogN] ring _ = u * r i y * log N + u * r i y * (log u + log (r i y)) - u * r i y * log (q y) := by ring have hplogN : ∑ i, ∑ y, p (i, y) * log N = log N := by calc (∑ i, ∑ y, p (i, y) * log N) = (∑ i, ∑ y, p (i, y)) * log N := by rw [Finset.sum_mul] simp_rw [Finset.sum_mul] _ = (∑ z : α × β, p z) * log N := by rw [Fintype.sum_prod_type] _ = log N := by rw [hsump, one_mul] have hqlog : ∑ i, ∑ y, u * r i y * log (q y) = ∑ y, q y * log (q y) := by rw [Finset.sum_comm] apply Finset.sum_congr rfl intro y _hy rw [← Finset.sum_mul] simp only [q, ← Finset.mul_sum] have hpneg : (∑ i, ∑ y, -p (i, y) * log (p (i, y))) = -(∑ i, ∑ y, p (i, y) * log (p (i, y))) := by rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro i _hi rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro y _hy ring have hqneg : (∑ y, -q y * log (q y)) = -(∑ y, q y * log (q y)) := by rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro y _hy ring change log N - condEntropy p = u * ∑ i, ∑ y, r i y * log (r i y / q y) rw [condEntropy_def, hq, entropy_def, entropy_def] rw [Fintype.sum_prod_type] simp only [Real.negMulLog_def] simp_rw [Finset.mul_sum] simp_rw [← mul_assoc] simp_rw [hcell] rw [show (∑ i, ∑ y, (p (i, y) * log N + p (i, y) * log (p (i, y)) - u * r i y * log (q y))) = (∑ i, ∑ y, p (i, y) * log N) + (∑ i, ∑ y, p (i, y) * log (p (i, y))) - (∑ i, ∑ y, u * r i y * log (q y)) by simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]] rw [hplogN, hqlog, hpneg, hqneg] ring
Causalean.Mathlib.InformationTheory.uniform_condEntropy_kl_identity · Causalean/Mathlib/InformationTheory/FiniteMutualInformation.lean:19 · uses condEntropy
theorem uniform_information_le_average_logRatio reviewed
Causalean.Mathlib.InformationTheory

Given finite input and output alphabets, a nonnegative stochastic matrix r whose rows sum to one, and a reference output mass function q that sums to one and dominates every row's support, the uniform-input information relative to the output marginal is at most the average logarithmic density ratio to q.

Formal statement
hypotheses
α β :
Type*
Fintype α
Fintype β
Nonempty α
r :
α → β → ℝ
hr0 :
∀ i y, 0 ≤ r i y
hrsum :
∀ i, ∑ y, r i y = 1
q :
β → ℝ
hq0 :
∀ y, 0 ≤ q y
hqsum :
∑ y, q y = 1
hac :
∀ i y
if
r i y ≠ 0
then
q y ≠ 0
conclusion
(Fintype.card α : ℝ)⁻¹ * ∑ i, ∑ y, r i y * log (r i y / ((Fintype.card α : ℝ)⁻¹ * ∑ k, r k y))
≤ (Fintype.card α : ℝ)⁻¹ * ∑ i, ∑ y, r i y * log (r i y / q y)
Proof (Lean source)
theorem uniform_information_le_average_logRatio {α β : Type*} [Fintype α] [Fintype β] [Nonempty α] (r : α → β → ℝ) (hr0 : ∀ i y, 0 ≤ r i y) (hrsum : ∀ i, ∑ y, r i y = 1) (q : β → ℝ) (hq0 : ∀ y, 0 ≤ q y) (hqsum : ∑ y, q y = 1) (hac : ∀ i y, r i y ≠ 0 → q y ≠ 0) : (Fintype.card α : ℝ)⁻¹ * ∑ i, ∑ y, r i y * log (r i y / ((Fintype.card α : ℝ)⁻¹ * ∑ k, r k y)) ≤ (Fintype.card α : ℝ)⁻¹ * ∑ i, ∑ y, r i y * log (r i y / q y) := by classical let N : ℝ := Fintype.card α let u : ℝ := N⁻¹ let qbar : β → ℝ := fun y => u * ∑ i, r i y have hNpos : 0 < N := by dsimp [N] exact_mod_cast Fintype.card_pos have hu : 0 < u := inv_pos.mpr hNpos have hqbar0 : ∀ y, 0 ≤ qbar y := fun y => mul_nonneg hu.le (Finset.sum_nonneg fun i _hi => hr0 i y) have hqbarsum : ∑ y, qbar y = 1 := by simp only [qbar, ← Finset.mul_sum] rw [Finset.sum_comm] simp_rw [hrsum] simp [u, N, ne_of_gt hNpos] have hacbar : ∀ y, qbar y ≠ 0 → 0 < q y := by intro y hqbar have hsumne : ∑ i, r i y ≠ 0 := by intro hzero exact hqbar (by simp [qbar, hzero]) obtain ⟨i, _hi, hri⟩ := Finset.exists_ne_zero_of_sum_ne_zero hsumne exact lt_of_le_of_ne (hq0 y) (Ne.symm (hac i y hri)) have hcross := entropy_le_crossEntropy hqbar0 hq0 (by rw [hqbarsum, hqsum]) hacbar have hlogs : ∑ y, qbar y * log (q y) ≤ ∑ y, qbar y * log (qbar y) := by rw [entropy_def] at hcross simp only [Real.negMulLog_def] at hcross have hneg : (∑ y, -qbar y * log (qbar y)) = -(∑ y, qbar y * log (qbar y)) := by rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro y _hy ring rw [hneg] at hcross linarith have hleft : u * ∑ i, ∑ y, r i y * log (r i y / qbar y) = u * ∑ i, ∑ y, r i y * log (r i y) - ∑ y, qbar y * log (qbar y) := by have hcell : ∀ i y, u * (r i y * log (r i y / qbar y)) = u * (r i y * log (r i y)) - u * r i y * log (qbar y) := by intro i y by_cases hri : r i y = 0 · simp [hri] have hrpos : 0 < r i y := lt_of_le_of_ne (hr0 i y) (Ne.symm hri) have hqbarpos : 0 < qbar y := by dsimp [qbar] exact mul_pos hu (lt_of_lt_of_le hrpos (Finset.single_le_sum (fun j _ => hr0 j y) (Finset.mem_univ i))) rw [Real.log_div hrpos.ne' hqbarpos.ne'] ring simp_rw [Finset.mul_sum, hcell] rw [show (∑ i, ∑ y, (u * (r i y * log (r i y)) - u * r i y * log (qbar y))) = (∑ i, ∑ y, u * (r i y * log (r i y))) - (∑ i, ∑ y, u * r i y * log (qbar y)) by simp only [Finset.sum_sub_distrib]] congr 1 rw [Finset.sum_comm] apply Finset.sum_congr rfl intro y _hy rw [← Finset.sum_mul] simp only [qbar, ← Finset.mul_sum] have hright : u * ∑ i, ∑ y, r i y * log (r i y / q y) = u * ∑ i, ∑ y, r i y * log (r i y) - ∑ y, qbar y * log (q y) := by have hcell : ∀ i y, u * (r i y * log (r i y / q y)) = u * (r i y * log (r i y)) - u * r i y * log (q y) := by intro i y by_cases hri : r i y = 0 · simp [hri] have hrpos : 0 < r i y := lt_of_le_of_ne (hr0 i y) (Ne.symm hri) have hqpos : 0 < q y := lt_of_le_of_ne (hq0 y) (Ne.symm (hac i y hri)) rw [Real.log_div hrpos.ne' hqpos.ne'] ring simp_rw [Finset.mul_sum, hcell] rw [show (∑ i, ∑ y, (u * (r i y * log (r i y)) - u * r i y * log (q y))) = (∑ i, ∑ y, u * (r i y * log (r i y))) - (∑ i, ∑ y, u * r i y * log (q y)) by simp only [Finset.sum_sub_distrib]] congr 1 rw [Finset.sum_comm] apply Finset.sum_congr rfl intro y _hy rw [← Finset.sum_mul] simp only [qbar, ← Finset.mul_sum] change u * ∑ i, ∑ y, r i y * log (r i y / qbar y) ≤ u * ∑ i, ∑ y, r i y * log (r i y / q y) rw [hleft, hright] linarith
Causalean.Mathlib.InformationTheory.uniform_information_le_average_logRatio · Causalean/Mathlib/InformationTheory/FiniteMutualInformation.lean:131
Finite­Word­Chain­Rule 7 core · 13 supporting This module disintegrates an arbitrary probability mass function on a finite word into its strict-prefix marginal and a totalized conditional law for the last symbol. ★ klDiv_eq_chainKL

Kullback--Leibler chain rule for finite words

This module disintegrates an arbitrary probability mass function on a finite word into its strict-prefix marginal and a totalized conditional law for the last symbol. It then expresses Kullback--Leibler divergence recursively through the resulting chronological factorization, without requiring full support except for the explicit pointwise conditional-divergence formula.

def appendSymbol reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

Given a finite word and a final symbol, append the symbol to the word.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
k :
Nat
u :
Fin k → Ω
x :
Ω
def
appendSymbol u x :
Fin (k + 1) → Ω
given by
Fin.lastCases x u
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.appendSymbol · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:26
def lastCoordinateSplit reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

Given a prefix length, split a nonempty finite word into its strict prefix and last symbol.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
k :
Nat
def
lastCoordinateSplit k :
(Fin (k + 1) → Ω) ≃ (Fin k → Ω) × Ω
given by
clause 1
toFun w := (fun i ↦ w i.castSucc, w (last k))
clause 2
invFun ux := appendSymbol ux.1 ux.2
clause 3
left_inv w := by funext i refine Fin.lastCases ?_ (fun j ↦ ?_) i · simp [appendSymbol] · simp [appendSymbol]
clause 4
right_inv ux := by rcases ux with ⟨u, x⟩ ext i <;> simp [appendSymbol]
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.lastCoordinateSplit · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:37
def prefixPMF reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

Given a probability mass function on nonempty finite words, its strict-prefix marginal sums over the final symbol.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
k :
Nat
p :
PMF (Fin (k + 1) → Ω)
def
prefixPMF p :
PMF (Fin k → Ω)
given by
PMF.ofFintype (fun u ↦ ∑ x : Ω, p (appendSymbol u x)) (by calc ∑ u, ∑ x : Ω, p (appendSymbol u x) = ∑ ux : (Fin k → Ω) × Ω, p (appendSymbol ux.1 ux.2) := by rw [Fintype.sum_prod_type] _ = ∑ w, p w := by rw [← (lastCoordinateSplit k).sum_comp] apply Finset.sum_congr rfl intro w _ change p ((lastCoordinateSplit k).symm ((lastCoordinateSplit k) w)) = p w rw [Equiv.symm_apply_apply] _ = 1 := by simpa only [tsum_fintype] using PMF.tsum_coe p)
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.prefixPMF · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:51
def nextSymbolPMF reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

Given a finite-word law and a strict prefix, the conditional law of the last symbol is the normalized extension mass, totalized by a point mass on null prefixes.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
k :
Nat
p :
PMF (Fin (k + 1) → Ω)
u :
Fin k → Ω
def
nextSymbolPMF p u :
PMF Ω
given by
if h : prefixPMF p u
= 0 then PMF.pure (choice inferInstance) else PMF.ofFintype (fun x ↦ p (appendSymbol u x) / prefixPMF p u) (by calc ∑ x : Ω, p (appendSymbol u x) / prefixPMF p u = (∑ x : Ω, p (appendSymbol u x)) / prefixPMF p u := by simp_rw [ENNReal.div_eq_inv_mul] rw [Finset.mul_sum] _ = prefixPMF p u / prefixPMF p u := by rw [prefixPMF_apply] _ = 1 := ENNReal.div_self h (PMF.apply_ne_top _ _))
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.nextSymbolPMF · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:75
def nextSymbolKernel reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

Given a finite-word law, its conditional last-symbol laws form a kernel on strict prefixes.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
k :
Nat
p :
PMF (Fin (k + 1) → Ω)
def
nextSymbolKernel p :
Kernel (Fin k → Ω) Ω
given by
Kernel.ofFunOfCountable (fun u ↦ (nextSymbolPMF p u).toMeasure)
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.nextSymbolKernel · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:93
def chainKL reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

The chronological conditional-KL sum recursively adds the shared-prefix conditional divergence of two finite-word laws at each word length.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
k :
ℕ
shared
def
chainKL k :
(k : Nat) → PMF (Fin k → Ω) → PMF (Fin k → Ω) → ℝ≥0∞
given by
clause 1
| 0, _, _ => 0
clause 2
| k + 1, p, q
=> chainKL k (prefixPMF p) (prefixPMF q)
+ klDiv ((prefixPMF p).toMeasure.compProd (nextSymbolKernel p)) ((prefixPMF p).toMeasure.compProd (nextSymbolKernel q))
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.chainKL · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:270
lemma klDiv_eq_chainKL reviewed
Causalean.Mathlib.InformationTheory.FiniteWordChainRule

Given a word length and two finite-word laws, their KL divergence equals the chronological sum of their history-dependent one-step conditional increments.

Formal statement
hypotheses
Ω :
Type u_1
shared
k :
Nat
p q :
PMF (Fin k → Ω)
conclusion
klDiv p.toMeasure q.toMeasure = chainKL k p q
Proof (Lean source)
lemma klDiv_eq_chainKL (k : Nat) (p q : PMF (Fin k → Ω)) : klDiv p.toMeasure q.toMeasure = chainKL k p q := by induction k with | zero => have hpq : p.toMeasure = q.toMeasure := by apply Measure.ext intro s hs by_cases hnonempty : s.Nonempty · rcases hnonempty with ⟨x, hx⟩ have hs_univ : s = univ := by apply Set.eq_univ_of_forall intro y simpa only [Subsingleton.elim y x] using hx simp [hs_univ] · have hs_empty : s = ∅ := Set.not_nonempty_iff_eq_empty.mp hnonempty simp [hs_empty] rw [hpq] simp [chainKL] | succ k ih => rw [klDiv_lastCoordinate_eq_add, ih] rfl
Causalean.Mathlib.InformationTheory.FiniteWordChainRule.klDiv_eq_chainKL · Causalean/Mathlib/InformationTheory/FiniteWordChainRule.lean:281 · uses chainKL
13 supporting declarations (lemmas, instances)
Gaussian­KL 1 core · 6 supporting Mathlib provides the real Gaussian measure ProbabilityTheory.gaussianReal m v (mean m : ℝ, variance v : ℝ≥0) and the Kullback–Leibler divergence InformationTheory.klDiv (an ℝ≥0∞), but not the closed form of the KL diverg ★ gaussianKL_eq

Kullback–Leibler divergence between real Gaussian measures

Mathlib provides the real Gaussian measure ProbabilityTheory.gaussianReal m v (mean m : ℝ, variance v : ℝ≥0) and the Kullback–Leibler divergence InformationTheory.klDiv (an ℝ≥0∞), but not the closed form of the KL divergence between two Gaussians. This file derives the equal-variance closed form

`klDiv (gaussianReal m₀ v) (gaussianReal m₁ v) = ENNReal.ofReal ((m₀ - m₁)^2 / (2 * v)) (0 < v`),

the standard equal-variance Gaussian KL identity.

Proof outline

For 0 < v both measures are volume.withDensity (gaussianPDF · v) with a strictly positive density, hence mutually absolutely continuous with volume. The derivation follows the standard four steps:

1. gaussianReal_ac_gaussianReal — absolute continuity gaussianReal m₀ v ≪ gaussianReal m₁ v, via volume as an intermediary. 2. llr_gaussianReal_ae — the log-likelihood ratio is a.e. the difference of the two Gaussian log-densities; at equal variance the normalising constants cancel, leaving the affine function x ↦ (m₀ - m₁) * (2*x - m₀ - m₁) / (2*v). 3. integrable_llr_gaussianReal — that affine ratio is integrable under gaussianReal m₀ v (the Gaussian has a finite first moment). 4. gaussianKL_eq — klDiv = ENNReal.ofReal (∫ llr ∂gaussianReal m₀ v), evaluated with ∫ x ∂gaussianReal m₀ v = m₀.

Main result

  • gaussianKL_eq — the equal-variance Gaussian KL closed form (the reusable workhorse).

References

Standard information-theory identity KL(N(m₀,σ²) ∥ N(m₁,σ²)) = (m₀ − m₁)² / (2σ²) (e.g. Cover & Thomas).

theorem gaussianKL_eq reviewed
Causalean.Mathlib.InformationTheory

Equal-variance Gaussian KL divergence (closed form). For two real means and a strictly positive common variance, the Kullback–Leibler divergence between the corresponding equal-variance Gaussians equals their squared mean difference divided by twice the variance:

Formal statement
hypotheses
v :
NNReal
shared
m₀ m₁ :
ℝ
hv :
0 < v
conclusion
klDiv (gaussianReal m₀ v) (gaussianReal m₁ v)
= ofReal ((m₀ - m₁) ^ 2 / (2 * (v : ℝ)))
Proof (Lean source)
theorem gaussianKL_eq (m₀ m₁ : ℝ) (hv : 0 < v) : klDiv (gaussianReal m₀ v) (gaussianReal m₁ v) = ofReal ((m₀ - m₁) ^ 2 / (2 * (v : ℝ))) := by have hv0 : v ≠ 0 := hv.ne' rw [InformationTheory.klDiv_of_ac_of_integrable (gaussianReal_ac_gaussianReal m₀ m₁ hv0 hv0) (integrable_llr_gaussianReal m₀ m₁ hv0)] rw [integral_llr_gaussianReal m₀ m₁ hv0] simp
Causalean.Mathlib.InformationTheory.gaussianKL_eq · Causalean/Mathlib/InformationTheory/GaussianKL.lean:179
6 supporting declarations (lemmas, instances)
  • gaussianReal_ac_gaussianReal lemma — Absolute continuity of nondegenerate Gaussians. For v₀ ≠ 0 and v₁ ≠ 0, gaussianReal m₀ v₀ is absolutely continuous with respect to gaussianReal m₁ v₁: both are volume.withDensity of a strictly positive density, so each is mutually absolutely continuous with Lebesgue measure, and absolute continuity is transitive.
    hypotheses
    m₀ m₁ :
    ℝ
    v₀ v₁ :
    ℝ≥0
    hv₀ :
    v₀ ≠ 0
    hv₁ :
    v₁ ≠ 0
    conclusion
    gaussianReal m₀ v₀ ≪ gaussianReal m₁ v₁
    Proof (Lean source)
    lemma gaussianReal_ac_gaussianReal (m₀ m₁ : ℝ) {v₀ v₁ : ℝ≥0} (hv₀ : v₀ ≠ 0) (hv₁ : v₁ ≠ 0) : gaussianReal m₀ v₀ ≪ gaussianReal m₁ v₁ := (gaussianReal_absolutelyContinuous m₀ hv₀).trans (gaussianReal_absolutelyContinuous' m₁ hv₁)
    Causalean.Mathlib.InformationTheory.gaussianReal_ac_gaussianReal · Causalean/Mathlib/InformationTheory/GaussianKL.lean:59
  • rnDeriv_toReal_gaussianReal_ae lemma — Radon–Nikodym ratio of equal-variance Gaussians, as a real number. For v ≠ 0, the real part of the Radon–Nikodym derivative ∂(gaussianReal m₀ v)/∂(gaussianReal m₁ v) is a.e. (with respect to gaussianReal m₀ v) the pointwise ratio of the two Gaussian densities gaussianPDFReal m₀ v x / gaussianPDFReal m₁ v x.
    hypotheses
    v :
    NNReal
    shared
    m₀ m₁ :
    ℝ
    hv :
    v ≠ 0
    conclusion
    (fun x ↦ ((gaussianReal m₀ v).rnDeriv (gaussianReal m₁ v) x).toReal)
    =ᵐ[gaussianReal m₀ v] fun x ↦ gaussianPDFReal m₀ v x / gaussianPDFReal m₁ v x
    Proof (Lean source)
    lemma rnDeriv_toReal_gaussianReal_ae (m₀ m₁ : ℝ) (hv : v ≠ 0) : (fun x ↦ ((gaussianReal m₀ v).rnDeriv (gaussianReal m₁ v) x).toReal) =ᵐ[gaussianReal m₀ v] fun x ↦ gaussianPDFReal m₀ v x / gaussianPDFReal m₁ v x := by let μ : Measure ℝ := gaussianReal m₀ v let ν : Measure ℝ := gaussianReal m₁ v have hμvol : μ ≪ volume := gaussianReal_absolutelyContinuous m₀ hv have hμν : μ ≪ ν := gaussianReal_ac_gaussianReal m₀ m₁ hv hv have hvolν : volume ≪ ν := gaussianReal_absolutelyContinuous' m₁ hv have hchain : μ.rnDeriv volume * volume.rnDeriv ν =ᵐ[μ] μ.rnDeriv ν := by exact hμν (Measure.rnDeriv_mul_rnDeriv (μ := μ) (ν := volume) (κ := ν) hμvol) have hμpdf : μ.rnDeriv volume =ᵐ[μ] gaussianPDF m₀ v := hμvol (rnDeriv_gaussianReal m₀ v) have hνpdf_vol : (ν.rnDeriv volume)⁻¹ =ᵐ[volume] volume.rnDeriv ν := by exact Measure.inv_rnDeriv' (μ := volume) (ν := ν) hvolν have hνpdf : (gaussianPDF m₁ v)⁻¹ =ᵐ[μ] volume.rnDeriv ν := by exact hμvol (((rnDeriv_gaussianReal m₁ v).symm.inv).trans hνpdf_vol) filter_upwards [hchain, hμpdf, hνpdf] with x hchain hx0 hx1 rw [← hchain] simp only [Pi.mul_apply] rw [hx0, ← hx1] simp [div_eq_mul_inv]
    Causalean.Mathlib.InformationTheory.rnDeriv_toReal_gaussianReal_ae · Causalean/Mathlib/InformationTheory/GaussianKL.lean:69
  • llr_gaussianReal_ae lemma — Log-likelihood ratio of equal-variance Gaussians. For v ≠ 0, the log-likelihood ratio llr (gaussianReal m₀ v) (gaussianReal m₁ v) is a.e. (with respect to gaussianReal m₀ v) equal to the affine function x ↦ (m₀ - m₁) * (2*x - m₀ - m₁) / (2*v). At equal variance the (√(2πv))⁻¹ normalising constants cancel in the density ratio, so the log-ratio reduces to ((x - m₁)^2 - (x - m₀)^2) / (2*v) = (m₀ - m₁)*(2*x - m₀ - m₁)/(2*v).
    hypotheses
    v :
    NNReal
    shared
    m₀ m₁ :
    ℝ
    hv :
    v ≠ 0
    conclusion
    llr (gaussianReal m₀ v) (gaussianReal m₁ v)
    =ᵐ[gaussianReal m₀ v] fun x ↦ (m₀ - m₁) * (2 * x - m₀ - m₁) / (2 * (v : ℝ))
    Proof (Lean source)
    lemma llr_gaussianReal_ae (m₀ m₁ : ℝ) (hv : v ≠ 0) : llr (gaussianReal m₀ v) (gaussianReal m₁ v) =ᵐ[gaussianReal m₀ v] fun x ↦ (m₀ - m₁) * (2 * x - m₀ - m₁) / (2 * (v : ℝ)) := by filter_upwards [rnDeriv_toReal_gaussianReal_ae m₀ m₁ hv] with x hx have hvposNN : 0 < v := by exact zero_lt_iff.mpr hv have hvpos : 0 < (v : ℝ) := by exact_mod_cast hvposNN have hc : (√(2 * π * (v : ℝ)))⁻¹ ≠ 0 := by positivity simp only [llr_def, hx] calc log (gaussianPDFReal m₀ v x / gaussianPDFReal m₁ v x) = log (rexp (-(x - m₀) ^ 2 / (2 * (v : ℝ))) / rexp (-(x - m₁) ^ 2 / (2 * (v : ℝ)))) := by congr 1 simp [gaussianPDFReal] field_simp [hc] _ = (-(x - m₀) ^ 2 / (2 * (v : ℝ))) - (-(x - m₁) ^ 2 / (2 * (v : ℝ))) := by rw [Real.log_div (Real.exp_ne_zero _) (Real.exp_ne_zero _)] simp _ = (m₀ - m₁) * (2 * x - m₀ - m₁) / (2 * (v : ℝ)) := by field_simp [(show (2 : ℝ) * (v : ℝ) ≠ 0 by positivity)] ring
    Causalean.Mathlib.InformationTheory.llr_gaussianReal_ae · Causalean/Mathlib/InformationTheory/GaussianKL.lean:96
  • integrable_llr_gaussianReal lemma — Integrability of the Gaussian log-likelihood ratio. For v ≠ 0, the affine log-likelihood ratio x ↦ (m₀ - m₁) * (2*x - m₀ - m₁) / (2*v) is integrable with respect to gaussianReal m₀ v, because the Gaussian has a finite first moment.
    hypotheses
    v :
    NNReal
    shared
    m₀ m₁ :
    ℝ
    hv :
    v ≠ 0
    conclusion
    Integrable (llr (gaussianReal m₀ v) (gaussianReal m₁ v)) (gaussianReal m₀ v)
    Proof (Lean source)
    @[fun_prop] lemma integrable_llr_gaussianReal (m₀ m₁ : ℝ) (hv : v ≠ 0) : Integrable (llr (gaussianReal m₀ v) (gaussianReal m₁ v)) (gaussianReal m₀ v) := by have hid : Integrable (fun x : ℝ ↦ x) (gaussianReal m₀ v) := by simpa [Function.id_def] using (memLp_id_gaussianReal (μ := m₀) (v := v) (p := 1)).integrable (by norm_num) have haffine : Integrable (fun x : ℝ ↦ ((m₀ - m₁) / (2 * (v : ℝ))) * (2 * x - (m₀ + m₁))) (gaussianReal m₀ v) := by exact (((hid.const_mul 2).sub (integrable_const (m₀ + m₁))).const_mul ((m₀ - m₁) / (2 * (v : ℝ)))) have htarget : Integrable (fun x : ℝ ↦ (m₀ - m₁) * (2 * x - m₀ - m₁) / (2 * (v : ℝ))) (gaussianReal m₀ v) := by convert haffine using 1 funext x ring exact htarget.congr (llr_gaussianReal_ae m₀ m₁ hv).symm
    Causalean.Mathlib.InformationTheory.integrable_llr_gaussianReal · Causalean/Mathlib/InformationTheory/GaussianKL.lean:126
  • integral_llr_gaussianReal lemma — Integral of the Gaussian log-likelihood ratio. For v ≠ 0, ∫ llr (gaussianReal m₀ v) (gaussianReal m₁ v) ∂(gaussianReal m₀ v) = (m₀ - m₁)^2 / (2*v), obtained by integrating the affine a.e. form against ∫ x ∂gaussianReal m₀ v = m₀.
    hypotheses
    v :
    NNReal
    shared
    m₀ m₁ :
    ℝ
    hv :
    v ≠ 0
    conclusion
    ∫ x, llr (gaussianReal m₀ v) (gaussianReal m₁ v) x ∂(gaussianReal m₀ v)
    = (m₀ - m₁) ^ 2 / (2 * (v : ℝ))
    Proof (Lean source)
    lemma integral_llr_gaussianReal (m₀ m₁ : ℝ) (hv : v ≠ 0) : ∫ x, llr (gaussianReal m₀ v) (gaussianReal m₁ v) x ∂(gaussianReal m₀ v) = (m₀ - m₁) ^ 2 / (2 * (v : ℝ)) := by have hid : Integrable (fun x : ℝ ↦ x) (gaussianReal m₀ v) := by simpa [Function.id_def] using (memLp_id_gaussianReal (μ := m₀) (v := v) (p := 1)).integrable (by norm_num) have hden : (2 : ℝ) * (v : ℝ) ≠ 0 := by have hvposNN : 0 < v := by exact zero_lt_iff.mpr hv have hvpos : 0 < (v : ℝ) := by exact_mod_cast hvposNN positivity rw [integral_congr_ae (llr_gaussianReal_ae m₀ m₁ hv)] calc ∫ x, (m₀ - m₁) * (2 * x - m₀ - m₁) / (2 * (v : ℝ)) ∂(gaussianReal m₀ v) = ∫ x, ((m₀ - m₁) / (2 * (v : ℝ))) * (2 * x - (m₀ + m₁)) ∂(gaussianReal m₀ v) := by apply integral_congr_ae exact ae_of_all _ (fun x ↦ by ring) _ = ((m₀ - m₁) / (2 * (v : ℝ))) * ∫ x, (2 * x - (m₀ + m₁)) ∂(gaussianReal m₀ v) := by rw [integral_const_mul] _ = ((m₀ - m₁) / (2 * (v : ℝ))) * (2 * m₀ - (m₀ + m₁)) := by rw [integral_sub (hid.const_mul 2) (integrable_const (m₀ + m₁))] rw [integral_const_mul, integral_id_gaussianReal] simp [integral_const] _ = (m₀ - m₁) ^ 2 / (2 * (v : ℝ)) := by field_simp [hden] ring
    Causalean.Mathlib.InformationTheory.integral_llr_gaussianReal · Causalean/Mathlib/InformationTheory/GaussianKL.lean:148
  • gaussianReal_klDiv_eq_of_ne_zero theorem — Two real Gaussian locations with a common nonzero variance have Kullback--Leibler divergence equal to the squared location difference divided by twice the variance.
    hypotheses
    m₀ m₁ :
    ℝ
    v :
    ℝ≥0
    hv :
    v ≠ 0
    conclusion
    klDiv (gaussianReal m₀ v) (gaussianReal m₁ v)
    = ofReal ((m₀ - m₁) ^ 2 / (2 * (v : ℝ)))
    Proof (Lean source)
    theorem gaussianReal_klDiv_eq_of_ne_zero (m₀ m₁ : ℝ) (v : ℝ≥0) (hv : v ≠ 0) : klDiv (gaussianReal m₀ v) (gaussianReal m₁ v) = ofReal ((m₀ - m₁) ^ 2 / (2 * (v : ℝ))) := gaussianKL_eq m₀ m₁ (zero_lt_iff.mpr hv)
    Causalean.Mathlib.InformationTheory.gaussianReal_klDiv_eq_of_ne_zero · Causalean/Mathlib/InformationTheory/GaussianKL.lean:196
KLBind 2 core · 4 supporting This file proves Kullback--Leibler identities for composition products and binds whose two laws share the same base measure and differ only in their conditional kernels. ★ klDiv_compProd_right_of_forall_ac★ klDiv_bind_eq_of_base_recording

KL Identities for Shared-Base Binds

This file proves Kullback--Leibler identities for composition products and binds whose two laws share the same base measure and differ only in their conditional kernels. These are measure-theoretic chain-rule tools for bind-based information arguments.

Inside the Measure namespace: * rnDeriv_compProd_right_of_forall_ac identifies the Radon--Nikodym derivative of μ ⊗ₘ κ with respect to μ ⊗ₘ η as the fibre derivative Kernel.rnDeriv κ η. * klDiv_compProd_right_of_forall_ac is the KL chain rule for shared-base composition products: klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, klDiv (κ a) (η a) ∂μ. * klDiv_map_measurableEmbedding shows that KL is invariant under a measurable embedding. * klDiv_bind_eq_of_base_recording transfers the chain rule to binds when the output records its base coordinate through a measurable projection.

lemma klDiv_compProd_right_of_forall_ac reviewed
Causalean.Mathlib.InformationTheory.Measure

For a countably-generated pair of measurable spaces, a finite base measure μ, and finite kernels κ, η out of the base, if κ b is absolutely continuous with respect to η b for μ-almost every base point b, then the Kullback–Leibler divergence between the composition products μ ⊗ₘ κ and μ ⊗ₘ η equals the μ-average, over the base point, of the Kullback–Leibler divergence between κ and η at that base point.

Formal statement
hypotheses
α :
Type u_1
shared
β :
Type u_2
shared
μ :
Measure α
shared
κ :
Kernel α β
shared
η :
Kernel α β
shared
CountableOrCountablyGenerated α β
IsFiniteMeasure μ
IsFiniteKernel κ
IsFiniteKernel η
hκη :
∀ᵐ a ∂μ, κ a ≪ η a
conclusion
_root_.InformationTheory.klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
= ∫⁻ a, _root_.InformationTheory.klDiv (κ a) (η a) ∂μ
Proof (Lean source)
lemma klDiv_compProd_right_of_forall_ac [CountableOrCountablyGenerated α β] [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : _root_.InformationTheory.klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, _root_.InformationTheory.klDiv (κ a) (η a) ∂μ := by classical have hcomp_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η := Measure.AbsolutelyContinuous.compProd_right hκη rw [_root_.InformationTheory.klDiv_eq_lintegral_klFun, if_pos hcomp_ac] trans ∫⁻ p : α × β, ofReal (_root_.InformationTheory.klFun ((Kernel.rnDeriv κ η p.1 p.2).toReal)) ∂(μ ⊗ₘ η) · refine lintegral_congr_ae ?_ filter_upwards [rnDeriv_compProd_right_of_forall_ac (μ := μ) (κ := κ) (η := η) hκη] with p hp rw [hp] · rw [Measure.lintegral_compProd] · refine lintegral_congr_ae ?_ filter_upwards [hκη] with a ha rw [_root_.InformationTheory.klDiv_eq_lintegral_klFun, if_pos ha] refine lintegral_congr_ae ?_ filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb rw [hb] · fun_prop
Causalean.Mathlib.InformationTheory.Measure.klDiv_compProd_right_of_forall_ac · Causalean/Mathlib/InformationTheory/KLBind.lean:81
lemma klDiv_bind_eq_of_base_recording reviewed
Causalean.Mathlib.InformationTheory.Measure

For measurable spaces B and Ω, a finite base measure m, finite kernels κ, η from B to Ω, and a measurable projection proj : Ω → B whose graph {(b, ω) | b = proj ω} is a measurable subset of B × Ω, suppose κ-almost every output, for m-almost every base point b, lands in the fibre proj⁻¹{b}, likewise for η, and κ b is absolutely continuous with respect to η b for m-almost every b. Then the Kullback–Leibler divergence between the bind of m with κ and the bind of m with η equals the m-average, over the base point b, of the Kullback–Leibler divergence between κ b and η b.

Formal statement
hypotheses
B Ω :
Type*
MeasurableSpace B
MeasurableSpace Ω
CountableOrCountablyGenerated B Ω
m :
Measure B
IsFiniteMeasure m
κ η :
Kernel B Ω
IsFiniteKernel κ
IsFiniteKernel η
proj :
Ω → B
hproj :
Measurable proj
hgraph :
MeasurableSet {p : B × Ω | p.1 = proj p.2}
hκ_fib :
∀ᵐ b ∂m, (κ b) {ω | proj ω = b}ᶜ = 0
hη_fib :
∀ᵐ b ∂m, (η b) {ω | proj ω = b}ᶜ = 0
hκη :
∀ᵐ b ∂m, κ b ≪ η b
conclusion
_root_.InformationTheory.klDiv (m.bind κ) (m.bind η)
= ∫⁻ b, _root_.InformationTheory.klDiv (κ b) (η b) ∂m
Proof (Lean source)
lemma klDiv_bind_eq_of_base_recording {B Ω : Type*} [MeasurableSpace B] [MeasurableSpace Ω] [CountableOrCountablyGenerated B Ω] (m : Measure B) [IsFiniteMeasure m] (κ η : Kernel B Ω) [IsFiniteKernel κ] [IsFiniteKernel η] (proj : Ω → B) (hproj : Measurable proj) (hgraph : MeasurableSet {p : B × Ω | p.1 = proj p.2}) (hκ_fib : ∀ᵐ b ∂m, (κ b) {ω | proj ω = b}ᶜ = 0) (hη_fib : ∀ᵐ b ∂m, (η b) {ω | proj ω = b}ᶜ = 0) (hκη : ∀ᵐ b ∂m, κ b ≪ η b) : _root_.InformationTheory.klDiv (m.bind κ) (m.bind η) = ∫⁻ b, _root_.InformationTheory.klDiv (κ b) (η b) ∂m := by let g : Ω → B × Ω := fun ω => (proj ω, ω) have hg_emb : MeasurableEmbedding g := by simpa [g] using measurableEmbedding_base_recording (proj := proj) hproj hgraph have hκ_map : (m.bind κ).map g = m ⊗ₘ κ := by simpa [g] using map_bind_eq_compProd_of_base_recording (m := m) (κ := κ) (proj := proj) hproj hκ_fib have hη_map : (m.bind η).map g = m ⊗ₘ η := by simpa [g] using map_bind_eq_compProd_of_base_recording (m := m) (κ := η) (proj := proj) hproj hη_fib haveI hmκ : IsFiniteMeasure (m.bind κ) := by rw [← Measure.snd_compProd (μ := m) (κ := κ)] infer_instance haveI hmη : IsFiniteMeasure (m.bind η) := by rw [← Measure.snd_compProd (μ := m) (κ := η)] infer_instance calc _root_.InformationTheory.klDiv (m.bind κ) (m.bind η) = _root_.InformationTheory.klDiv ((m.bind κ).map g) ((m.bind η).map g) := by exact (klDiv_map_measurableEmbedding (μ := m.bind κ) (ν := m.bind η) (f := g) hg_emb).symm _ = _root_.InformationTheory.klDiv (m ⊗ₘ κ) (m ⊗ₘ η) := by rw [hκ_map, hη_map] _ = ∫⁻ b, _root_.InformationTheory.klDiv (κ b) (η b) ∂m := klDiv_compProd_right_of_forall_ac (μ := m) (κ := κ) (η := η) hκη
Causalean.Mathlib.InformationTheory.Measure.klDiv_bind_eq_of_base_recording · Causalean/Mathlib/InformationTheory/KLBind.lean:198
4 supporting declarations (lemmas, instances)
  • rnDeriv_compProd_right_of_forall_ac lemma — Radon--Nikodym derivative of a shared-base composition product.
    hypotheses
    α :
    Type u_1
    shared
    β :
    Type u_2
    shared
    μ :
    Measure α
    shared
    κ :
    Kernel α β
    shared
    η :
    Kernel α β
    shared
    CountableOrCountablyGenerated α β
    IsFiniteMeasure μ
    IsFiniteKernel κ
    IsFiniteKernel η
    hκη :
    ∀ᵐ a ∂μ, κ a ≪ η a
    conclusion
    (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p : α × β => Kernel.rnDeriv κ η p.1 p.2
    Proof (Lean source)
    lemma rnDeriv_compProd_right_of_forall_ac [CountableOrCountablyGenerated α β] [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p : α × β => Kernel.rnDeriv κ η p.1 p.2 := by have hκ_eq : κ =ᵐ[μ] Kernel.withDensity η (Kernel.rnDeriv κ η) := by filter_upwards [hκη] with a ha exact (Kernel.withDensity_rnDeriv_eq (κ := κ) (η := η) (a := a) ha).symm have hcomp : μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun p : α × β => Kernel.rnDeriv κ η p.1 p.2) := by calc μ ⊗ₘ κ = μ ⊗ₘ Kernel.withDensity η (Kernel.rnDeriv κ η) := Measure.compProd_congr hκ_eq _ = (μ ⊗ₘ η).withDensity (fun p : α × β => Kernel.rnDeriv κ η p.1 p.2) := by rw [Measure.compProd_withDensity] exact Kernel.measurable_rnDeriv κ η rw [hcomp] have hwd := Measure.rnDeriv_withDensity_left_of_absolutelyContinuous (μ := μ ⊗ₘ η) (ν := μ ⊗ₘ η) (f := fun p : α × β => Kernel.rnDeriv κ η p.1 p.2) Measure.AbsolutelyContinuous.rfl (Kernel.measurable_rnDeriv κ η).aemeasurable refine hwd.trans ?_ filter_upwards [Measure.rnDeriv_self (μ ⊗ₘ η)] with p hp rw [hp, mul_one]
    Causalean.Mathlib.InformationTheory.Measure.rnDeriv_compProd_right_of_forall_ac · Causalean/Mathlib/InformationTheory/KLBind.lean:47
  • klDiv_map_measurableEmbedding lemma — KL is invariant under a measurable embedding.
    hypotheses
    α :
    Type u_1
    shared
    γ :
    Type u_3
    shared
    μ :
    Measure α
    shared
    f :
    α → γ
    hf :
    MeasurableEmbedding f
    IsFiniteMeasure μ
    ν :
    Measure α
    IsFiniteMeasure ν
    conclusion
    _root_.InformationTheory.klDiv (μ.map f) (ν.map f) = _root_.InformationTheory.klDiv μ ν
    Proof (Lean source)
    lemma klDiv_map_measurableEmbedding {f : α → γ} (hf : MeasurableEmbedding f) [IsFiniteMeasure μ] {ν : Measure α} [IsFiniteMeasure ν] : _root_.InformationTheory.klDiv (μ.map f) (ν.map f) = _root_.InformationTheory.klDiv μ ν := by classical by_cases hμν : μ ≪ ν · have hmap_ac : μ.map f ≪ ν.map f := hf.absolutelyContinuous_map hμν rw [_root_.InformationTheory.klDiv_eq_lintegral_klFun, _root_.InformationTheory.klDiv_eq_lintegral_klFun, if_pos hmap_ac, if_pos hμν] rw [hf.lintegral_map] refine lintegral_congr_ae ?_ filter_upwards [hf.rnDeriv_map μ ν] with x hx rw [hx] · rw [_root_.InformationTheory.klDiv_of_not_ac hμν] have hmap_not_ac : ¬ μ.map f ≪ ν.map f := by intro hmap exact hμν (Measure.AbsolutelyContinuous.mk fun s hs hs0 => by have hpre : f ⁻¹' (f '' s) = s := by rw [hf.injective.preimage_image] have hs_image : MeasurableSet (f '' s) := hf.measurableSet_image' hs have hν_image : ν.map f (f '' s) = 0 := by rw [hf.map_apply ν (f '' s), hpre] exact hs0 have hμ_image : μ.map f (f '' s) = 0 := hmap hν_image rw [hf.map_apply μ (f '' s), hpre] at hμ_image exact hμ_image) rw [_root_.InformationTheory.klDiv_of_not_ac hmap_not_ac]
    Causalean.Mathlib.InformationTheory.Measure.klDiv_map_measurableEmbedding · Causalean/Mathlib/InformationTheory/KLBind.lean:117
  • measurableEmbedding_base_recording lemma — If a measurable map has a measurable graph, pairing each observation with its map value produces a measurable embedding into the corresponding product space.
    hypotheses
    B Ω :
    Type*
    MeasurableSpace B
    MeasurableSpace Ω
    proj :
    Ω → B
    hproj :
    Measurable proj
    hgraph :
    MeasurableSet {p : B × Ω | p.1 = proj p.2}
    conclusion
    MeasurableEmbedding (fun ω : Ω => (proj ω, ω))
    Proof (Lean source)
    lemma measurableEmbedding_base_recording {B Ω : Type*} [MeasurableSpace B] [MeasurableSpace Ω] (proj : Ω → B) (hproj : Measurable proj) (hgraph : MeasurableSet {p : B × Ω | p.1 = proj p.2}) : MeasurableEmbedding (fun ω : Ω => (proj ω, ω)) := by have hg : Measurable (fun ω : Ω => (proj ω, ω)) := by fun_prop have hRange : range (fun ω : Ω => (proj ω, ω)) = {p : B × Ω | p.1 = proj p.2} := by ext p constructor · rintro ⟨ω, rfl⟩ rfl · intro hp exact ⟨p.2, Prod.ext hp.symm rfl⟩ exact MeasurableEmbedding.of_measurable_inverse hg (by simpa [hRange] using hgraph) measurable_snd (by intro ω; rfl)
    Causalean.Mathlib.InformationTheory.Measure.measurableEmbedding_base_recording · Causalean/Mathlib/InformationTheory/KLBind.lean:148
  • map_bind_eq_compProd_of_base_recording lemma — If a kernel is supported almost everywhere on outputs that record their base coordinate, then mapping its bound measure to the recorded base-output pair gives the corresponding composition-product measure.
    hypotheses
    B Ω :
    Type*
    MeasurableSpace B
    MeasurableSpace Ω
    m :
    Measure B
    SFinite m
    κ :
    Kernel B Ω
    IsSFiniteKernel κ
    proj :
    Ω → B
    hproj :
    Measurable proj
    hκ_fib :
    ∀ᵐ b ∂m, (κ b) {ω | proj ω = b}ᶜ = 0
    conclusion
    (m.bind κ).map (fun ω : Ω => (proj ω, ω)) = m ⊗ₘ κ
    Proof (Lean source)
    lemma map_bind_eq_compProd_of_base_recording {B Ω : Type*} [MeasurableSpace B] [MeasurableSpace Ω] (m : Measure B) [SFinite m] (κ : Kernel B Ω) [IsSFiniteKernel κ] (proj : Ω → B) (hproj : Measurable proj) (hκ_fib : ∀ᵐ b ∂m, (κ b) {ω | proj ω = b}ᶜ = 0) : (m.bind κ).map (fun ω : Ω => (proj ω, ω)) = m ⊗ₘ κ := by let g : Ω → B × Ω := fun ω => (proj ω, ω) have hg : Measurable g := by fun_prop calc (m.bind κ).map (fun ω : Ω => (proj ω, ω)) = m.bind (Kernel.map κ g) := by simpa [g] using Measure.map_comp (μ := m) (κ := κ) (f := g) hg _ = m.bind (Kernel.id ×ₖ κ) := by refine Measure.bind_congr_right ?_ filter_upwards [hκ_fib] with b hκ_fib have hsupp : {ω : Ω | proj ω = b} ∈ ae (κ b) := mem_ae_iff.mpr hκ_fib have h_ae : g =ᵐ[κ b] Prod.mk b := by filter_upwards [hsupp] with ω hω exact Prod.ext hω rfl calc (Kernel.map κ g) b = (κ b).map g := Kernel.map_apply κ hg b _ = (κ b).map (Prod.mk b) := Measure.map_congr h_ae _ = (Kernel.id ×ₖ κ) b := by ext s hs rw [Measure.map_apply measurable_prodMk_left hs, Kernel.id_prod_apply' κ b hs] _ = m ⊗ₘ κ := by simpa using (Measure.compProd_eq_comp_prod m κ).symm
    Causalean.Mathlib.InformationTheory.Measure.map_bind_eq_compProd_of_base_recording · Causalean/Mathlib/InformationTheory/KLBind.lean:168
Product­KLLe­Cam 2 core · 12 supporting This file proves and packages tensorisation tools for Kullback--Leibler divergence over finite product laws. ★ productKL_tensorization

Product KL bounds

This file proves and packages tensorisation tools for Kullback--Leibler divergence over finite product laws. The central proposition ProductKLTensorizationBound records the finite product KL, the finite one-observation KL, and the real-valued inequality KL(μ^n, ν^n) ≤ n * KL(μ,ν) while explicitly retaining the finiteness conditions needed to use ENNReal.toReal soundly.

The main public results are: * productKL_tensorization_of_finite, the finite-branch equality for finite products; * productKL_tensorization, the packaged i.i.d. ProductKLTensorizationBound from one-sample absolute continuity and log-likelihood-ratio integrability; * pi_iid_llr_integrable, the reusable finite-product integrability side condition.

Finite-product absolute continuity is supplied by the imported ProductAbsolutelyContinuous.pi_iid_absolutelyContinuous theorem.

It is a Mathlib-adjacent information-theory layer rather than a causal model construction.

def ProductKLTensorizationBound reviewed
Causalean.Mathlib.InformationTheory

For a measurable observation space, a sample size, and two measures on that space, the product-KL tensorisation bound asserts that the Kullback--Leibler divergence between their n-fold product measures is finite, their one-observation Kullback--Leibler divergence is finite, and the real-valued product divergence is at most n times the real-valued one-observation divergence.

Definition (Lean source)
parameters
α :
Type*
MeasurableSpace α
n :
ℕ
μ ν :
Measure α
def
ProductKLTensorizationBound n μ ν :
Prop
given by
clause 1
_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))
≠ ∞
clause 2
_root_.InformationTheory.klDiv μ ν ≠ ∞
clause 3
(_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal
≤ (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal
Causalean.Mathlib.InformationTheory.ProductKLTensorizationBound · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:330
theorem productKL_tensorization reviewed
Causalean.Mathlib.InformationTheory

For a measurable observation space, a sample size, and two probability measures, if the first measure is absolutely continuous with respect to the second and their log-likelihood ratio is integrable under the first measure, then both the product and one-observation KL divergences are finite, and the real-valued product divergence is at most the sample size times the one-observation divergence.

Formal statement
hypotheses
α :
Type*
MeasurableSpace α
n :
ℕ
μ ν :
Measure α
IsProbabilityMeasure μ
IsProbabilityMeasure ν
hac :
μ ≪ ν
hint :
Integrable (llr μ ν) μ
conclusion
ProductKLTensorizationBound n μ ν
Proof (Lean source)
theorem productKL_tensorization {α : Type*} [MeasurableSpace α] (n : ℕ) (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hint : Integrable (llr μ ν) μ) : ProductKLTensorizationBound n μ ν := by have hπac := pi_iid_absolutelyContinuous μ ν hac have hπint := ProductKL.pi_llr_integrable_iid μ ν hac hint have hleft_ne_top : _root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) ≠ ∞ := _root_.InformationTheory.klDiv_ne_top (hπac n) (hπint n) have hright_kl_ne_top : _root_.InformationTheory.klDiv μ ν ≠ ∞ := _root_.InformationTheory.klDiv_ne_top hac hint exact ⟨hleft_ne_top, hright_kl_ne_top, le_of_eq <| productKL_tensorization_of_finite n μ ν hac hint⟩
Causalean.Mathlib.InformationTheory.productKL_tensorization · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:367 · uses ProductKLTensorizationBound
12 supporting declarations (lemmas, instances)
  • ae_prod_fst_of_ae lemma — A measurable property holding almost everywhere under a measure also holds for the first coordinate almost everywhere under its product with a probability measure.
    hypotheses
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    Measure α
    Measure β
    IsProbabilityMeasure ν
    p :
    α → Prop
    hp_meas :
    MeasurableSet {x | p x}
    hp :
    ∀ᵐ x ∂μ, p x
    conclusion
    ∀ᵐ z ∂μ.prod ν, p z.1
    Proof (Lean source)
    lemma ae_prod_fst_of_ae {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [IsProbabilityMeasure ν] {p : α → Prop} (hp_meas : MeasurableSet {x | p x}) (hp : ∀ᵐ x ∂μ, p x) : ∀ᵐ z ∂μ.prod ν, p z.1 := by have hmap : ∀ᵐ x ∂Measure.map fst (μ.prod ν), p x := by simpa [MeasurePreserving.map_eq (measurePreserving_fst (μ := μ) (ν := ν))] using hp exact (ae_map_iff (measurePreserving_fst (μ := μ) (ν := ν)).aemeasurable hp_meas).mp hmap
    Causalean.Mathlib.InformationTheory.ProductKL.ae_prod_fst_of_ae · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:59
  • ae_prod_snd_of_ae lemma — A measurable property holding almost everywhere under a measure also holds for the second coordinate almost everywhere under its product with a probability measure.
    hypotheses
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    Measure α
    Measure β
    IsProbabilityMeasure μ
    SFinite ν
    p :
    β → Prop
    hp_meas :
    MeasurableSet {y | p y}
    hp :
    ∀ᵐ y ∂ν, p y
    conclusion
    ∀ᵐ z ∂μ.prod ν, p z.2
    Proof (Lean source)
    lemma ae_prod_snd_of_ae {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [IsProbabilityMeasure μ] [SFinite ν] {p : β → Prop} (hp_meas : MeasurableSet {y | p y}) (hp : ∀ᵐ y ∂ν, p y) : ∀ᵐ z ∂μ.prod ν, p z.2 := by have hmap : ∀ᵐ y ∂Measure.map snd (μ.prod ν), p y := by simpa [MeasurePreserving.map_eq (measurePreserving_snd (μ := μ) (ν := ν))] using hp exact (ae_map_iff (measurePreserving_snd (μ := μ) (ν := ν)).aemeasurable hp_meas).mp hmap
    Causalean.Mathlib.InformationTheory.ProductKL.ae_prod_snd_of_ae · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:69
  • llr_prod_ae lemma — When each component law is absolutely continuous with respect to its reference law, the log-likelihood ratio of their product laws is almost surely the sum of the two component log-likelihood ratios.
    hypotheses
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    μ₁ ν₁ :
    Measure α
    μ₂ ν₂ :
    Measure β
    IsProbabilityMeasure μ₁
    SigmaFinite ν₁
    IsProbabilityMeasure μ₂
    SigmaFinite ν₂
    h₁ :
    μ₁ ≪ ν₁
    h₂ :
    μ₂ ≪ ν₂
    conclusion
    llr (μ₁.prod μ₂) (ν₁.prod ν₂)
    =ᵐ[μ₁.prod μ₂] fun z : α × β => llr μ₁ ν₁ z.1 + llr μ₂ ν₂ z.2
    Proof (Lean source)
    lemma llr_prod_ae {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ₁ ν₁ : Measure α) (μ₂ ν₂ : Measure β) [IsProbabilityMeasure μ₁] [SigmaFinite ν₁] [IsProbabilityMeasure μ₂] [SigmaFinite ν₂] (h₁ : μ₁ ≪ ν₁) (h₂ : μ₂ ≪ ν₂) : llr (μ₁.prod μ₂) (ν₁.prod ν₂) =ᵐ[μ₁.prod μ₂] fun z : α × β => llr μ₁ ν₁ z.1 + llr μ₂ ν₂ z.2 := by have hprod : μ₁.prod μ₂ ≪ ν₁.prod ν₂ := h₁.prod h₂ have hrn := hprod.ae_eq (rnDeriv_prod_eq μ₁ ν₁ μ₂ ν₂ h₁ h₂).symm have hpos₁ : ∀ᵐ x ∂μ₁, 0 < μ₁.rnDeriv ν₁ x := Measure.rnDeriv_pos h₁ have hpos₂ : ∀ᵐ y ∂μ₂, 0 < μ₂.rnDeriv ν₂ y := Measure.rnDeriv_pos h₂ have hfin₁ : ∀ᵐ x ∂μ₁, μ₁.rnDeriv ν₁ x ≠ ∞ := Filter.Eventually.filter_mono h₁.ae_le (Measure.rnDeriv_ne_top μ₁ ν₁) have hfin₂ : ∀ᵐ y ∂μ₂, μ₂.rnDeriv ν₂ y ≠ ∞ := Filter.Eventually.filter_mono h₂.ae_le (Measure.rnDeriv_ne_top μ₂ ν₂) have hpos₁p : ∀ᵐ z ∂μ₁.prod μ₂, 0 < μ₁.rnDeriv ν₁ z.1 := ae_prod_fst_of_ae (measurableSet_lt measurable_const (Measure.measurable_rnDeriv μ₁ ν₁)) hpos₁ have hpos₂p : ∀ᵐ z ∂μ₁.prod μ₂, 0 < μ₂.rnDeriv ν₂ z.2 := ae_prod_snd_of_ae (measurableSet_lt measurable_const (Measure.measurable_rnDeriv μ₂ ν₂)) hpos₂ have hfin₁p : ∀ᵐ z ∂μ₁.prod μ₂, μ₁.rnDeriv ν₁ z.1 ≠ ∞ := ae_prod_fst_of_ae (p := fun x => μ₁.rnDeriv ν₁ x ≠ ∞) (by change MeasurableSet ((fun x => μ₁.rnDeriv ν₁ x) ⁻¹' ({∞} : Set ℝ≥0∞))ᶜ exact (Measure.measurable_rnDeriv μ₁ ν₁ (MeasurableSet.singleton (∞ : ℝ≥0∞))).compl) hfin₁ have hfin₂p : ∀ᵐ z ∂μ₁.prod μ₂, μ₂.rnDeriv ν₂ z.2 ≠ ∞ := ae_prod_snd_of_ae (p := fun y => μ₂.rnDeriv ν₂ y ≠ ∞) (by change MeasurableSet ((fun y => μ₂.rnDeriv ν₂ y) ⁻¹' ({∞} : Set ℝ≥0∞))ᶜ exact (Measure.measurable_rnDeriv μ₂ ν₂ (MeasurableSet.singleton (∞ : ℝ≥0∞))).compl) hfin₂ filter_upwards [hrn, hpos₁p, hpos₂p, hfin₁p, hfin₂p] with z hz hposz₁ hposz₂ hfinz₁ hfinz₂ rw [llr_def, llr_def, llr_def] change log (((μ₁.prod μ₂).rnDeriv (ν₁.prod ν₂) z).toReal) = log (μ₁.rnDeriv ν₁ z.1).toReal + log (μ₂.rnDeriv ν₂ z.2).toReal rw [← hz] rw [ENNReal.toReal_mul, Real.log_mul] · exact (ENNReal.toReal_pos hposz₁.ne' hfinz₁).ne' · exact (ENNReal.toReal_pos hposz₂.ne' hfinz₂).ne'
    Causalean.Mathlib.InformationTheory.ProductKL.llr_prod_ae · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:79
  • llr_prod_integrable lemma — Integrable component log-likelihood ratios imply that the log-likelihood ratio of the corresponding product laws is integrable.
    hypotheses
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    μ₁ ν₁ :
    Measure α
    μ₂ ν₂ :
    Measure β
    IsProbabilityMeasure μ₁
    SigmaFinite ν₁
    IsProbabilityMeasure μ₂
    SigmaFinite ν₂
    h₁ :
    μ₁ ≪ ν₁
    h₂ :
    μ₂ ≪ ν₂
    hint₁ :
    Integrable (llr μ₁ ν₁) μ₁
    hint₂ :
    Integrable (llr μ₂ ν₂) μ₂
    conclusion
    Integrable (llr (μ₁.prod μ₂) (ν₁.prod ν₂)) (μ₁.prod μ₂)
    Proof (Lean source)
    lemma llr_prod_integrable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ₁ ν₁ : Measure α) (μ₂ ν₂ : Measure β) [IsProbabilityMeasure μ₁] [SigmaFinite ν₁] [IsProbabilityMeasure μ₂] [SigmaFinite ν₂] (h₁ : μ₁ ≪ ν₁) (h₂ : μ₂ ≪ ν₂) (hint₁ : Integrable (llr μ₁ ν₁) μ₁) (hint₂ : Integrable (llr μ₂ ν₂) μ₂) : Integrable (llr (μ₁.prod μ₂) (ν₁.prod ν₂)) (μ₁.prod μ₂) := by have hllr := llr_prod_ae μ₁ ν₁ μ₂ ν₂ h₁ h₂ have hcomp₁ : Integrable (fun z : α × β => llr μ₁ ν₁ z.1) (μ₁.prod μ₂) := by simpa [Function.comp_def] using ((measurePreserving_fst (μ := μ₁) (ν := μ₂)).integrable_comp (stronglyMeasurable_llr μ₁ ν₁).aestronglyMeasurable).2 hint₁ have hcomp₂ : Integrable (fun z : α × β => llr μ₂ ν₂ z.2) (μ₁.prod μ₂) := by simpa [Function.comp_def] using ((measurePreserving_snd (μ := μ₁) (ν := μ₂)).integrable_comp (stronglyMeasurable_llr μ₂ ν₂).aestronglyMeasurable).2 hint₂ exact (integrable_congr hllr).2 (hcomp₁.add hcomp₂)
    Causalean.Mathlib.InformationTheory.ProductKL.llr_prod_integrable · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:126
  • llr_integrable_of_map_measurableEquiv lemma — Pushing two measures through a measurable relabelling preserves integrability of their log-likelihood ratio, allowing KL side conditions to transfer between equivalent sample spaces.
    hypotheses
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    e :
    α ≃ᵐ β
    μ ν :
    Measure α
    SigmaFinite μ
    SigmaFinite ν
    hμν :
    μ ≪ ν
    hint :
    Integrable (llr (Measure.map e μ) (Measure.map e ν)) (Measure.map e μ)
    conclusion
    Integrable (llr μ ν) μ
    Proof (Lean source)
    lemma llr_integrable_of_map_measurableEquiv {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hint : Integrable (llr (Measure.map e μ) (Measure.map e ν)) (Measure.map e μ)) : Integrable (llr μ ν) μ := by have hcomp : Integrable (fun x : α => llr (Measure.map e μ) (Measure.map e ν) (e x)) μ := (integrable_map_equiv e (llr (Measure.map e μ) (Measure.map e ν))).1 hint have hllr : (fun x : α => llr (Measure.map e μ) (Measure.map e ν) (e x)) =ᵐ[μ] llr μ ν := by have hrn := hμν.ae_eq (e.measurableEmbedding.rnDeriv_map μ ν) filter_upwards [hrn] with x hx rw [llr_def, llr_def] simp [hx] exact (integrable_congr hllr).1 hcomp
    Causalean.Mathlib.InformationTheory.ProductKL.llr_integrable_of_map_measurableEquiv · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:147
  • klDiv_prod_toReal_add lemma — For product probability laws with integrable component log-likelihood ratios, the real-valued KL divergence of the product equals the sum of the component KL divergences.
    hypotheses
    α β :
    Type*
    MeasurableSpace α
    MeasurableSpace β
    μ₁ ν₁ :
    Measure α
    μ₂ ν₂ :
    Measure β
    IsProbabilityMeasure μ₁
    IsProbabilityMeasure ν₁
    IsProbabilityMeasure μ₂
    IsProbabilityMeasure ν₂
    h₁ :
    μ₁ ≪ ν₁
    h₂ :
    μ₂ ≪ ν₂
    hint₁ :
    Integrable (llr μ₁ ν₁) μ₁
    hint₂ :
    Integrable (llr μ₂ ν₂) μ₂
    conclusion
    (klDiv (μ₁.prod μ₂) (ν₁.prod ν₂)).toReal = (klDiv μ₁ ν₁).toReal + (klDiv μ₂ ν₂).toReal
    Proof (Lean source)
    lemma klDiv_prod_toReal_add {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (μ₁ ν₁ : Measure α) (μ₂ ν₂ : Measure β) [IsProbabilityMeasure μ₁] [IsProbabilityMeasure ν₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure ν₂] (h₁ : μ₁ ≪ ν₁) (h₂ : μ₂ ≪ ν₂) (hint₁ : Integrable (llr μ₁ ν₁) μ₁) (hint₂ : Integrable (llr μ₂ ν₂) μ₂) : (klDiv (μ₁.prod μ₂) (ν₁.prod ν₂)).toReal = (klDiv μ₁ ν₁).toReal + (klDiv μ₂ ν₂).toReal := by have hllr := llr_prod_ae μ₁ ν₁ μ₂ ν₂ h₁ h₂ have hcomp₁ : Integrable (fun z : α × β => llr μ₁ ν₁ z.1) (μ₁.prod μ₂) := by simpa [Function.comp_def] using ((measurePreserving_fst (μ := μ₁) (ν := μ₂)).integrable_comp (stronglyMeasurable_llr μ₁ ν₁).aestronglyMeasurable).2 hint₁ have hcomp₂ : Integrable (fun z : α × β => llr μ₂ ν₂ z.2) (μ₁.prod μ₂) := by simpa [Function.comp_def] using ((measurePreserving_snd (μ := μ₁) (ν := μ₂)).integrable_comp (stronglyMeasurable_llr μ₂ ν₂).aestronglyMeasurable).2 hint₂ have hprod_int : Integrable (llr (μ₁.prod μ₂) (ν₁.prod ν₂)) (μ₁.prod μ₂) := by exact (integrable_congr hllr).2 (hcomp₁.add hcomp₂) rw [toReal_klDiv_of_measure_eq (h₁.prod h₂), toReal_klDiv_of_measure_eq h₁, toReal_klDiv_of_measure_eq h₂] · rw [integral_congr_ae hllr] rw [integral_add hcomp₁ hcomp₂] have hfst : ∫ z : α × β, llr μ₁ ν₁ z.1 ∂μ₁.prod μ₂ = ∫ x, llr μ₁ ν₁ x ∂μ₁ := by have hmap := integral_map (μ := μ₁.prod μ₂) (φ := fst) (f := llr μ₁ ν₁) (measurePreserving_fst (μ := μ₁) (ν := μ₂)).aemeasurable (stronglyMeasurable_llr μ₁ ν₁).aestronglyMeasurable rw [(measurePreserving_fst (μ := μ₁) (ν := μ₂)).map_eq] at hmap exact hmap.symm have hsnd : ∫ z : α × β, llr μ₂ ν₂ z.2 ∂μ₁.prod μ₂ = ∫ y, llr μ₂ ν₂ y ∂μ₂ := by have hmap := integral_map (μ := μ₁.prod μ₂) (φ := snd) (f := llr μ₂ ν₂) (measurePreserving_snd (μ := μ₁) (ν := μ₂)).aemeasurable (stronglyMeasurable_llr μ₂ ν₂).aestronglyMeasurable rw [(measurePreserving_snd (μ := μ₁) (ν := μ₂)).map_eq] at hmap exact hmap.symm rw [hfst, hsnd] · simp · simp · simp
    Causalean.Mathlib.InformationTheory.ProductKL.klDiv_prod_toReal_add · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:213
  • productKL_tensorization_toReal_eq lemma — Under absolute-continuity and integrability conditions for every finite product, the real-valued Kullback–Leibler divergence of two n-fold product laws is n times the one-law divergence.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    n :
    ℕ
    μ ν :
    Measure α
    IsProbabilityMeasure μ
    IsProbabilityMeasure ν
    hac :
    μ ≪ ν
    hint :
    Integrable (llr μ ν) μ
    hπac :
    ∀ k : ℕ, Measure.pi (fun _ : Fin k => μ) ≪ Measure.pi (fun _ : Fin k => ν)
    hπint :
    ∀ k : ℕ,
    Integrable (llr (Measure.pi (fun _ : Fin k => μ)) (Measure.pi (fun _ : Fin k => ν))) (Measure.pi (fun _ : Fin k => μ))
    conclusion
    (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal
    = (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal
    Proof (Lean source)
    lemma productKL_tensorization_toReal_eq {α : Type*} [MeasurableSpace α] (n : ℕ) (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hint : Integrable (llr μ ν) μ) (hπac : ∀ k : ℕ, Measure.pi (fun _ : Fin k => μ) ≪ Measure.pi (fun _ : Fin k => ν)) (hπint : ∀ k : ℕ, Integrable (llr (Measure.pi (fun _ : Fin k => μ)) (Measure.pi (fun _ : Fin k => ν))) (Measure.pi (fun _ : Fin k => μ))) : (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal = (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal := by induction n with | zero => rw [Measure.pi_of_empty, Measure.pi_of_empty] simp | succ n ih => let e : ((i : Fin (n + 1)) → α) ≃ᵐ α × ((j : Fin n) → α) := piFinSuccAbove (fun _ : Fin (n + 1) => α) 0 have hmapμ : Measure.map e (Measure.pi (fun _ : Fin (n + 1) => μ)) = μ.prod (Measure.pi (fun _ : Fin n => μ)) := by simpa [e] using (measurePreserving_piFinSuccAbove (μ := fun _ : Fin (n + 1) => μ) (0 : Fin (n + 1))).map_eq have hmapν : Measure.map e (Measure.pi (fun _ : Fin (n + 1) => ν)) = ν.prod (Measure.pi (fun _ : Fin n => ν)) := by simpa [e] using (measurePreserving_piFinSuccAbove (μ := fun _ : Fin (n + 1) => ν) (0 : Fin (n + 1))).map_eq have hrelab := klDiv_toReal_map_measurableEquiv e (Measure.pi (fun _ : Fin (n + 1) => μ)) (Measure.pi (fun _ : Fin (n + 1) => ν)) (hπac (n + 1)) rw [Nat.cast_add_one] change (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin (n + 1) => μ)) (Measure.pi (fun _ : Fin (n + 1) => ν))).toReal = ((n : ℝ) + 1) * (_root_.InformationTheory.klDiv μ ν).toReal calc (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin (n + 1) => μ)) (Measure.pi (fun _ : Fin (n + 1) => ν))).toReal = (_root_.InformationTheory.klDiv (Measure.map e (Measure.pi (fun _ : Fin (n + 1) => μ))) (Measure.map e (Measure.pi (fun _ : Fin (n + 1) => ν)))).toReal := hrelab.symm _ = (_root_.InformationTheory.klDiv (μ.prod (Measure.pi (fun _ : Fin n => μ))) (ν.prod (Measure.pi (fun _ : Fin n => ν)))).toReal := by rw [hmapμ, hmapν] _ = (_root_.InformationTheory.klDiv μ ν).toReal + (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal := by exact klDiv_prod_toReal_add μ ν (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) hac (hπac n) hint (hπint n) _ = ((n : ℝ) + 1) * (_root_.InformationTheory.klDiv μ ν).toReal := by rw [ih] ring
    Causalean.Mathlib.InformationTheory.ProductKL.productKL_tensorization_toReal_eq · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:260
  • productKL_tensorization_of_finite theorem — Finite-branch product-KL tensorisation for i.i.d. finite products.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    n :
    ℕ
    μ ν :
    Measure α
    IsProbabilityMeasure μ
    IsProbabilityMeasure ν
    hac :
    μ ≪ ν
    hint :
    Integrable (llr μ ν) μ
    conclusion
    (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal
    = (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal
    Proof (Lean source)
    theorem productKL_tensorization_of_finite {α : Type*} [MeasurableSpace α] (n : ℕ) (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hac : μ ≪ ν) (hint : Integrable (llr μ ν) μ) : (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal = (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal := ProductKL.productKL_tensorization_toReal_eq n μ ν hac hint (pi_iid_absolutelyContinuous μ ν hac) (ProductKL.pi_llr_integrable_iid μ ν hac hint)
    Causalean.Mathlib.InformationTheory.productKL_tensorization_of_finite · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:350
  • apply theorem — Unpack a supplied product-KL tensorisation bound.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    n :
    ℕ
    μ ν :
    Measure α
    h :
    ProductKLTensorizationBound n μ ν
    conclusion
    (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal
    ≤ (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal
    Proof (Lean source)
    theorem ProductKLTensorizationBound.apply {α : Type*} [MeasurableSpace α] {n : ℕ} {μ ν : Measure α} (h : ProductKLTensorizationBound n μ ν) : (_root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))).toReal ≤ (n : ℝ) * (_root_.InformationTheory.klDiv μ ν).toReal := h.2.2
    Causalean.Mathlib.InformationTheory.ProductKLTensorizationBound.apply · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:389
  • product_ne_top theorem — The product KL divergence in a supplied tensorisation bound is finite.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    n :
    ℕ
    μ ν :
    Measure α
    h :
    ProductKLTensorizationBound n μ ν
    conclusion
    _root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))
    ≠ ∞
    Proof (Lean source)
    theorem ProductKLTensorizationBound.product_ne_top {α : Type*} [MeasurableSpace α] {n : ℕ} {μ ν : Measure α} (h : ProductKLTensorizationBound n μ ν) : _root_.InformationTheory.klDiv (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν)) ≠ ∞ := h.1
    Causalean.Mathlib.InformationTheory.ProductKLTensorizationBound.product_ne_top · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:399
  • one_ne_top theorem — The one-observation KL divergence in a supplied tensorisation bound is finite.
    hypotheses
    α :
    Type*
    MeasurableSpace α
    n :
    ℕ
    μ ν :
    Measure α
    h :
    ProductKLTensorizationBound n μ ν
    conclusion
    _root_.InformationTheory.klDiv μ ν ≠ ∞
    Proof (Lean source)
    theorem ProductKLTensorizationBound.one_ne_top {α : Type*} [MeasurableSpace α] {n : ℕ} {μ ν : Measure α} (h : ProductKLTensorizationBound n μ ν) : _root_.InformationTheory.klDiv μ ν ≠ ∞ := h.2.1
    Causalean.Mathlib.InformationTheory.ProductKLTensorizationBound.one_ne_top · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:408
  • pi_iid_llr_integrable theorem — Public: log-likelihood-ratio integrability for i.i.d. finite products from the one-sample hypotheses μ ≪ ν and Integrable (llr μ ν) μ. Combined with ProductAbsolutelyContinuous.pi_iid_absolutelyContinuous this certifies klDiv (pi μ) (pi ν) ≠ ⊤ (via InformationTheory.klDiv_ne_top).
    hypotheses
    α :
    Type*
    MeasurableSpace α
    μ ν :
    Measure α
    IsProbabilityMeasure μ
    SigmaFinite ν
    hμν :
    μ ≪ ν
    hint :
    Integrable (llr μ ν) μ
    n :
    ℕ
    conclusion
    Integrable (llr (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))) (Measure.pi (fun _ : Fin n => μ))
    Proof (Lean source)
    theorem pi_iid_llr_integrable {α : Type*} [MeasurableSpace α] (μ ν : Measure α) [IsProbabilityMeasure μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hint : Integrable (llr μ ν) μ) (n : ℕ) : Integrable (llr (Measure.pi (fun _ : Fin n => μ)) (Measure.pi (fun _ : Fin n => ν))) (Measure.pi (fun _ : Fin n => μ)) := ProductKL.pi_llr_integrable_iid μ ν hμν hint n
    Causalean.Mathlib.InformationTheory.pi_iid_llr_integrable · Causalean/Mathlib/InformationTheory/ProductKLLeCam.lean:415