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_le_one: |∏ f| ≤ 1 when all |f i| ≤ 1
• abs_prod_sub_prod_le: |∏ f - ∏ g| ≤ ∑ |f_j - g_j| when factors bounded by 1

theorem Exchangeability.Util.abs_prod_le_one {n : ℕ} (f : Fin n → ℝ) (hf : ∀ (i : Fin n), |f i| ≤ 1) : |∏ i : Fin n, f i| ≤ 1

Helper: |∏ f| ≤ 1 when all |f i| ≤ 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

theorem Exchangeability.Util.abs_sub_le_abs_add (a b : ℝ) : |a - b| ≤ |a| + |b|

Helper: |a - b| ≤ |a| + |b|.