Product Bounds for Bounded Sequences

General lemmas about bounds on products of bounded sequences. These are used in the contractability-based proof of de Finetti's theorem.

Main results

• abs_prod_sub_prod_le: |∏ f - ∏ g| ≤ ∑ |f_j - g_j| when factors bounded by 1

theorem Exchangeability.Util.abs_prod_sub_prod_le {m : ℕ} (f g : Fin m → ℝ) (hf : ∀ (i : Fin m), |f i| ≤ 1) (hg : ∀ (i : Fin m), |g i| ≤ 1) : |∏ i : Fin m, f i - ∏ i : Fin m, g i| ≤ ∑ i : Fin m, |f i - g i|

Telescoping bound: |∏ f - ∏ g| ≤ ∑ |f_j - g_j| when factors are bounded by 1.

This is proved by induction using the identity: ab - cd = a*(b-d) + (a-c)*d