Symmetric Absolute Difference and Supporting Lemmas for ℝ≥0∞

This file defines ENNReal.absDiff, a symmetric absolute difference on extended non-negative reals using truncating subtraction, and proves supporting lemmas about tsum and absDiff interactions. These are the building blocks for total variation distance on PMF.

Main definitions

• ENNReal.absDiff a b — (a - b) + (b - a), a symmetric absolute difference in ℝ≥0∞

Main results

• ENNReal.absDiff_toReal — connection to real-valued absolute difference
• ENNReal.absDiff_triangle — triangle inequality
• ENNReal.absDiff_tsum_le — subadditivity of absDiff over infinite sums
• ENNReal.absDiff_mul_right_le — |ac - bc| ≤ |a - b| · c
• ENNReal.tsum_fiber — fiber decomposition for ℝ≥0∞-valued sums

noncomputable def ENNReal.absDiff (a b : ENNReal) : ENNReal

Symmetric absolute difference in ℝ≥0∞, defined via truncating subtraction. Satisfies absDiff a b = |a.toReal - b.toReal| when both are finite.

@[simp]

theorem ENNReal.absDiff_self (a : ENNReal) : a.absDiff a = 0

theorem ENNReal.absDiff_comm (a b : ENNReal) : a.absDiff b = b.absDiff a

theorem ENNReal.absDiff_le_add (a b : ENNReal) : a.absDiff b ≤ a + b

theorem ENNReal.absDiff_triangle (a b c : ENNReal) : a.absDiff c ≤ a.absDiff b + b.absDiff c

theorem ENNReal.absDiff_toReal {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : (a.absDiff b).toReal = |a.toReal - b.toReal|

theorem ENNReal.absDiff_tsub_tsub {a b c : ENNReal} (ha : a ≤ c) (hb : b ≤ c) (hc : c ≠ ⊤) : (c - a).absDiff (c - b) = a.absDiff b

@[simp]

theorem ENNReal.absDiff_eq_zero {a b : ENNReal} : a.absDiff b = 0 ↔ a = b

Tsum inequalities

theorem ENNReal.tsum_tsub_le_tsum_tsub {α : Type u_1} (a b : α → ENNReal) : ∑' (x : α), a x - ∑' (x : α), b x ≤ ∑' (x : α), (a x - b x)

theorem ENNReal.absDiff_tsum_le {α : Type u_1} (a b : α → ENNReal) : (∑' (x : α), a x).absDiff (∑' (x : α), b x) ≤ ∑' (x : α), (a x).absDiff (b x)

Multiplication inequality

theorem ENNReal.absDiff_mul_right_le (a b c : ENNReal) : (a * c).absDiff (b * c) ≤ a.absDiff b * c

Fiber decomposition

theorem ENNReal.tsum_fiber {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (g : α → ENNReal) : (∑' (y : β) (x : α), if f x = y then g x else 0) = ∑' (x : α), g x