noncomputable def SD {α : Type u_1} [Fintype α] (a : FinPMF α) (b : FinPMF α) : ℝ

Equations

• SD a b = Finset.sum Finset.univ fun (x : α) => |1 / 2 * (a x - b x)|

theorem SD_eq_half_L1 {α : Type u_1} [Fintype α] (a : FinPMF α) (b : FinPMF α) : SD a b = 1 / 2 * ‖⇑a - ⇑b‖_[1]

theorem SD_linear_combination_le {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (a : FinPMF α) (f : α → FinPMF β) (b : FinPMF β) : SD (FinPMF.linear_combination a f) b ≤ Finset.sum Finset.univ fun (x : α) => a x * SD (f x) b

theorem abs_ite (x : ℝ) : |x| = if x ≥ 0 then x else -x

theorem SD_eq_sup_sum_diff {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) (b : FinPMF α) : SD a b = ⨆ (S : Finset α), Finset.sum S fun (x : α) => a x - b x

theorem prb_le_prb_add_sd {α : Type u_1} [Nonempty α] [Fintype α] (a : FinPMF α) (b : FinPMF α) (t : Finset α) : (Finset.sum t fun (x : α) => a x) ≤ (Finset.sum t fun (x : α) => b x) + SD a b