LeanMachineLearning

InformationTheory.klDiv_compProd_comap🔗

Lemma

From the authors

The conditional divergence of two kernels which depend on the conditioning variable only through a statistic f is the conditional divergence given f.

Types
  • α : Type u_1mα : MeasurableSpace αA measurable space is a space equipped with a σ-algebra.
  • β : Type u_2mβ : MeasurableSpace β
  • γ : Type u_3mγ : MeasurableSpace γ
Given
  • μ : MeasureTheory.Measure αA measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsFiniteMeasure μA measure μ is called finite if μ univ < ∞.
  • κ : ProbabilityTheory.Kernel β γA kernel from a measurable space α to another measurable space β is a measurable function κ : α → Measure β.ProbabilityTheory.IsFiniteKernel κA kernel is finite if every measure in its image is finite, with a uniform bound.
  • η : ProbabilityTheory.Kernel β γProbabilityTheory.IsFiniteKernel η
  • f : α → β
Assuming
  • hf : Measurable fA function f between measurable spaces is measurable if the preimage of every measurable set is measurable.
Then
klDiv (μ.compProd (κ.comap f hf)) (μ.compProd (η.comap f hf)) =
  klDiv ((MeasureTheory.Measure.map f μ).compProd κ) ((MeasureTheory.Measure.map f μ).compProd η)
Code
lemma klDiv_compProd_comap (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel β γ)
    [IsFiniteKernel κ] [IsFiniteKernel η] {f : α → β} (hf : Measurable f) :
    klDiv (μ ⊗ₘ κ.comap f hf) (μ ⊗ₘ η.comap f hf) = klDiv (μ.map f ⊗ₘ κ) (μ.map f ⊗ₘ η)
Proof
by
  have hg : Measurable fun p : α × γ ↦ (f p.1, p.2) := by fun_prop
  by_cases hac : μ.map f ⊗ₘ κ ≪ μ.map f ⊗ₘ η
  swap
  · rw [klDiv_of_not_ac hac, klDiv_of_not_ac]
    refine fun h ↦ hac ?_
    have := h.map hg
    rwa [Measure.map_compProd_comap, Measure.map_compProd_comap] at this
  let D := (μ.map f ⊗ₘ κ).rnDeriv (μ.map f ⊗ₘ η)
  have hD : Measurable D := Measure.measurable_rnDeriv _ _
  have hDκ : μ.map f ⊗ₘ κ = (μ.map f ⊗ₘ η).withDensity D :=
    (Measure.withDensity_rnDeriv_eq _ _ hac).symm
  -- for every measurable `t`, the sections of the density integrate to `κ (f a) t`, `μ`-a.e.
  have h_sect {t : Set γ} (ht : MeasurableSet t) :
      ∀ᵐ a ∂μ, ∫⁻ c in t, D (f a, c) ∂(η (f a)) = κ (f a) t := by
    refine ae_of_ae_map (p := fun b ↦ ∫⁻ c in t, D (b, c) ∂(η b) = κ b t) hf.aemeasurable ?_
    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
      (Measurable.setLIntegral_kernel_prod_right (f := fun b c ↦ D (b, c)) hD ht)
      (Kernel.measurable_coe κ ht) fun u hu _ ↦ ?_
    have h1 := congrArg (fun ρ : Measure (β × γ) ↦ ρ (u ×ˢ t)) hDκ
    rw [Measure.compProd_apply_prod hu ht, withDensity_apply _ (hu.prod ht),
      Measure.setLIntegral_compProd hD hu ht] at h1
    exact h1.symm
  have h_rect s t (hs : MeasurableSet s) (ht : MeasurableSet t) :
      (μ ⊗ₘ κ.comap f hf) (s ×ˢ t) =
        ((μ ⊗ₘ η.comap f hf).withDensity (D ∘ fun p ↦ (f p.1, p.2))) (s ×ˢ t) := by
    rw [Measure.compProd_apply_prod hs ht, withDensity_apply _ (hs.prod ht),
      Measure.setLIntegral_compProd (hD.comp hg) hs ht]
    refine setLIntegral_congr_fun_ae hs ?_
    filter_upwards [h_sect ht] with a ha _
    simp only [Kernel.comap_apply, Function.comp_apply]
    exact ha.symm
  have key : μ ⊗ₘ κ.comap f hf =
      (μ ⊗ₘ η.comap f hf).withDensity (D ∘ fun p ↦ (f p.1, p.2)) := by
    refine ext_of_generate_finite _ generateFrom_prod.symm isPiSystem_prod ?_ ?_
    · rintro _ ⟨s, hs, t, ht, rfl⟩
      exact h_rect s t hs ht
    · simpa using h_rect Set.univ Set.univ MeasurableSet.univ MeasurableSet.univ
  rw [← Measure.map_compProd_comap μ κ hf, ← Measure.map_compProd_comap μ η hf,
    klDiv_map_of_eq_withDensity_comp hD hg key]

Meaning last changed in v4.34.0-rc2-76-g565f652 (2026-09-10).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Nothing to draw. Its statement rests on no other declaration in this project, and names nothing from a package left unaudited — so the graph is this declaration alone. That is the answer, not a missing picture.

Audit surface: 0 project declarations, 14 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.