data_processing_inequality

proof body

Tactic-mode proof.

 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
 267            (Finset.single_le_sum hnonneg (by simp) (by simp [hω]))
 268        exact lt_of_lt_of_le hterm hle
 269      have h_ls := log_sum_inequality_fiber p q (fun ω => φ ω = ω')
 270        hp_nonneg hq_nonneg (fun ω hω => hp ω) (fun ω hω => hq ω) hne
 271      have h_term :
 272          (if push_forward p φ ω' > 0 ∧ push_forward q φ ω' > 0 then
 273              push_forward p φ ω' * log (push_forward p φ ω' / push_forward q φ ω')
 274            else 0) =
 275          (∑ ω, if φ ω = ω' then p ω else 0) *
 276            log ((∑ ω, if φ ω = ω' then p ω else 0) / (∑ ω, if φ ω = ω' then q ω else 0)) := by
 277        simp [push_forward, hp', hq']
 278      -- Combine.
 279      simpa [h_term] using h_ls
 280    · -- Empty fiber: both push-forward masses are 0, term is 0.
 281      have hpf : push_forward p φ ω' = 0 := by
 282        unfold push_forward
 283        apply Finset.sum_eq_zero
 284        intro ω _
 285        split_ifs with h
 286        · exact (hne ⟨ω, h⟩).elim
 287        · rfl
 288      have hqf : push_forward q φ ω' = 0 := by
 289        unfold push_forward
 290        apply Finset.sum_eq_zero
 291        intro ω _
 292        split_ifs with h
 293        · exact (hne ⟨ω, h⟩).elim
 294        · rfl
 295      simp [hpf, hqf]
 296  -- Sum the fiber bounds.
 297  have h_sum :
 298      kl_divergence (push_forward p φ) (push_forward q φ) ≤
 299        ∑ ω', ∑ ω, if φ ω = ω' then p ω * log (p ω / q ω) else 0 := by
 300    unfold kl_divergence
 301    apply Finset.sum_le_sum
 302    intro ω' _
 303    exact h_fiber_bound ω'
 304  -- Swap sums and collapse indicators.
 305  have h_swap :
 306      (∑ ω', ∑ ω, if φ ω = ω' then p ω * log (p ω / q ω) else 0) =
 307        ∑ ω, p ω * log (p ω / q ω) := by
 308    rw [Finset.sum_comm]
 309    simp [Finset.sum_ite_eq, Finset.mem_univ]
 310  -- Finish by rewriting KL with positivity.
 311  have h_kl : kl_divergence p q = ∑ ω, p ω * log (p ω / q ω) := by
 312    unfold kl_divergence
 313    apply Finset.sum_congr rfl
 314    intro ω _
 315    simp [hp ω, hq ω]
 316  linarith [h_sum, h_swap, h_kl]
 317
 318/-- **THEOREM**: Free energy monotonicity under coarse-graining.
 319
 320-- ... 5 more lines elided ...