data_processing_inequality

formal source

 233    D(p'‖q') ≤ D(p‖q) where p', q' are push-forwards.
 234
 235    **STATUS**: PROVEN using log-sum inequality on each fiber. -/
 236theorem data_processing_inequality (p q : Ω → ℝ) (φ : Ω → Ω')
 237    (hp : ∀ ω, 0 < p ω) (hq : ∀ ω, 0 < q ω)
 238    (hp_sum : ∑ ω, p ω = 1) (hq_sum : ∑ ω, q ω = 1) :
 239    kl_divergence (push_forward p φ) (push_forward q φ) ≤ kl_divergence p q := by
 240  classical
 241  have hp_nonneg : ∀ ω, 0 ≤ p ω := fun ω => (hp ω).le
 242  have hq_nonneg : ∀ ω, 0 ≤ q ω := fun ω => (hq ω).le
 243  -- Fiberwise log-sum inequality bounds each coarse term.
 244  have h_fiber_bound :
 245      ∀ ω', (if push_forward p φ ω' > 0 ∧ push_forward q φ ω' > 0 then
 246              push_forward p φ ω' * log (push_forward p φ ω' / push_forward q φ ω')
 247            else 0) ≤
 248            ∑ ω, if φ ω = ω' then p ω * log (p ω / q ω) else 0 := by
 249    intro ω'
 250    by_cases hne : ∃ ω, φ ω = ω'
 251    · have hp' : 0 < push_forward p φ ω' := by
 252        obtain ⟨ω, hω⟩ := hne
 253        have hterm : 0 < p ω := hp ω
 254        have hnonneg : ∀ ω, 0 ≤ if φ ω = ω' then p ω else 0 := by
 255          intro ω; split_ifs <;> [exact (hp ω).le, exact le_rfl]
 256        have hle : p ω ≤ push_forward p φ ω' := by
 257          simpa [push_forward, hω] using
 258            (Finset.single_le_sum hnonneg (by simp) (by simp [hω]))
 259        exact lt_of_lt_of_le hterm hle
 260      have hq' : 0 < push_forward q φ ω' := by
 261        obtain ⟨ω, hω⟩ := hne
 262        have hterm : 0 < q ω := hq ω
 263        have hnonneg : ∀ ω, 0 ≤ if φ ω = ω' then q ω else 0 := by
 264          intro ω; split_ifs <;> [exact (hq ω).le, exact le_rfl]
 265        have hle : q ω ≤ push_forward q φ ω' := by
 266          simpa [push_forward, hω] using