Mathlib.Probability.Poisson.FinitePartition.UnequalMassKL
This module collects the count, conditional-sample, and finite-measure components of the exact KL identity for finite marked Poisson laws with arbitrary total intensity masses.
Count 2 core · 3 supporting This module gives the exact extended-real divergence of Poisson count laws at arbitrary nonnegative rates, including zero rates. ★ klDiv_poissonMeasure
Unequal-rate Poisson count divergence
This module gives the exact extended-real divergence of Poisson count laws at arbitrary nonnegative rates, including zero rates.
def poissonRateKL reviewed
⚑ flagged
Causalean.Mathlib.Probability.Poisson.FinitePartition.UnequalMassKL
Two nonnegative Poisson rates determine the extended-real rate divergence, given by three cases: the second rate when the first rate is zero; infinity when the first rate is positive and the second is zero; and otherwise the first rate times the logarithm of the ratio of first to second rate, plus the second rate, minus the first.
theorem klDiv_poissonMeasure reviewed
⚑ flagged
Causalean.Mathlib.Probability.Poisson.FinitePartition.UnequalMassKL
Two nonnegative Poisson rates imply that the exact extended-real count-law divergence equals their rate divergence, including the zero-rate cases.
Formal statement
Proof (Lean source)
theorem klDiv_poissonMeasure (r s : ℝ≥0) :
klDiv
(poissonMeasure r) (poissonMeasure s) =
poissonRateKL r s := by
by_cases hr : r = 0
· subst r
simpa [poissonRateKL] using klDiv_poissonMeasure_zero_left s
by_cases hs : s = 0
· subst s
simpa [poissonRateKL, hr] using klDiv_poissonMeasure_zero_right r hr
simpa [poissonRateKL, hr, hs] using klDiv_poissonMeasure_pos r s hr hs
3 supporting declarations (lemmas, instances)
-
poissonMeasure_zero_eq_diractheorem — The Poisson count law at zero rate is the point mass at count zero.conclusionpoissonMeasure 0 = Measure.dirac 0Proof (Lean source)
theorem poissonMeasure_zero_eq_dirac : poissonMeasure 0 = Measure.dirac 0 := by ext s hs rw [poissonMeasure, Measure.sum_apply _ hs] refine (tsum_eq_single 0 ?_).trans ?_ · intro n hn rw [Measure.smul_apply, smul_eq_mul] simp [zero_pow hn] · simp -
poisson_lintegral_counttheorem — A nonnegative Poisson rate determines an extended-real first count moment equal to that rate.hypothesesr :ℝ≥0conclusion∫⁻ n : ℕ, (n : ℝ≥0∞) ∂poissonMeasure r = (r : ℝ≥0∞)Proof (Lean source)
theorem poisson_lintegral_count (r : ℝ≥0) : ∫⁻ n : ℕ, (n : ℝ≥0∞) ∂poissonMeasure r = (r : ℝ≥0∞) := by rw [lintegral_countable'] simp_rw [poissonMeasure_singleton_eq_poissonPMF] rw [tsum_eq_zero_add' ENNReal.summable] simp only [Nat.cast_zero, zero_mul, zero_add] simp_rw [poissonPMF_succ_mul] rw [ENNReal.tsum_mul_left, PMF.tsum_coe, mul_one] -
poissonRateKL_mul_lefttheorem — A common intensity multiplier and two Poisson rates imply that their rate divergence scales by that multiplier, including zero rates.hypotheseslam r s :ℝ≥0conclusionpoissonRateKL (lam * r) (lam * s) = (lam : ℝ≥0∞) * poissonRateKL r sProof (Lean source)
theorem poissonRateKL_mul_left (lam r s : ℝ≥0) : poissonRateKL (lam * r) (lam * s) = (lam : ℝ≥0∞) * poissonRateKL r s := by by_cases hl : lam = 0 · subst lam simp [poissonRateKL] by_cases hr : r = 0 · subst r simp [poissonRateKL] by_cases hs : s = 0 · subst s simp [poissonRateKL, hl, hr] have hlr : lam * r ≠ 0 := mul_ne_zero hl hr have hls : lam * s ≠ 0 := mul_ne_zero hl hs simp only [poissonRateKL, if_neg hlr, if_neg hls, if_neg hr, if_neg hs] have hla : (lam : ℝ) ≠ 0 := by exact_mod_cast hl have hsa : (s : ℝ) ≠ 0 := by exact_mod_cast hs have hratio : ((lam * r : ℝ≥0) : ℝ) / ((lam * s : ℝ≥0) : ℝ) = (r : ℝ) / (s : ℝ) := by push_cast field_simp rw [hratio] have hfactor : ((lam * r : ℝ≥0) : ℝ) * log ((r : ℝ) / (s : ℝ)) + ((lam * s : ℝ≥0) : ℝ) - ((lam * r : ℝ≥0) : ℝ) = (lam : ℝ) * ((r : ℝ) * log ((r : ℝ) / (s : ℝ)) + (s : ℝ) - (r : ℝ)) := by push_cast ring rw [hfactor] rw [ENNReal.ofReal_mul (by exact_mod_cast (show 0 ≤ lam from lam.property))] simp
FiniteMeasure 1 core · 2 supporting This module identifies the relative entropy of finite marked Poisson laws with scalar intensity times the finite-measure divergence, retaining the total-mass correction. ★ klDiv_finiteMeasureMarkedPoissonLaw_unequal
Unequal-mass finite marked-Poisson divergence
This module identifies the relative entropy of finite marked Poisson laws with scalar intensity times the finite-measure divergence, retaining the total-mass correction.
theorem klDiv_finiteMeasureMarkedPoissonLaw_unequal reviewed
⚑ flagged
Causalean.Mathlib.Probability.Poisson.FinitePartition.UnequalMassKL
On a standard Borel observation space, two finite intensity measures, a shared fallback probability law, a shared real mark law, and a nonnegative scalar intensity imply that the extended-real KL divergence between the two finite-measure marked Poisson laws equals the scalar intensity times the KL divergence between the two intensity measures, where the divergence of finite measures includes the total-mass correction, so unequal total masses are covered.
Formal statement
Proof (Lean source)
theorem klDiv_finiteMeasureMarkedPoissonLaw_unequal
{X : Type*} [MeasurableSpace X] [StandardBorelSpace X]
(ν₁ ν₀ : Measure X) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₀]
(P₀ : Measure X) [IsProbabilityMeasure P₀]
(R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) :
klDiv
(finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam)
(finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam) =
(lam : ℝ≥0∞) * klDiv ν₁ ν₀ := by
/- Unfold each marked law; use `klDiv_finiteMarkedPoissonSampleLaw_unequal`.
Rewrite count KL by `klDiv_poissonMeasure` and scale the rate expression
with `poissonRateKL_mul_left`. The remaining sum is `lam *` the
`klDiv_eq_poissonRateKL_add_normalized` identity; use distributivity.
Do not split on absolute continuity or mass here: those cases are
already covered by the two imported identities, including `0 * ∞`. -/
unfold finiteMeasureMarkedPoissonLaw
rw [klDiv_finiteMarkedPoissonSampleLaw_unequal, klDiv_poissonMeasure,
poissonRateKL_mul_left,
klDiv_eq_poissonRateKL_add_normalized ν₁ ν₀ P₀]
simp only [ENNReal.coe_mul, mul_add, mul_assoc]
2 supporting declarations (lemmas, instances)
-
klDiv_finiteMeasureMarkedPoissonLaw_unequal_ne_toptheorem — Two finite intensity measures, a shared fallback probability law, a shared real mark law, a nonnegative scalar intensity, and a finite scaled divergence imply that the marked-Poisson divergence is finite.Proof (Lean source)
theorem klDiv_finiteMeasureMarkedPoissonLaw_unequal_ne_top {X : Type*} [MeasurableSpace X] [StandardBorelSpace X] (ν₁ ν₀ : Measure X) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₀] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (hRHS : (lam : ℝ≥0∞) * klDiv ν₁ ν₀ ≠ ∞) : klDiv (finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) (finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam) ≠ ∞ := by rw [klDiv_finiteMeasureMarkedPoissonLaw_unequal] exact hRHS -
toReal_klDiv_finiteMeasureMarkedPoissonLaw_unequaltheorem — Two finite intensity measures, a shared fallback probability law, a shared real mark law, and a nonnegative scalar intensity imply that the real-valued marked-Poisson divergence is real intensity times real finite-measure divergence.hypothesesX :ν₁ ν₀ :P₀ :R :lam :ℝ≥0conclusion(klDiv (finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) (finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam)).toRealProof (Lean source)
theorem toReal_klDiv_finiteMeasureMarkedPoissonLaw_unequal {X : Type*} [MeasurableSpace X] [StandardBorelSpace X] (ν₁ ν₀ : Measure X) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₀] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : (klDiv (finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) (finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam)).toReal = (lam : ℝ) * (klDiv ν₁ ν₀).toReal := by rw [klDiv_finiteMeasureMarkedPoissonLaw_unequal] rw [ENNReal.toReal_mul] simp
Marked 1 core · 0 supporting This module factors a finite marked Poisson law through its count and fixed-size conditional sample kernel, then applies the KL chain rule at unequal rates. ★ klDiv_finiteMarkedPoissonSampleLaw_unequal
Marked Poisson divergence at unequal rates
This module factors a finite marked Poisson law through its count and fixed-size conditional sample kernel, then applies the KL chain rule at unequal rates.
theorem klDiv_finiteMarkedPoissonSampleLaw_unequal reviewed
⚑ flagged
Causalean.Mathlib.Probability.Poisson.FinitePartition.UnequalMassKL
On a standard Borel point space, two point probability laws, a shared real mark law, and two nonnegative count rates imply that the extended-real KL divergence between the two finite marked Poisson sample laws equals the KL divergence between the two Poisson count laws plus the first (source) rate times the KL divergence between the point laws.
Formal statement
Proof (Lean source)
theorem klDiv_finiteMarkedPoissonSampleLaw_unequal
{X : Type*} [MeasurableSpace X] [StandardBorelSpace X]
(P Q : Measure X) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
(R : Measure ℝ) [IsProbabilityMeasure R] (r s : ℝ≥0) :
klDiv
(finiteMarkedPoissonSampleLaw P R r)
(finiteMarkedPoissonSampleLaw Q R s) =
klDiv (poissonMeasure r) (poissonMeasure s) +
(r : ℝ≥0∞) * klDiv P Q := by
by_cases hPQ : P ≪ Q
· exact klDiv_finiteMarkedPoissonSampleLaw_of_ac_unequal P Q R r s hPQ
by_cases hr : r = 0
· subst r
rw [klDiv_finiteMarkedPoissonSampleLaw_zero_left]
simp
rw [InformationTheory.klDiv_of_not_ac
(finiteMarkedPoissonSampleLaw_not_ac_of_not_point_ac P Q R r s hr hPQ),
InformationTheory.klDiv_of_not_ac hPQ]
have hr' : (r : ℝ≥0∞) ≠ 0 := by simpa using hr
simp [ENNReal.mul_top hr']