Mathlib.InformationTheory
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.
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
⚑ flagged
Causalean.Mathlib.InformationTheory
For a finite alphabet and a real-valued mass function on it, the Shannon entropy in nats is , with the standard zero-continuous convention for the summands.
Definition (Lean source)
theorem entropy_le_log_card reviewed
⚑ flagged
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
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
theorem entropy_const_eq_log_card reviewed
⚑ flagged
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
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
3 supporting declarations (lemmas, instances)
-
entropy_nonneglemma — 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.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 sum_nonneg ?_ intro i _ exact Real.negMulLog_nonneg (h0 i) (h1 i) -
negMulLog_sub_mul_log_lelemma — 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.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']
ConditionalEntropy 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
⚑ flagged
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
β :
Type u_2
p :
α × β → ℝ
y :
β
def
yMarginal p y :
ℝ
given by
∑ x, p (x, y)
def condEntropy reviewed
⚑ flagged
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.
def errorProb reviewed
⚑ flagged
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
β :
Type u_2
p :
α × β → ℝ
decode :
β → α
def
errorProb p decode :
ℝ
given by
by classical exact ∑ xy : α × β, (if xy.1 = decode xy.2 then 0 else p xy)
theorem entropy_le_crossEntropy reviewed
⚑ flagged
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
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
10 supporting declarations (lemmas, instances)
-
yMarginal_deflemma — The β-marginal is the finite sum of joint masses over the α coordinate at the chosen value of β.hypothesesα :sharedType u_1β :sharedType u_2p :α × β → ℝy :βconclusionyMarginal p y = ∑ x, p (x, y)Proof (Lean source)
-
condEntropy_deflemma — Conditional entropy unfolds to total joint entropy minus the entropy of the conditioning marginal.hypothesesα :sharedType u_1β :sharedType u_2p :α × β → ℝconclusionProof (Lean source)
@[simp] lemma condEntropy_def (p : α × β → ℝ) : condEntropy p = entropy p - entropy (yMarginal p) := rfl -
errorProb_deflemma — The decoder error probability unfolds to the sum of the joint masses on incorrect decoding cells.hypothesesα :sharedType u_1β :sharedType u_2p :α × β → ℝdecode :β → αconclusionerrorProb 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 -
negMulLog_add_mul_log_lelemma — 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.hypothesesx g :ℝhx :0 ≤ xhg :0 ≤ ghac :x ≠ 0 → 0 < gProof (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'] -
yMarginal_sumlemma — The β-marginal of a pmf is itself a pmf summing to one: if ∑ xy, p xy = 1 then ∑ y, yMarginal p y = 1.hypothesesα :sharedType u_1β :sharedType u_2α × β → ℝhsum :∑ xy : α × β, p xy = 1conclusion∑ y, yMarginal p y = 1Proof (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 -
yMarginal_nonneglemma — The β-marginal of a nonnegative mass function is nonnegative.hypothesesα :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xyy :βconclusion0 ≤ yMarginal p yProof (Lean source)
lemma yMarginal_nonneg {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (y : β) : 0 ≤ yMarginal p y := by rw [yMarginal_def] exact sum_nonneg (fun x _ => hp0 (x, y)) -
le_yMarginallemma — A joint mass is dominated by its β-marginal: p (x, y) ≤ yMarginal p y for nonnegative p.hypothesesα :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xyx :αy :βconclusionp (x, y) ≤ yMarginal p yProof (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) -
errorProb_nonneglemma — The error probability is nonnegative.hypothesesα :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xydecode :β → αconclusion0 ≤ errorProb p decodeProof (Lean source)
lemma errorProb_nonneg {p : α × β → ℝ} (hp0 : ∀ xy, 0 ≤ p xy) (decode : β → α) : 0 ≤ errorProb p decode := by rw [errorProb_def] refine sum_nonneg ?_ intro xy _ split_ifs · exact le_refl 0 · exact hp0 xy -
errorProb_le_onelemma — The error probability is at most one (it is a sub-sum of the total mass = 1).hypothesesα :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xyhsum :∑ xy : α × β, p xy = 1decode :β → αconclusionerrorProb p decode ≤ 1Proof (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) -
correctMass_eqlemma — 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α :sharedType u_1β :sharedType u_2α × β → ℝhsum :∑ xy : α × β, p xy = 1decode :β → αconclusion(∑ xy : α × β, (if xy.1 = decode xy.2 then p xy else 0)) = 1 - errorProb p decodeProof (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]
CommonStatisticBernoulli 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
⚑ flagged
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
def
given by
clause 1
toFun r := bernoulliLaw (p r)
clause 2
measurable' := by unfold bernoulliLaw fun_prop
def statisticSuccessMeasure reviewed
⚑ flagged
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 . 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)
def statisticSuccessParameter reviewed
⚑ flagged
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
def
statisticSuccessParameter nu p stat :
ℝ → ℝ
given by
fun r => ((statisticSuccessMeasure nu p stat).rnDeriv (Measure.map stat nu) r).toReal
def clippedStatisticSuccessParameter reviewed
⚑ flagged
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 and above at .
Definition (Lean source)
parameters
def
clippedStatisticSuccessParameter nu p stat :
ℝ → ℝ
given by
lemma statisticBernoulliOutcome_klDiv_le_of_localized_success_bound reviewed
⚑ flagged
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*
nu nu' :
p p' :
A → ℝ
stat :
A → ℝ
hp :
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 :
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 hD hE hdiff
14 supporting declarations (lemmas, instances)
-
one_add_mul_one_sub_mem_Icctheorem — A Bernoulli parameter in the middle half of the unit interval has variance between zero and one quarter, so adding unit noise gives variance between one and five quarters.hypothesesp :ℝhp :p ∈ Icc (1 / 4 : ℝ) (3 / 4 : ℝ)conclusion1 + p * (1 - p) ∈ Icc (1 : ℝ) (5 / 4 : ℝ)Proof (Lean source)
theorem one_add_mul_one_sub_mem_Icc {p : ℝ} (hp : p ∈ Icc (1 / 4 : ℝ) (3 / 4 : ℝ)) : 1 + p * (1 - p) ∈ Icc (1 : ℝ) (5 / 4 : ℝ) := by constructor · have hp0 : 0 ≤ p := by linarith [hp.1] have hp1 : p ≤ 1 := by linarith [hp.2] have hprod : 0 ≤ p * (1 - p) := mul_nonneg hp0 (sub_nonneg.mpr hp1) linarith · nlinarith [sq_nonneg (p - 1 / 2)] -
commonStatisticBernoulliKernel_isMarkovKernellemma — Pointwise unit-interval parameters make the common-statistic Bernoulli kernel Markov.hypothesesconclusionProof (Lean source)
lemma commonStatisticBernoulliKernel_isMarkovKernel {S : Type*} [MeasurableSpace S] (p : S → ℝ) (hp : Measurable p) (h0 : ∀ r, 0 ≤ p r) (h1 : ∀ r, p r ≤ 1) : IsMarkovKernel (commonStatisticBernoulliKernel p hp) := by constructor intro r exact bernoulliLaw_isProbabilityMeasure (h0 r) (h1 r) -
commonStatisticBernoulli_klDiv_le_of_localized_parameterlemma — A common statistic with conditionally Bernoulli outcomes has KL bounded by the squared change in its success parameter, integrated only over the statistic region where that parameter can change. This is the generic disintegration step used by the signed hard-cell comparison.hypothesesm :p q :ℝ → ℝhp :hq :hp0 :∀ r, 1 / 4 ≤ p rhp1 :∀ r, p r ≤ 3 / 4hq0 :∀ r, 1 / 4 ≤ q rhq1 :∀ r, q r ≤ 3 / 4D :ℝhD :0 ≤ DE :Set ℝhE :hdiff :∀ᵐ r ∂m, |p r - q r| ≤ E.indicator (fun _ => D) rconclusionklDiv (Measure.compProd m (commonStatisticBernoulliKernel p hp)) (Measure.compProd m (commonStatisticBernoulliKernel q hq))≤ ofReal (4 * D ^ 2) * m EProof (Lean source)
lemma commonStatisticBernoulli_klDiv_le_of_localized_parameter (m : Measure ℝ) [IsFiniteMeasure m] (p q : ℝ → ℝ) (hp : Measurable p) (hq : Measurable q) (hp0 : ∀ r, 1 / 4 ≤ p r) (hp1 : ∀ r, p r ≤ 3 / 4) (hq0 : ∀ r, 1 / 4 ≤ q r) (hq1 : ∀ r, q r ≤ 3 / 4) {D : ℝ} (hD : 0 ≤ D) {E : Set ℝ} (hE : MeasurableSet E) (hdiff : ∀ᵐ r ∂m, |p r - q r| ≤ E.indicator (fun _ => D) r) : klDiv (Measure.compProd m (commonStatisticBernoulliKernel p hp)) (Measure.compProd m (commonStatisticBernoulliKernel q hq)) ≤ ofReal (4 * D ^ 2) * m E := by let k : Kernel ℝ ℝ := commonStatisticBernoulliKernel p hp let k' : Kernel ℝ ℝ := commonStatisticBernoulliKernel q hq letI : IsMarkovKernel k := commonStatisticBernoulliKernel_isMarkovKernel p hp (fun r => by linarith [hp0 r]) (fun r => by linarith [hp1 r]) letI : IsMarkovKernel k' := commonStatisticBernoulliKernel_isMarkovKernel q hq (fun r => by linarith [hq0 r]) (fun r => by linarith [hq1 r]) rw [klDiv_compProd_right_of_forall_ac] · calc (∫⁻ r, klDiv (k r) (k' r) ∂m) ≤ ∫⁻ r, E.indicator (fun _ => ofReal (4 * D ^ 2)) r ∂m := by apply lintegral_mono_ae filter_upwards [hdiff] with r hr have hkl := bernoulliLaw_klDiv_le_four_sq_sub (hp0 r) (hp1 r) (hq0 r) (hq1 r) change klDiv (k r) (k' r) ≤ _ at hkl by_cases hrE : r ∈ E · rw [Set.indicator_of_mem hrE] exact hkl.trans (ENNReal.ofReal_le_ofReal (by have habs : |p r - q r| ≤ D := by simpa [hrE] using hr have hsq := (sq_le_sq₀ (abs_nonneg (p r - q r)) hD).2 habs rw [← sq_abs (p r - q r)] nlinarith)) · rw [Set.indicator_of_notMem hrE] have hpq : p r = q r := by have hz : |p r - q r| ≤ 0 := by simpa [hrE] using hr exact sub_eq_zero.mp (abs_eq_zero.mp (le_antisymm hz (abs_nonneg _))) have hkk : k r = k' r := by ext A hA simp [k, k', commonStatisticBernoulliKernel, hpq] rw [hkk, InformationTheory.klDiv_self] _ = ∫⁻ _r in E, ofReal (4 * D ^ 2) ∂m := lintegral_indicator hE _ _ = ofReal (4 * D ^ 2) * m E := setLIntegral_const E (ofReal (4 * D ^ 2)) · filter_upwards with r have hkl := bernoulliLaw_klDiv_le_four_sq_sub (hp0 r) (hp1 r) (hq0 r) (hq1 r) have hfinite : klDiv (k r) (k' r) ≠ ⊤ := by change klDiv (k r) (k' r) ≤ _ at hkl exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top hkl exact (InformationTheory.klDiv_ne_top_iff.mp hfinite).1 -
commonStatisticBernoulliOutcome_klDiv_le_of_localized_parameterlemma — Swapping a common statistic behind its Bernoulli outcome preserves the localized KL estimate, giving the (outcome, statistic) coordinate order used by signed observations.hypothesesm :p q :ℝ → ℝhp :hq :hp0 :∀ r, 1 / 4 ≤ p rhp1 :∀ r, p r ≤ 3 / 4hq0 :∀ r, 1 / 4 ≤ q rhq1 :∀ r, q r ≤ 3 / 4D :ℝhD :0 ≤ DE :Set ℝhE :hdiff :∀ᵐ r ∂m, |p r - q r| ≤ E.indicator (fun _ => D) rconclusionklDiv (Measure.map swap (Measure.compProd m (commonStatisticBernoulliKernel p hp))) (Measure.map swap (Measure.compProd m (commonStatisticBernoulliKernel q hq)))≤ ofReal (4 * D ^ 2) * m EProof (Lean source)
lemma commonStatisticBernoulliOutcome_klDiv_le_of_localized_parameter (m : Measure ℝ) [IsFiniteMeasure m] (p q : ℝ → ℝ) (hp : Measurable p) (hq : Measurable q) (hp0 : ∀ r, 1 / 4 ≤ p r) (hp1 : ∀ r, p r ≤ 3 / 4) (hq0 : ∀ r, 1 / 4 ≤ q r) (hq1 : ∀ r, q r ≤ 3 / 4) {D : ℝ} (hD : 0 ≤ D) {E : Set ℝ} (hE : MeasurableSet E) (hdiff : ∀ᵐ r ∂m, |p r - q r| ≤ E.indicator (fun _ => D) r) : klDiv (Measure.map Prod.swap (Measure.compProd m (commonStatisticBernoulliKernel p hp))) (Measure.map Prod.swap (Measure.compProd m (commonStatisticBernoulliKernel q hq))) ≤ ofReal (4 * D ^ 2) * m E := by letI : IsMarkovKernel (commonStatisticBernoulliKernel p hp) := commonStatisticBernoulliKernel_isMarkovKernel p hp (fun r => by linarith [hp0 r]) (fun r => by linarith [hp1 r]) letI : IsMarkovKernel (commonStatisticBernoulliKernel q hq) := commonStatisticBernoulliKernel_isMarkovKernel q hq (fun r => by linarith [hq0 r]) (fun r => by linarith [hq1 r]) rw [show (Prod.swap : ℝ × ℝ → ℝ × ℝ) = ⇑(MeasurableEquiv.prodComm (α := ℝ) (β := ℝ)) by rfl] rw [klDiv_map_measurableEmbedding (MeasurableEquiv.prodComm (α := ℝ) (β := ℝ)).measurableEmbedding] exact commonStatisticBernoulli_klDiv_le_of_localized_parameter m p q hp hq hp0 hp1 hq0 hq1 hD hE hdiff -
statisticSuccessMeasure_absolutelyContinuouslemma — The success-weighted statistic law is dominated by the statistic marginal when the pointwise success probability is at most one.hypothesesconclusionstatisticSuccessMeasure nu p stat ≪ Measure.map stat nuProof (Lean source)
lemma statisticSuccessMeasure_absolutelyContinuous {A : Type*} [MeasurableSpace A] (nu : Measure A) [IsFiniteMeasure nu] (p : A → ℝ) (stat : A → ℝ) (hstat : Measurable stat) (hp1 : ∀ x, p x ≤ 1) : statisticSuccessMeasure nu p stat ≪ Measure.map stat nu := by apply Measure.absolutelyContinuous_of_le apply Measure.map_mono · calc nu.withDensity (fun x => ofReal (p x)) ≤ nu.withDensity 1 := by apply withDensity_mono filter_upwards with x simpa using ENNReal.ofReal_le_one.mpr (hp1 x) _ = nu := withDensity_one · exact hstat -
statisticSuccessParameter_setIntegrallemma — Set integrals of the conditional parameter recover success-weighted integrals on statistic preimages.hypothesesA :Type*nu :p :A → ℝstat :A → ℝhp :hstat :Measurable stathp0 :∀ x, 0 ≤ p xhp1 :∀ x, p x ≤ 1B :Set ℝhB :conclusion(∫ r in B, statisticSuccessParameter nu p stat r ∂(Measure.map stat nu))= ∫ x in {x | stat x ∈ B}, p x ∂nuProof (Lean source)
lemma statisticSuccessParameter_setIntegral {A : Type*} [MeasurableSpace A] (nu : Measure A) [IsFiniteMeasure nu] (p : A → ℝ) (stat : A → ℝ) (hp : Measurable p) (hstat : Measurable stat) (hp0 : ∀ x, 0 ≤ p x) (hp1 : ∀ x, p x ≤ 1) (B : Set ℝ) (hB : MeasurableSet B) : (∫ r in B, statisticSuccessParameter nu p stat r ∂(Measure.map stat nu)) = ∫ x in {x | stat x ∈ B}, p x ∂nu := by let m : Measure ℝ := Measure.map stat nu let s : Measure ℝ := statisticSuccessMeasure nu p stat have hle : s ≤ m := by dsimp [s, m, statisticSuccessMeasure] apply Measure.map_mono · calc nu.withDensity (fun x => ofReal (p x)) ≤ nu.withDensity 1 := by apply withDensity_mono filter_upwards with x simpa using ENNReal.ofReal_le_one.mpr (hp1 x) _ = nu := withDensity_one · exact hstat have hac : s ≪ m := Measure.absolutelyContinuous_of_le hle letI : IsFiniteMeasure m := Measure.isFiniteMeasure_map nu stat letI : IsFiniteMeasure s := isFiniteMeasure_of_le m hle have hleft := Measure.setIntegral_toReal_rnDeriv hac B have hsB : s B = ofReal (∫ x in {x | stat x ∈ B}, p x ∂nu) := by change (Measure.map stat (nu.withDensity fun x => ofReal (p x))) B = _ rw [Measure.map_apply hstat hB, withDensity_apply _ (hB.preimage hstat)] rw [← ofReal_integral_eq_lintegral_ofReal] · rfl · apply Measure.integrableOn_of_bounded (measure_ne_top _ _) hp.aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (hp0 x)] exact hp1 x · exact Filter.Eventually.of_forall hp0 change (∫ r in B, ((s.rnDeriv m) r).toReal ∂m) = _ rw [hleft, Measure.real_def, hsB, ENNReal.toReal_ofReal] exact integral_nonneg_of_ae (Filter.Eventually.of_forall hp0) -
statisticSuccessParameter_mem_Icc_aelemma — Middle-half pointwise bounds pass to the conditional statistic parameter almost everywhere.hypothesesA :Type*nu :p :A → ℝstat :A → ℝhp :hstat :Measurable stathp0 :∀ x, 1 / 4 ≤ p xhp1 :∀ x, p x ≤ 3 / 4conclusion∀ᵐ r ∂(Measure.map stat nu), statisticSuccessParameter nu p stat r ∈ Icc (1 / 4 : ℝ) (3 / 4 : ℝ)Proof (Lean source)
lemma statisticSuccessParameter_mem_Icc_ae {A : Type*} [MeasurableSpace A] (nu : Measure A) [IsFiniteMeasure nu] (p : A → ℝ) (stat : A → ℝ) (hp : Measurable p) (hstat : Measurable stat) (hp0 : ∀ x, 1 / 4 ≤ p x) (hp1 : ∀ x, p x ≤ 3 / 4) : ∀ᵐ r ∂(Measure.map stat nu), statisticSuccessParameter nu p stat r ∈ Icc (1 / 4 : ℝ) (3 / 4 : ℝ) := by let m : Measure ℝ := Measure.map stat nu let g : ℝ → ℝ := statisticSuccessParameter nu p stat letI : IsFiniteMeasure m := Measure.isFiniteMeasure_map nu stat let s : Measure ℝ := statisticSuccessMeasure nu p stat have hsle : s ≤ m := by dsimp [s, m, statisticSuccessMeasure] apply Measure.map_mono · calc nu.withDensity (fun x => ofReal (p x)) ≤ nu.withDensity 1 := by apply withDensity_mono filter_upwards with x simpa using ENNReal.ofReal_le_one.mpr (by linarith [hp1 x]) _ = nu := withDensity_one · exact hstat letI : IsFiniteMeasure s := isFiniteMeasure_of_le m hsle have hg : Integrable g m := by dsimp [g, statisticSuccessParameter, m] exact Measure.integrable_toReal_rnDeriv have hcLo : Integrable (fun _ : ℝ => (1 / 4 : ℝ)) m := integrable_const _ have hcHi : Integrable (fun _ : ℝ => (3 / 4 : ℝ)) m := integrable_const _ have hlo : (fun _ : ℝ => (1 / 4 : ℝ)) ≤ᵐ[m] g := by apply ae_le_of_forall_setIntegral_le hcLo hg intro B hB _ rw [statisticSuccessParameter_setIntegral nu p stat hp hstat (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) B hB] rw [integral_const] change (m.restrict B).real univ * (1 / 4 : ℝ) ≤ _ rw [Measure.real_def, Measure.restrict_apply_univ] have hmap : m B = nu {x | stat x ∈ B} := by rw [Measure.map_apply hstat hB] rfl rw [hmap] have hmono : (∫ x in {x | stat x ∈ B}, (1 / 4 : ℝ) ∂nu) ≤ ∫ x in {x | stat x ∈ B}, p x ∂nu := by apply integral_mono_ae · exact integrableOn_const · apply Measure.integrableOn_of_bounded (M := 1) (measure_ne_top _ _) hp.aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [hp0 x], by linarith [hp1 x]⟩ · exact ae_restrict_of_forall_mem (hB.preimage hstat) (fun x _ => hp0 x) simpa [Measure.real_def] using hmono have hhi : g ≤ᵐ[m] (fun _ : ℝ => (3 / 4 : ℝ)) := by apply ae_le_of_forall_setIntegral_le hg hcHi intro B hB _ rw [statisticSuccessParameter_setIntegral nu p stat hp hstat (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) B hB] rw [integral_const] change _ ≤ (m.restrict B).real univ * (3 / 4 : ℝ) rw [Measure.real_def, Measure.restrict_apply_univ] have hmap : m B = nu {x | stat x ∈ B} := by rw [Measure.map_apply hstat hB] rfl rw [hmap] have hmono : (∫ x in {x | stat x ∈ B}, p x ∂nu) ≤ ∫ x in {x | stat x ∈ B}, (3 / 4 : ℝ) ∂nu := by apply integral_mono_ae · apply Measure.integrableOn_of_bounded (M := 1) (measure_ne_top _ _) hp.aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [hp0 x], by linarith [hp1 x]⟩ · exact integrableOn_const · exact ae_restrict_of_forall_mem (hB.preimage hstat) (fun x _ => hp1 x) simpa [Measure.real_def] using hmono filter_upwards [hlo, hhi] with r hr0 hr1 exact ⟨hr0, hr1⟩ -
clippedStatisticSuccessParameter_measurablelemmahypothesesconclusionMeasurable (clippedStatisticSuccessParameter nu p stat)Proof (Lean source)
@[fun_prop] lemma clippedStatisticSuccessParameter_measurable {A : Type*} [MeasurableSpace A] (nu : Measure A) (p : A → ℝ) (stat : A → ℝ) : Measurable (clippedStatisticSuccessParameter nu p stat) := by unfold clippedStatisticSuccessParameter statisticSuccessParameter fun_prop -
clippedStatisticSuccessParameter_mem_IcclemmahypothesesconclusionclippedStatisticSuccessParameter nu p stat r ∈ Icc (1 / 4 : ℝ) (3 / 4 : ℝ)Proof (Lean source)
lemma clippedStatisticSuccessParameter_mem_Icc {A : Type*} [MeasurableSpace A] (nu : Measure A) (p : A → ℝ) (stat : A → ℝ) (r : ℝ) : clippedStatisticSuccessParameter nu p stat r ∈ Icc (1 / 4 : ℝ) (3 / 4 : ℝ) := by unfold clippedStatisticSuccessParameter constructor <;> simp <;> norm_num -
clippedStatisticSuccessParameter_ae_eqlemmahypothesesA :Type*nu :p :A → ℝstat :A → ℝhp :hstat :Measurable stathp0 :∀ x, 1 / 4 ≤ p xhp1 :∀ x, p x ≤ 3 / 4conclusionclippedStatisticSuccessParameter nu p stat=ᵐ[Measure.map stat nu] statisticSuccessParameter nu p statProof (Lean source)
lemma clippedStatisticSuccessParameter_ae_eq {A : Type*} [MeasurableSpace A] (nu : Measure A) [IsFiniteMeasure nu] (p : A → ℝ) (stat : A → ℝ) (hp : Measurable p) (hstat : Measurable stat) (hp0 : ∀ x, 1 / 4 ≤ p x) (hp1 : ∀ x, p x ≤ 3 / 4) : clippedStatisticSuccessParameter nu p stat =ᵐ[Measure.map stat nu] statisticSuccessParameter nu p stat := by filter_upwards [statisticSuccessParameter_mem_Icc_ae nu p stat hp hstat hp0 hp1] with r hr unfold clippedStatisticSuccessParameter rw [min_eq_right hr.2, max_eq_right hr.1] -
commonStatisticBernoulliKernel_setLIntegral_eqlemma — Integrating Bernoulli kernels over two base sets gives the same outcome measure when the base masses and success-weighted masses agree.hypothesesA B :nu :nu' :Measure BIsFiniteMeasure nu'p :A → ℝp' :B → ℝhp :hp' :Measurable p'hp0 :∀ x, 0 ≤ p xhp1 :∀ x, p x ≤ 1hp0' :∀ x, 0 ≤ p' xhp1' :∀ x, p' x ≤ 1D :Set AD' :Set Bhmass :nu D = nu' D'hmean :∫ x in D, p x ∂nu = ∫ x in D', p' x ∂nu'E :Set ℝconclusion(∫⁻ x in D, commonStatisticBernoulliKernel p hp x E ∂nu)= ∫⁻ x in D', commonStatisticBernoulliKernel p' hp' x E ∂nu'Proof (Lean source)
lemma commonStatisticBernoulliKernel_setLIntegral_eq {A B : Type*} [MeasurableSpace A] [MeasurableSpace B] (nu : Measure A) [IsFiniteMeasure nu] (nu' : Measure B) [IsFiniteMeasure nu'] (p : A → ℝ) (p' : B → ℝ) (hp : Measurable p) (hp' : Measurable p') (hp0 : ∀ x, 0 ≤ p x) (hp1 : ∀ x, p x ≤ 1) (hp0' : ∀ x, 0 ≤ p' x) (hp1' : ∀ x, p' x ≤ 1) {D : Set A} {D' : Set B} (hmass : nu D = nu' D') (hmean : ∫ x in D, p x ∂nu = ∫ x in D', p' x ∂nu') (E : Set ℝ) : (∫⁻ x in D, commonStatisticBernoulliKernel p hp x E ∂nu) = ∫⁻ x in D', commonStatisticBernoulliKernel p' hp' x E ∂nu' := by have hpInt : IntegrableOn p D nu := by apply Measure.integrableOn_of_bounded (M := 1) (measure_ne_top nu D) hp.aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (hp0 x)] exact hp1 x have hpInt' : IntegrableOn p' D' nu' := by apply Measure.integrableOn_of_bounded (M := 1) (measure_ne_top nu' D') hp'.aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (hp0' x)] exact hp1' x have hqInt : IntegrableOn (fun x => 1 - p x) D nu := (integrableOn_const (s := D) (C := (1 : ℝ))).sub hpInt have hqInt' : IntegrableOn (fun x => 1 - p' x) D' nu' := (integrableOn_const (s := D') (C := (1 : ℝ))).sub hpInt' have hpL : (∫⁻ x in D, ofReal (p x) ∂nu) = ∫⁻ x in D', ofReal (p' x) ∂nu' := by rw [← ofReal_integral_eq_lintegral_ofReal hpInt (Filter.Eventually.of_forall hp0), ← ofReal_integral_eq_lintegral_ofReal hpInt' (Filter.Eventually.of_forall hp0'), hmean] have hqmean : ∫ x in D, (1 - p x) ∂nu = ∫ x in D', (1 - p' x) ∂nu' := by rw [integral_sub (integrableOn_const (s := D) (C := (1 : ℝ))) hpInt, integral_sub (integrableOn_const (s := D') (C := (1 : ℝ))) hpInt'] simp only [integral_const, Measure.real_def] rw [Measure.restrict_apply_univ, Measure.restrict_apply_univ, hmass, hmean] have hqL : (∫⁻ x in D, ofReal (1 - p x) ∂nu) = ∫⁻ x in D', ofReal (1 - p' x) ∂nu' := by rw [← ofReal_integral_eq_lintegral_ofReal hqInt (Filter.Eventually.of_forall fun x => sub_nonneg.mpr (hp1 x)), ← ofReal_integral_eq_lintegral_ofReal hqInt' (Filter.Eventually.of_forall fun x => sub_nonneg.mpr (hp1' x)), hqmean] simp only [commonStatisticBernoulliKernel, Kernel.coe_mk, bernoulliLaw, Measure.add_apply, Measure.smul_apply, smul_eq_mul] change (∫⁻ x, ofReal (p x) * Measure.dirac (1 : ℝ) E + ofReal (1 - p x) * Measure.dirac (0 : ℝ) E ∂(nu.restrict D)) = ∫⁻ x, ofReal (p' x) * Measure.dirac (1 : ℝ) E + ofReal (1 - p' x) * Measure.dirac (0 : ℝ) E ∂(nu'.restrict D') rw [lintegral_add_left (by fun_prop) _, lintegral_add_left (by fun_prop) _] simp_rw [mul_comm (ofReal (p _)), mul_comm (ofReal (1 - p _)), mul_comm (ofReal (p' _)), mul_comm (ofReal (1 - p' _))] rw [lintegral_const_mul _ (by fun_prop), lintegral_const_mul _ (by fun_prop), lintegral_const_mul _ (by fun_prop), lintegral_const_mul _ (by fun_prop), hpL, hqL] -
statisticBernoulliOutcomeLaw_eq_map_swap_compProdlemma — Compressing the base coordinate to a statistic turns a Bernoulli mixture into a Bernoulli composition product over the statistic marginal.hypothesesA :Type*nu :p :A → ℝstat :A → ℝhp :hstat :Measurable stathp0 :∀ x, 1 / 4 ≤ p xhp1 :∀ x, p x ≤ 3 / 4conclusionMeasure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp))= Measure.map swap (Measure.compProd (Measure.map stat nu) (commonStatisticBernoulliKernel (clippedStatisticSuccessParameter nu p stat) (clippedStatisticSuccessParameter_measurable nu p stat)))Proof (Lean source)
lemma statisticBernoulliOutcomeLaw_eq_map_swap_compProd {A : Type*} [MeasurableSpace A] (nu : Measure A) [IsFiniteMeasure nu] (p : A → ℝ) (stat : A → ℝ) (hp : Measurable p) (hstat : Measurable stat) (hp0 : ∀ x, 1 / 4 ≤ p x) (hp1 : ∀ x, p x ≤ 3 / 4) : Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp)) = Measure.map swap (Measure.compProd (Measure.map stat nu) (commonStatisticBernoulliKernel (clippedStatisticSuccessParameter nu p stat) (clippedStatisticSuccessParameter_measurable nu p stat))) := by let m : Measure ℝ := Measure.map stat nu let g : ℝ → ℝ := clippedStatisticSuccessParameter nu p stat let hg : Measurable g := clippedStatisticSuccessParameter_measurable nu p stat letI : IsMarkovKernel (commonStatisticBernoulliKernel p hp) := commonStatisticBernoulliKernel_isMarkovKernel p hp (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) letI : IsFiniteMeasure m := Measure.isFiniteMeasure_map nu stat letI : IsMarkovKernel (commonStatisticBernoulliKernel g hg) := commonStatisticBernoulliKernel_isMarkovKernel g hg (fun r => by dsimp [g]; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu p stat r).1]) (fun r => by dsimp [g]; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu p stat r).2]) apply Measure.ext_prod intro E B hE hB have hleft : (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp))) (E ×ˢ B) = ∫⁻ x in {x | stat x ∈ B}, commonStatisticBernoulliKernel p hp x E ∂nu := by rw [Measure.map_apply (by fun_prop) (hE.prod hB), Measure.compProd_apply] · change _ = ∫⁻ x in stat ⁻¹' B, commonStatisticBernoulliKernel p hp x E ∂nu rw [← lintegral_indicator (hB.preimage hstat)] apply lintegral_congr intro x by_cases hx : stat x ∈ B · have hpre : Prod.mk x ⁻¹' ((fun z : A × ℝ => (z.2, stat z.1)) ⁻¹' (E ×ˢ B)) = E := by ext y simp [hx] have hx' : x ∈ stat ⁻¹' B := hx rw [hpre, Set.indicator_of_mem hx'] · have hpre : Prod.mk x ⁻¹' ((fun z : A × ℝ => (z.2, stat z.1)) ⁻¹' (E ×ˢ B)) = ∅ := by ext y simp [hx] have hx' : x ∉ stat ⁻¹' B := hx rw [hpre, measure_empty, Set.indicator_of_notMem hx'] · exact (hE.prod hB).preimage (by fun_prop) rw [hleft] have hright : (Measure.map swap (Measure.compProd m (commonStatisticBernoulliKernel g hg))) (E ×ˢ B) = ∫⁻ r in B, commonStatisticBernoulliKernel g hg r E ∂m := by rw [Measure.map_apply measurable_swap (hE.prod hB), Measure.compProd_apply] · rw [← lintegral_indicator hB] congr 1 funext r by_cases hr : r ∈ B <;> simp [hr] · exact (hE.prod hB).preimage measurable_swap rw [hright] apply commonStatisticBernoulliKernel_setLIntegral_eq nu m p g hp hg (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) (fun r => by dsimp [g]; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu p stat r).1]) (fun r => by dsimp [g]; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu p stat r).2]) · rw [Measure.map_apply hstat hB] rfl · have heq := clippedStatisticSuccessParameter_ae_eq nu p stat hp hstat hp0 hp1 rw [integral_congr_ae (ae_restrict_of_ae heq)] exact (statisticSuccessParameter_setIntegral nu p stat hp hstat (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) B hB).symm -
clippedStatisticSuccessParameter_abs_sub_le_aelemma — A localized setwise bound on success-weighted statistic masses yields the corresponding almost-everywhere bound on conditional Bernoulli parameters.hypothesesA :Type*nu nu' :p p' :A → ℝstat :A → ℝhp :hp' :Measurable p'hstat :Measurable stathp0 :∀ x, 1 / 4 ≤ p xhp1 :∀ x, p x ≤ 3 / 4hp0' :∀ x, 1 / 4 ≤ p' xhp1' :∀ x, p' x ≤ 3 / 4hmap :Measure.map stat nu = Measure.map stat nu'D :ℝhD :0 ≤ DE :Set ℝhE :conclusion∀ᵐ r ∂(Measure.map stat nu), |clippedStatisticSuccessParameter nu p stat r- clippedStatisticSuccessParameter nu' p' stat r|≤ E.indicator (fun _ => D) rProof (Lean source)
lemma clippedStatisticSuccessParameter_abs_sub_le_ae {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) : ∀ᵐ r ∂(Measure.map stat nu), |clippedStatisticSuccessParameter nu p stat r - clippedStatisticSuccessParameter nu' p' stat r| ≤ E.indicator (fun _ => D) r := by let m : Measure ℝ := Measure.map stat nu let g : ℝ → ℝ := statisticSuccessParameter nu p stat let g' : ℝ → ℝ := statisticSuccessParameter nu' p' stat letI : IsFiniteMeasure m := Measure.isFiniteMeasure_map nu stat let s : Measure ℝ := statisticSuccessMeasure nu p stat let s' : Measure ℝ := statisticSuccessMeasure nu' p' stat have hsle : s ≤ m := by dsimp [s, m, statisticSuccessMeasure] apply Measure.map_mono · calc nu.withDensity (fun x => ofReal (p x)) ≤ nu.withDensity 1 := by apply withDensity_mono filter_upwards with x simpa using ENNReal.ofReal_le_one.mpr (by linarith [hp1 x]) _ = nu := withDensity_one · exact hstat have hs'le : s' ≤ m := by change statisticSuccessMeasure nu' p' stat ≤ Measure.map stat nu rw [hmap] dsimp [s', statisticSuccessMeasure] apply Measure.map_mono · calc nu'.withDensity (fun x => ofReal (p' x)) ≤ nu'.withDensity 1 := by apply withDensity_mono filter_upwards with x simpa using ENNReal.ofReal_le_one.mpr (by linarith [hp1' x]) _ = nu' := withDensity_one · exact hstat letI : IsFiniteMeasure s := isFiniteMeasure_of_le m hsle letI : IsFiniteMeasure s' := isFiniteMeasure_of_le m hs'le have hg : Integrable g m := by dsimp [g, statisticSuccessParameter, m] exact Measure.integrable_toReal_rnDeriv have hg' : Integrable g' m := by change Integrable (statisticSuccessParameter nu' p' stat) (Measure.map stat nu) rw [hmap] unfold statisticSuccessParameter exact Measure.integrable_toReal_rnDeriv have hc : Integrable (E.indicator (fun _ : ℝ => D)) m := (integrable_const _).indicator hE have hconst (B : Set ℝ) (hB : MeasurableSet B) : (∫ r in B, E.indicator (fun _ : ℝ => D) r ∂m) = D * (m (B ∩ E)).toReal := by rw [integral_indicator hE, integral_const] simp [Measure.real_def, Measure.restrict_apply, hB, hE, inter_comm, mul_comm] have hup : (fun r => g r - g' r) ≤ᵐ[m] E.indicator (fun _ => D) := by apply ae_le_of_forall_setIntegral_le (hg.sub hg') hc intro B hB _ change (∫ r in B, g r - g' r ∂m) ≤ _ rw [integral_sub hg.integrableOn hg'.integrableOn] rw [statisticSuccessParameter_setIntegral nu p stat hp hstat (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) B hB] have hp'Int := statisticSuccessParameter_setIntegral nu' p' stat hp' hstat (fun x => by linarith [hp0' x]) (fun x => by linarith [hp1' x]) B hB change (∫ r in B, g' r ∂Measure.map stat nu') = _ at hp'Int rw [← hmap] at hp'Int rw [hp'Int, hconst B hB] exact (abs_le.mp (hdiff B hB)).2 have hdown : (fun r => g' r - g r) ≤ᵐ[m] E.indicator (fun _ => D) := by apply ae_le_of_forall_setIntegral_le (hg'.sub hg) hc intro B hB _ change (∫ r in B, g' r - g r ∂m) ≤ _ rw [integral_sub hg'.integrableOn hg.integrableOn] have hp'Int := statisticSuccessParameter_setIntegral nu' p' stat hp' hstat (fun x => by linarith [hp0' x]) (fun x => by linarith [hp1' x]) B hB change (∫ r in B, g' r ∂Measure.map stat nu') = _ at hp'Int rw [← hmap] at hp'Int rw [hp'Int, statisticSuccessParameter_setIntegral nu p stat hp hstat (fun x => by linarith [hp0 x]) (fun x => by linarith [hp1 x]) B hB, hconst B hB] have hh := (abs_le.mp (hdiff B hB)).1 dsimp [m] linarith have heq := clippedStatisticSuccessParameter_ae_eq nu p stat hp hstat hp0 hp1 have heq' := clippedStatisticSuccessParameter_ae_eq nu' p' stat hp' hstat hp0' hp1' rw [← hmap] at heq' filter_upwards [hup, hdown, heq, heq'] with r hrup hrdown hr hr' rw [hr, hr'] exact abs_le.mpr ⟨by linarith, by linarith⟩ -
statisticBernoulliOutcome_restrict_compl_eq_of_localized_success_boundlemma — Common statistic marginals and a localized setwise success-mass bound also imply exact agreement of the compressed outcome laws away from the exceptional statistic set.hypothesesA :Type*nu nu' :p p' :A → ℝstat :A → ℝhp :hp' :Measurable p'hstat :Measurable stathp0 :∀ x, 1 / 4 ≤ p xhp1 :∀ x, p x ≤ 3 / 4hp0' :∀ x, 1 / 4 ≤ p' xhp1' :∀ x, p' x ≤ 3 / 4hmap :Measure.map stat nu = Measure.map stat nu'D :ℝhD :0 ≤ DE :Set ℝhE :conclusion(Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp))).restrict {z | z.2 ∉ E}= (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu' (commonStatisticBernoulliKernel p' hp'))).restrict {z | z.2 ∉ E}Proof (Lean source)
lemma statisticBernoulliOutcome_restrict_compl_eq_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) : (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu (commonStatisticBernoulliKernel p hp))).restrict {z | z.2 ∉ E} = (Measure.map (fun z : A × ℝ => (z.2, stat z.1)) (Measure.compProd nu' (commonStatisticBernoulliKernel p' hp'))).restrict {z | z.2 ∉ 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] let m : Measure ℝ := Measure.map stat nu let g : ℝ → ℝ := clippedStatisticSuccessParameter nu p stat let g' : ℝ → ℝ := clippedStatisticSuccessParameter nu' p' stat let hg : Measurable g := clippedStatisticSuccessParameter_measurable nu p stat let hg' : Measurable g' := clippedStatisticSuccessParameter_measurable nu' p' stat letI : IsFiniteMeasure m := Measure.isFiniteMeasure_map nu stat letI : IsMarkovKernel (commonStatisticBernoulliKernel g hg) := commonStatisticBernoulliKernel_isMarkovKernel g hg (fun r => by dsimp [g]; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu p stat r).1]) (fun r => by dsimp [g]; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu p stat r).2]) letI : IsMarkovKernel (commonStatisticBernoulliKernel g' hg') := commonStatisticBernoulliKernel_isMarkovKernel g' hg' (fun r => by dsimp [g']; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu' p' stat r).1]) (fun r => by dsimp [g']; linarith [ (clippedStatisticSuccessParameter_mem_Icc nu' p' stat r).2]) have hparam := clippedStatisticSuccessParameter_abs_sub_le_ae nu nu' p p' stat hp hp' hstat hp0 hp1 hp0' hp1' hmap hD hE hdiff ext S hS have houtside : {z : ℝ × ℝ | z.2 ∉ E} = snd ⁻¹' Eᶜ := by ext z simp rw [houtside] rw [Measure.restrict_apply hS, Measure.restrict_apply hS] rw [Measure.map_apply measurable_swap (hS.inter (hE.compl.preimage measurable_snd)), Measure.map_apply measurable_swap (hS.inter (hE.compl.preimage measurable_snd))] rw [Measure.compProd_apply, Measure.compProd_apply] · apply lintegral_congr_ae filter_upwards [hparam] with r hr by_cases hrE : r ∈ E · have hempty : Prod.mk r ⁻¹' (swap ⁻¹' (S ∩ snd ⁻¹' Eᶜ)) = ∅ := by ext y simp [hrE] rw [hempty, measure_empty, measure_empty] · have hzero : |g r - g' r| ≤ 0 := by simpa [g, g', Set.indicator_of_notMem hrE] using hr have heq : g r = g' r := sub_eq_zero.mp (abs_eq_zero.mp (le_antisymm hzero (abs_nonneg _))) have hk : commonStatisticBernoulliKernel g hg r = commonStatisticBernoulliKernel g' hg' r := by ext B hB simp [commonStatisticBernoulliKernel, heq] rw [hk] · exact (hS.inter (hE.compl.preimage measurable_snd)).preimage measurable_swap · exact (hS.inter (hE.compl.preimage measurable_snd)).preimage measurable_swap
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
⚑ flagged
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 when its outcome is the decoded outcome, and by otherwise, where is the decoder's error mass and is the number of outcome values.
theorem fano_inequality reviewed
⚑ flagged
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
β :
Type u_2
α × β → ℝ
hp0 :
∀ xy, 0 ≤ p xy
hsum :
∑ xy : α × β, p xy = 1
hcard :
2 ≤ Fintype.card α
decode :
β → α
conclusion
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
theorem fano_error_lower_bound reviewed
⚑ flagged
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
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
5 supporting declarations (lemmas, instances)
-
fanoRef_deflemmahypothesesα :sharedType u_1β :sharedType u_2p :α × β → ℝdecode :β → αxy :α × β -
fanoRef_nonneglemma — The Fano reference distribution is nonnegative.hypothesesα :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xyhsum :∑ xy : α × β, p xy = 1decode :β → αxy :α × βconclusion0 ≤ fanoRef p decode xyProof (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) -
fanoRef_sum_eq_onelemma — 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α :sharedType u_1β :sharedType u_2α × β → ℝhsum :∑ xy : α × β, p xy = 1hcard :2 ≤ card αdecode :β → αconclusion∑ xy : α × β, fanoRef p decode xy = 1Proof (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 -
fanoRef_aclemma — 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α :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xyhsum :∑ xy : α × β, p xy = 1hcard :2 ≤ card αdecode :β → αxy :α × βhxy :p xy ≠ 0conclusion0 < fanoRef p decode xyProof (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 -
neg_crossEntropy_fanoReflemma — 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α :sharedType u_1β :sharedType u_2α × β → ℝhp0 :∀ xy, 0 ≤ p xyhsum :∑ xy : α × β, p xy = 1hcard :2 ≤ Fintype.card αdecode :β → α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]
FiniteWordChainRule 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
⚑ flagged
Causalean.Mathlib.InformationTheory.FiniteWordChainRule
Given a finite word and a final symbol, append the symbol to the word.
def lastCoordinateSplit reviewed
⚑ flagged
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
k :
given by
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]
def prefixPMF reviewed
⚑ flagged
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
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)
def nextSymbolPMF reviewed
⚑ flagged
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
def
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 _ _))
def nextSymbolKernel reviewed
⚑ flagged
Causalean.Mathlib.InformationTheory.FiniteWordChainRule
Given a finite-word law, its conditional last-symbol laws form a kernel on strict prefixes.
def chainKL reviewed
⚑ flagged
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
k :
ℕ
given by
clause 1
| 0, _, _ => 0
clause 2
| k + 1, p, q
+ klDiv ((prefixPMF p).toMeasure.compProd (nextSymbolKernel p)) ((prefixPMF p).toMeasure.compProd (nextSymbolKernel q))
lemma klDiv_eq_chainKL reviewed
⚑ flagged
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
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
13 supporting declarations (lemmas, instances)
-
appendSymbol_eq_snoctheorem — Appending a symbol to a finite word agrees with Mathlib's tuple append Fin.snoc.hypothesesconclusionappendSymbol u x = snoc (α := fun _ ↦ Ω) u xProof (Lean source)
theorem appendSymbol_eq_snoc {k : Nat} (u : Fin k → Ω) (x : Ω) : appendSymbol u x = snoc (α := fun _ ↦ Ω) u x := by funext i refine Fin.lastCases ?_ (fun j ↦ ?_) i <;> simp [appendSymbol] -
prefixPMF_applylemma — For a finite-word law and a strict prefix, the prefix mass is the sum of the masses of all one-symbol extensions.hypothesesconclusionprefixPMF p u = ∑ x : Ω, p (appendSymbol u x)Proof (Lean source)
@[simp] lemma prefixPMF_apply {k : Nat} (p : PMF (Fin (k + 1) → Ω)) (u : Fin k → Ω) : prefixPMF p u = ∑ x : Ω, p (appendSymbol u x) := by simp [prefixPMF] -
nextSymbolKernel_isMarkovinstance — For a finite-word law, the conditional last-symbol kernel is Markov.parametersinstancegiven byisProbabilityMeasure u := by change IsProbabilityMeasure (nextSymbolPMF p u).toMeasure infer_instance -
prefix_mul_nextSymbollemma — Given a finite-word law, a strict prefix, and a final symbol, prefix mass times conditional final-symbol mass recovers the joint word mass, including on null prefixes.hypothesesconclusionProof (Lean source)
lemma prefix_mul_nextSymbol {k : Nat} (p : PMF (Fin (k + 1) → Ω)) (u : Fin k → Ω) (x : Ω) : prefixPMF p u * nextSymbolPMF p u x = p (appendSymbol u x) := by classical by_cases h : prefixPMF p u = 0 · have hx : p (appendSymbol u x) = 0 := by have hsum := prefixPMF_apply p u rw [h] at hsum exact (Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ bot_le)).mp hsum.symm x (Finset.mem_univ x) simp [nextSymbolPMF, h, hx] · rw [nextSymbolPMF, dif_neg h, PMF.ofFintype_apply] exact ENNReal.mul_div_cancel h (PMF.apply_ne_top _ _) -
prefixPMF_fullSupportlemma — If a finite-word law has strictly positive mass at every word, its strict-prefix marginal also has strictly positive mass everywhere.hypothesesconclusion0 < prefixPMF p uProof (Lean source)
lemma prefixPMF_fullSupport {k : Nat} {p : PMF (Fin (k + 1) → Ω)} (hp : ∀ w, 0 < p w) : ∀ u, 0 < prefixPMF p u := by intro u rw [prefixPMF_apply] exact lt_of_lt_of_le (hp (appendSymbol u (choice inferInstance))) (Finset.single_le_sum (f := fun x ↦ p (appendSymbol u x)) (fun _ _ ↦ bot_le) (Finset.mem_univ (choice inferInstance))) -
nextSymbolPMF_fullSupportlemma — If a finite-word law has strictly positive mass at every word, then for every strict prefix, its totalized conditional last-symbol law has strictly positive mass at every symbol.hypothesesconclusion0 < nextSymbolPMF p u xProof (Lean source)
lemma nextSymbolPMF_fullSupport {k : Nat} {p : PMF (Fin (k + 1) → Ω)} (hp : ∀ w, 0 < p w) (u : Fin k → Ω) : ∀ x, 0 < nextSymbolPMF p u x := by intro x have hprefix := prefixPMF_fullSupport hp u rw [nextSymbolPMF, dif_neg (ne_of_gt hprefix), PMF.ofFintype_apply] exact ENNReal.div_pos (ne_of_gt (hp (appendSymbol u x))) (PMF.apply_ne_top _ _) -
absolutelyContinuous_of_strictlyPositivePMFlemma — Given two strictly positive finite probability mass functions, the first induced measure is absolutely continuous with respect to the second.hypothesesW :hp :∀ w, 0 < p whq :∀ w, 0 < q wconclusionp.toMeasure ≪ q.toMeasureProof (Lean source)
lemma absolutelyContinuous_of_strictlyPositivePMF {W : Type*} [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] {p q : PMF W} (hp : ∀ w, 0 < p w) (hq : ∀ w, 0 < q w) : p.toMeasure ≪ q.toMeasure := by apply Measure.AbsolutelyContinuous.mk intro s _ hqs have hs_empty : s = ∅ := by rw [← Set.not_nonempty_iff_eq_empty] rintro ⟨w, hw⟩ have hle : q.toMeasure {w} ≤ q.toMeasure s := measure_mono (Set.singleton_subset_iff.mpr hw) rw [hqs] at hle have hzero : q.toMeasure {w} = 0 := bot_unique hle rw [q.toMeasure_apply_singleton w (MeasurableSet.singleton w)] at hzero exact (ne_of_gt (hq w)) hzero simp [hs_empty] -
nextSymbolPMF_absolutelyContinuouslemma — Given two finite-word laws that are strictly positive everywhere, then for every strict prefix, the first conditional last-symbol law is absolutely continuous with respect to the second.hypothesesconclusionProof (Lean source)
lemma nextSymbolPMF_absolutelyContinuous {k : Nat} {p q : PMF (Fin (k + 1) → Ω)} (hp : ∀ w, 0 < p w) (hq : ∀ w, 0 < q w) (u : Fin k → Ω) : (nextSymbolPMF p u).toMeasure ≪ (nextSymbolPMF q u).toMeasure := absolutelyContinuous_of_strictlyPositivePMF (nextSymbolPMF_fullSupport hp u) (nextSymbolPMF_fullSupport hq u) -
lastCoordinateSplit_compProdlemma — Given a finite-word law, transport by the last-coordinate split equals the composition of its prefix marginal and conditional last-symbol kernel.hypothesesconclusionMeasure.map (lastCoordinateSplit k) p.toMeasure= (prefixPMF p).toMeasure.compProd (nextSymbolKernel p)Proof (Lean source)
lemma lastCoordinateSplit_compProd {k : Nat} (p : PMF (Fin (k + 1) → Ω)) : Measure.map (lastCoordinateSplit k) p.toMeasure = (prefixPMF p).toMeasure.compProd (nextSymbolKernel p) := by classical apply Measure.ext_of_singleton rintro ⟨u, x⟩ rw [Measure.map_apply (measurable_of_finite _) (measurableSet_singleton _)] have hpre : (lastCoordinateSplit k : (Fin (k + 1) → Ω) → (Fin k → Ω) × Ω) ⁻¹' ({(u, x)} : Set ((Fin k → Ω) × Ω)) = {appendSymbol u x} := by ext w simp only [Set.mem_preimage, Set.mem_singleton_iff] constructor · intro hw apply (lastCoordinateSplit k).injective rw [hw] exact ((lastCoordinateSplit k).right_inv (u, x)).symm · intro hw rw [hw] exact (lastCoordinateSplit k).right_inv (u, x) rw [hpre, PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _)] have hpair : ({(u, x)} : Set ((Fin k → Ω) × Ω)) = {u} ×ˢ {x} := by ext y simp rw [hpair, Measure.compProd_apply_prod (measurableSet_singleton u) (measurableSet_singleton x)] simp only [lintegral_singleton] change p (appendSymbol u x) = (nextSymbolPMF p u).toMeasure {x} * (prefixPMF p).toMeasure {u} rw [PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), mul_comm] exact (prefix_mul_nextSymbol p u x).symm -
klDiv_lastCoordinate_eq_addlemma — Given two finite-word laws, one chronological extension splits their KL divergence into the prefix KL and a shared-prefix conditional-kernel KL.hypothesesProof (Lean source)
lemma klDiv_lastCoordinate_eq_add {k : Nat} (p q : PMF (Fin (k + 1) → Ω)) : klDiv p.toMeasure q.toMeasure = klDiv (prefixPMF p).toMeasure (prefixPMF q).toMeasure + klDiv ((prefixPMF p).toMeasure.compProd (nextSymbolKernel p)) ((prefixPMF p).toMeasure.compProd (nextSymbolKernel q)) := by let e : (Fin (k + 1) → Ω) ≃ᵐ (Fin k → Ω) × Ω := { toEquiv := lastCoordinateSplit k measurable_toFun := measurable_of_finite _ measurable_invFun := measurable_of_finite _ } rw [← klDiv_map_measurableEquiv e] change klDiv (Measure.map (lastCoordinateSplit k) p.toMeasure) (Measure.map (lastCoordinateSplit k) q.toMeasure) = _ rw [lastCoordinateSplit_compProd, lastCoordinateSplit_compProd] exact InformationTheory.klDiv_compProd_eq_add _ _ _ _ -
conditionalKL_eq_sumlemma — Given two finite-word laws whose conditional last-symbol laws satisfy pointwise absolute continuity, their shared-prefix conditional KL is the prefix-probability- weighted sum of pointwise conditional divergences.hypothesesΩ :sharedType u_1k :hac :conclusionklDiv ((prefixPMF p).toMeasure.compProd (nextSymbolKernel p)) ((prefixPMF p).toMeasure.compProd (nextSymbolKernel q))= ∑ u : Fin k → Ω, prefixPMF p u * klDiv (nextSymbolPMF p u).toMeasure (nextSymbolPMF q u).toMeasureProof (Lean source)
lemma conditionalKL_eq_sum {k : Nat} (p q : PMF (Fin (k + 1) → Ω)) (hac : ∀ u, (nextSymbolPMF p u).toMeasure ≪ (nextSymbolPMF q u).toMeasure) : klDiv ((prefixPMF p).toMeasure.compProd (nextSymbolKernel p)) ((prefixPMF p).toMeasure.compProd (nextSymbolKernel q)) = ∑ u : Fin k → Ω, prefixPMF p u * klDiv (nextSymbolPMF p u).toMeasure (nextSymbolPMF q u).toMeasure := by rw [klDiv_compProd_right_of_forall_ac] · rw [MeasureTheory.lintegral_fintype] apply Finset.sum_congr rfl intro u _ rw [PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), mul_comm] change prefixPMF p u * klDiv (nextSymbolPMF p u).toMeasure (nextSymbolPMF q u).toMeasure = _ rfl · exact Filter.Eventually.of_forall hac -
klDiv_lastCoordinate_eq_add_sumlemma — Given two finite-word laws whose conditional last-symbol laws satisfy pointwise absolute continuity, one chronological extension is the prefix KL plus the explicit average of pointwise conditional divergences.hypothesesΩ :sharedType u_1k :hac :Proof (Lean source)
lemma klDiv_lastCoordinate_eq_add_sum {k : Nat} (p q : PMF (Fin (k + 1) → Ω)) (hac : ∀ u, (nextSymbolPMF p u).toMeasure ≪ (nextSymbolPMF q u).toMeasure) : klDiv p.toMeasure q.toMeasure = klDiv (prefixPMF p).toMeasure (prefixPMF q).toMeasure + ∑ u : Fin k → Ω, prefixPMF p u * klDiv (nextSymbolPMF p u).toMeasure (nextSymbolPMF q u).toMeasure := by rw [klDiv_lastCoordinate_eq_add, conditionalKL_eq_sum p q hac] -
klDiv_lastCoordinate_eq_add_sum_of_fullSupportlemma — Given two finite-word laws that have strictly positive mass at every word, one chronological extension is the prefix KL plus the explicit average of pointwise conditional divergences.hypothesesProof (Lean source)
lemma klDiv_lastCoordinate_eq_add_sum_of_fullSupport {k : Nat} (p q : PMF (Fin (k + 1) → Ω)) (hp : ∀ w, 0 < p w) (hq : ∀ w, 0 < q w) : klDiv p.toMeasure q.toMeasure = klDiv (prefixPMF p).toMeasure (prefixPMF q).toMeasure + ∑ u : Fin k → Ω, prefixPMF p u * klDiv (nextSymbolPMF p u).toMeasure (nextSymbolPMF q u).toMeasure := klDiv_lastCoordinate_eq_add_sum p q (fun u ↦ nextSymbolPMF_absolutelyContinuous hp hq u)
GaussianKL 1 core · 5 supporting Mathlib provides the real Gaussian measure ProbabilityTheory.gaussianReal m v (mean m : ℝ, variance v : ℝ≥0) and the Kullback–Leibler divergence MeasureTheory.klDiv (an ℝ≥0∞), but not the closed form of the KL divergence ★ 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
MeasureTheory.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`),
which is the canonical KL input for Gaussian-location minimax (Le Cam / two-point) lower bounds.
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
⚑ flagged
Causalean.Mathlib.InformationTheory
Equal-variance Gaussian KL divergence (closed form). For means m₀, m₁ and a strictly positive common variance v, the Kullback–Leibler divergence between two real Gaussians of equal variance v and respective means m₀ and m₁ equals (m₀ - m₁)² / (2v):
Formal statement
hypotheses
conclusion
= 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
5 supporting declarations (lemmas, instances)
-
gaussianReal_ac_gaussianReallemma — 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.hypothesesm₀ m₁ :ℝv₀ v₁ :ℝ≥0hv₀ :v₀ ≠ 0hv₁ :v₁ ≠ 0conclusiongaussianReal 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₁) -
rnDeriv_toReal_gaussianReal_aelemma — 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.hypothesesconclusionProof (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] -
llr_gaussianReal_aelemma — 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).hypothesesconclusion=ᵐ[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 -
integrable_llr_gaussianReallemma — 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.hypothesesconclusionProof (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 -
integral_llr_gaussianReallemma — 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₀.hypothesesconclusion= (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
KLBind 3 core · 7 supporting 1 to review 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★ klDiv_bind_le
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 least-favourable laws and 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
⚑ flagged
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
β :
Type u_2
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
lemma klDiv_bind_eq_of_base_recording reviewed
⚑ flagged
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 Ω :
m :
κ η :
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κη
theorem klDiv_bind_le unreviewed
⚑ flagged
Causalean.Mathlib.InformationTheory.Measure
Passing two finite input laws μ and ν through the same randomized observation channel κ, the Kullback–Leibler divergence between the channel's output laws is no larger than the divergence between the original input laws, including when the channel is non-injective or the original divergence is infinite. Mathlib now provides the same data-processing inequality as InformationTheory.klDiv_comp_right_le.
Formal statement
hypotheses
conclusion
_root_.InformationTheory.klDiv (μ.bind κ) (ν.bind κ) ≤ _root_.InformationTheory.klDiv μ ν
Proof (Lean source)
theorem klDiv_bind_le (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
(κ : Kernel α β) [IsMarkovKernel κ] :
_root_.InformationTheory.klDiv (μ.bind κ) (ν.bind κ)
≤ _root_.InformationTheory.klDiv μ ν := by
rw [← Measure.snd_compProd μ κ, ← Measure.snd_compProd ν κ]
exact (klDiv_map_le (μ := μ ⊗ₘ κ) (ν := ν ⊗ₘ κ) measurable_snd).trans_eq
(klDiv_compProd_left μ ν κ)
7 supporting declarations (lemmas, instances)
-
rnDeriv_compProd_right_of_forall_aclemma — Radon--Nikodym derivative of a shared-base composition product.hypothesesα :sharedType u_1β :sharedType u_2hκη :∀ᵐ a ∂μ, κ a ≪ η aconclusion(μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p : α × β => Kernel.rnDeriv κ η p.1 p.2Proof (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] -
klDiv_map_measurableEmbeddinglemma — KL is invariant under a measurable embedding.hypothesesα :sharedType u_1γ :sharedType u_3f :α → γhf :ν :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] -
measurableEmbedding_base_recordinglemma — If a measurable map has a measurable graph, pairing each observation with its map value produces a measurable embedding into the corresponding product space.hypothesesconclusionMeasurableEmbedding (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) -
map_bind_eq_compProd_of_base_recordinglemma — 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.hypothesesB Ω :κ :Kernel B Ωproj :Ω → Bhproj :Measurable projhκ_fib :∀ᵐ b ∂m, (κ b) {ω | proj ω = b}ᶜ = 0conclusion(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 -
klDiv_map_letheorem — A common measurable observation rule cannot increase the Kullback--Leibler divergence between two finite input laws, even when the rule merges distinct inputs.hypothesesα :sharedType u_1β :sharedType u_2μ ν :f :α → βhf :conclusion_root_.InformationTheory.klDiv (μ.map f) (ν.map f) ≤ _root_.InformationTheory.klDiv μ νProof (Lean source)
theorem klDiv_map_le {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {f : α → β} (hf : Measurable f) : _root_.InformationTheory.klDiv (μ.map f) (ν.map f) ≤ _root_.InformationTheory.klDiv μ ν := by classical by_cases htop : _root_.InformationTheory.klDiv μ ν = ∞ · rw [htop] exact le_top have hμν_int := _root_.InformationTheory.klDiv_ne_top_iff.mp htop have hμν : μ ≪ ν := hμν_int.1 have hmap : μ.map f ≪ ν.map f := by refine Measure.AbsolutelyContinuous.mk ?_ intro s hs hs0 rw [Measure.map_apply hf hs] at hs0 ⊢ exact hμν hs0 let mf : Unit → MeasurableSpace α := fun _ => MeasurableSpace.comap f inferInstance have hmf : mf () ≤ (inferInstance : MeasurableSpace α) := by simpa [mf] using hf.comap_le let p : α → ℝ := fun x => (μ.rnDeriv ν x).toReal let q : β → ℝ := fun y => ((μ.map f).rnDeriv (ν.map f) y).toReal have hp : Integrable p ν := Measure.integrable_toReal_rnDeriv have hp0 : 0 ≤ᵐ[ν] p := ae_of_all ν fun _ => ENNReal.toReal_nonneg have hkp : Integrable (fun x => _root_.InformationTheory.klFun (p x)) ν := by exact (_root_.InformationTheory.integrable_klFun_rnDeriv_iff hμν).2 hμν_int.2 have hq : Integrable q (ν.map f) := Measure.integrable_toReal_rnDeriv have hq_comp : Integrable (q ∘ f) ν := hq.comp_measurable hf have hq_cond : q ∘ f =ᵐ[ν] ν[p | mf ()] := by apply ae_eq_condExp_of_forall_setIntegral_eq hmf hp · intro s _ _ exact hq_comp.integrableOn · intro s hs _ change ∃ t, MeasurableSet t ∧ f ⁻¹' t = s at hs obtain ⟨t, ht, rfl⟩ := hs calc ∫ x in f ⁻¹' t, (q ∘ f) x ∂ν = ∫ y in t, q y ∂(ν.map f) := by symm exact setIntegral_map ht (by fun_prop) hf.aemeasurable _ = (μ.map f).real t := Measure.setIntegral_toReal_rnDeriv hmap t _ = μ.real (f ⁻¹' t) := by simp [Measure.map_apply hf ht, measureReal_def] _ = ∫ x in f ⁻¹' t, p x ∂ν := (Measure.setIntegral_toReal_rnDeriv hμν (f ⁻¹' t)).symm · have hq_meas : Measurable q := by dsimp [q] exact (Measure.measurable_rnDeriv _ _).ennreal_toReal have hf_mf : Measurable[mf ()] f := by simpa [mf] using comap_measurable f exact (hq_meas.comp hf_mf).aestronglyMeasurable have hJ := klFun_condExp_le hmf p hp hp0 hkp have hineq : (fun x => _root_.InformationTheory.klFun (q (f x))) ≤ᵐ[ν] ν[fun y => _root_.InformationTheory.klFun (p y) | mf ()] := by filter_upwards [hq_cond, hJ] with x hqc hj change _root_.InformationTheory.klFun ((q ∘ f) x) ≤ _ rw [hqc] exact hj have hw0 : 0 ≤ᵐ[ν] ν[fun y => _root_.InformationTheory.klFun (p y) | mf ()] := condExp_nonneg (ae_of_all ν fun x => _root_.InformationTheory.klFun_nonneg (show 0 ≤ p x from ENNReal.toReal_nonneg)) have hkq_comp : Integrable (fun x => _root_.InformationTheory.klFun (q (f x))) ν := by apply Integrable.mono' (integrable_condExp : Integrable (ν[fun y => _root_.InformationTheory.klFun (p y) | mf ()]) ν) · have hq_meas : Measurable q := by dsimp [q] exact (Measure.measurable_rnDeriv _ _).ennreal_toReal exact (_root_.InformationTheory.measurable_klFun.comp (hq_meas.comp hf)).aestronglyMeasurable filter_upwards [hineq, hw0] with x hx hwx rw [Real.norm_eq_abs, abs_of_nonneg (_root_.InformationTheory.klFun_nonneg (show 0 ≤ q (f x) from ENNReal.toReal_nonneg))] exact hx have hkq : Integrable (fun y => _root_.InformationTheory.klFun (q y)) (ν.map f) := by rw [integrable_map_measure (by fun_prop) hf.aemeasurable] exact hkq_comp have hllr_map : Integrable (llr (μ.map f) (ν.map f)) (μ.map f) := (_root_.InformationTheory.integrable_klFun_rnDeriv_iff hmap).1 hkq apply (ENNReal.toReal_le_toReal (_root_.InformationTheory.klDiv_ne_top hmap hllr_map) htop).mp rw [_root_.InformationTheory.toReal_klDiv_eq_integral_klFun hmap, _root_.InformationTheory.toReal_klDiv_eq_integral_klFun hμν] change (∫ y, _root_.InformationTheory.klFun (q y) ∂(ν.map f)) ≤ ∫ x, _root_.InformationTheory.klFun (p x) ∂ν rw [integral_map hf.aemeasurable hkq.1] calc ∫ x, _root_.InformationTheory.klFun (q (f x)) ∂ν ≤ ∫ x, ν[fun y => _root_.InformationTheory.klFun (p y) | mf ()] x ∂ν := integral_mono_ae hkq_comp integrable_condExp hineq _ = ∫ x, _root_.InformationTheory.klFun (p x) ∂ν := integral_condExp hmf -
klDiv_compProd_lefttheorem — Adding an output drawn from the same Markov kernel preserves the Kullback--Leibler divergence between two finite input laws because the joint observation still retains the input coordinate.hypothesesconclusion_root_.InformationTheory.klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = _root_.InformationTheory.klDiv μ νProof (Lean source)
theorem klDiv_compProd_left (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ : Kernel α β) [IsMarkovKernel κ] : _root_.InformationTheory.klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = _root_.InformationTheory.klDiv μ ν := by classical by_cases hμν : μ ≪ ν · have hcomp : μ ⊗ₘ κ ≪ ν ⊗ₘ κ := hμν.compProd_left κ rw [_root_.InformationTheory.klDiv_eq_lintegral_klFun, _root_.InformationTheory.klDiv_eq_lintegral_klFun, if_pos hcomp, if_pos hμν] calc _ = ∫⁻ p : α × β, ofReal (_root_.InformationTheory.klFun ((μ.rnDeriv ν p.1).toReal)) ∂(ν ⊗ₘ κ) := by refine lintegral_congr_ae ?_ filter_upwards [ProbabilityTheory.rnDeriv_measure_compProd_left μ ν κ] with p hp rw [hp] _ = _ := by rw [Measure.lintegral_compProd] · simp · fun_prop · have hcomp : ¬ μ ⊗ₘ κ ≪ ν ⊗ₘ κ := fun hac ↦ hμν (Measure.absolutelyContinuous_of_compProd hac) rw [_root_.InformationTheory.klDiv_of_not_ac hcomp, _root_.InformationTheory.klDiv_of_not_ac hμν] -
klDiv_bind_le_of_isProbabilityMeasuretheorem — Passing two probability laws through a shared Markov channel cannot increase their Kullback--Leibler divergence; this is the probability-law specialization of the finite-measure data-processing inequality.hypothesesconclusion_root_.InformationTheory.klDiv (μ.bind κ) (ν.bind κ) ≤ _root_.InformationTheory.klDiv μ νProof (Lean source)
theorem klDiv_bind_le_of_isProbabilityMeasure (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (κ : Kernel α β) [IsMarkovKernel κ] : _root_.InformationTheory.klDiv (μ.bind κ) (ν.bind κ) ≤ _root_.InformationTheory.klDiv μ ν := by exact klDiv_bind_le μ ν κ
ProductKLLeCam 2 core · 13 supporting This file proves and packages tensorisation tools for Kullback--Leibler divergence over finite product laws. ★ productKL_tensorization
Product KL Bounds for Le Cam Arguments
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(μ,ν) so downstream Le Cam arguments cannot accidentally hide an
infinite KL term behind ENNReal.toReal.
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_absolutelyContinuous and pi_iid_llr_integrable, reusable finite-product
side conditions.
It is a Mathlib-adjacent information-theory layer rather than a causal model construction.
def ProductKLTensorizationBound reviewed
⚑ flagged
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 -fold product measures is finite, their one-observation Kullback--Leibler divergence is finite, and the real-valued product divergence is at most times the real-valued one-observation divergence.
Definition (Lean source)
parameters
def
ProductKLTensorizationBound n μ ν :
Prop
given by
clause 1
clause 2
_root_.InformationTheory.klDiv μ ν ≠ ∞
theorem productKL_tensorization reviewed
⚑ flagged
Causalean.Mathlib.InformationTheory
For a sample size n and probability measures μ, ν on a measurable space α, if μ is absolutely continuous with respect to ν and the log-likelihood ratio of μ against ν is μ-integrable, then both the KL divergence between the n-fold product of μ and the n-fold product of ν, and the one-observation KL divergence between μ and ν, are finite, and the real-valued product KL divergence is at most n times the real-valued one-observation KL divergence: this is product-KL tensorisation packaged in the Le Cam interface.
Formal statement
Proof (Lean source)
theorem productKL_tensorization {α : Type*} [MeasurableSpace α]
(n : ℕ) (μ ν : Measure α) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(hac : μ ≪ ν) (hint : Integrable (llr μ ν) μ) :
ProductKLTensorizationBound n μ ν := by
have hπac := ProductKLPrivate.pi_absolutelyContinuous_iid μ ν hac
have hπint := ProductKLPrivate.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⟩
13 supporting declarations (lemmas, instances)
-
ae_prod_fst_of_aelemma — A measurable property holding almost everywhere under a measure also holds for the first coordinate almost everywhere under its product with a probability measure.hypothesesconclusion∀ᵐ z ∂μ.prod ν, p z.1Proof (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 -
ae_prod_snd_of_aelemma — A measurable property holding almost everywhere under a measure also holds for the second coordinate almost everywhere under its product with a probability measure.hypothesesconclusion∀ᵐ z ∂μ.prod ν, p z.2Proof (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 -
llr_prod_aelemma — 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.hypothesesProof (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' -
llr_prod_integrablelemma — Integrable component log-likelihood ratios imply that the log-likelihood ratio of the corresponding product laws is integrable.hypothesesα β :μ₁ ν₁ :Measure αμ₂ ν₂ :Measure βSigmaFinite ν₁SigmaFinite ν₂h₁ :μ₁ ≪ ν₁h₂ :μ₂ ≪ ν₂hint₁ :Integrable (llr μ₁ ν₁) μ₁hint₂ :Integrable (llr μ₂ ν₂) μ₂conclusionIntegrable (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₂) -
llr_integrable_of_map_measurableEquivlemma — 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α β :e :α ≃ᵐ βμ ν :hμν :μ ≪ νhint :Integrable (llr (Measure.map e μ) (Measure.map e ν)) (Measure.map e μ)conclusionIntegrable (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 -
klDiv_prod_toReal_addlemma — 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α β :μ₁ ν₁ :Measure αμ₂ ν₂ :Measure βh₁ :μ₁ ≪ ν₁h₂ :μ₂ ≪ ν₂hint₁ :Integrable (llr μ₁ ν₁) μ₁hint₂ :Integrable (llr μ₂ ν₂) μ₂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 -
productKL_tensorization_toReal_eqlemma — 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*n :ℕμ ν :hac :μ ≪ νhint :Integrable (llr μ ν) μhπint :∀ k : ℕ,Integrable (llr (Measure.pi (fun _ : Fin k => μ)) (Measure.pi (fun _ : Fin k => ν))) (Measure.pi (fun _ : Fin k => μ))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) → α) := MeasurableEquiv.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 -
productKL_tensorization_of_finitetheorem — Finite-branch product-KL tensorisation for i.i.d. finite products.hypothesesProof (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 := ProductKLPrivate.productKL_tensorization_toReal_eq n μ ν hac hint (ProductKLPrivate.pi_absolutelyContinuous_iid μ ν hac) (ProductKLPrivate.pi_llr_integrable_iid μ ν hac hint) -
applytheorem — Unpack a supplied product-KL tensorisation bound.hypothesesProof (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 -
product_ne_toptheorem — The product KL divergence in a supplied tensorisation bound is finite.hypothesesProof (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 -
one_ne_toptheorem — The one-observation KL divergence in a supplied tensorisation bound is finite.hypothesesconclusion_root_.InformationTheory.klDiv μ ν ≠ ∞Proof (Lean source)
theorem ProductKLTensorizationBound.one_ne_top {α : Type*} [MeasurableSpace α] {n : ℕ} {μ ν : Measure α} (h : ProductKLTensorizationBound n μ ν) : _root_.InformationTheory.klDiv μ ν ≠ ∞ := h.2.1 -
pi_iid_absolutelyContinuoustheorem — Public: absolute continuity of i.i.d. finite products from the one-sample hypothesis μ ≪ ν for sigma-finite laws. (Thin wrapper over the private induction.)hypothesesProof (Lean source)
theorem pi_iid_absolutelyContinuous {α : Type*} [MeasurableSpace α] (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (n : ℕ) : Measure.pi (fun _ : Fin n => μ) ≪ Measure.pi (fun _ : Fin n => ν) := ProductKLPrivate.pi_absolutelyContinuous_iid μ ν hμν n -
pi_iid_llr_integrabletheorem — Public: log-likelihood-ratio integrability for i.i.d. finite products from the one-sample hypotheses μ ≪ ν and Integrable (llr μ ν) μ. Combined with pi_iid_absolutelyContinuous this certifies klDiv (pi μ) (pi ν) ≠ ⊤ (via InformationTheory.klDiv_ne_top).hypothesesconclusionIntegrable (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 => μ)) := ProductKLPrivate.pi_llr_integrable_iid μ ν hμν hint n