theorem CommutingRepetition.abs_sum4_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (f : X → Y → A → B → ℝ) : |∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, f x y a b| ≤ ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, |f x y a b|

Triangle inequality for a four-fold nested finite sum.

theorem CommutingRepetition.sum2_sub {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (f g : A → B → ℝ) : ∑ a : A, ∑ b : B, (f a b - g a b) = ∑ a : A, ∑ b : B, f a b - ∑ a : A, ∑ b : B, g a b

theorem CommutingRepetition.sum2_add {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (f g : A → B → ℝ) : ∑ a : A, ∑ b : B, (f a b + g a b) = ∑ a : A, ∑ b : B, f a b + ∑ a : A, ∑ b : B, g a b

theorem CommutingRepetition.sum2_mul_left {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (c : ℝ) (f : A → B → ℝ) : ∑ a : A, ∑ b : B, c * f a b = c * ∑ a : A, ∑ b : B, f a b

theorem CommutingRepetition.sum3_sub {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (f g : A → B → C → ℝ) : ∑ a : A, ∑ b : B, ∑ c : C, (f a b c - g a b c) = ∑ a : A, ∑ b : B, ∑ c : C, f a b c - ∑ a : A, ∑ b : B, ∑ c : C, g a b c

theorem CommutingRepetition.sum3_div {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (f : A → B → C → ℝ) (d : ℝ) : (∑ a : A, ∑ b : B, ∑ c : C, f a b c) / d = ∑ a : A, ∑ b : B, ∑ c : C, f a b c / d

theorem CommutingRepetition.sum3_swap {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (f : A → B → C → ℝ) : ∑ a : A, ∑ b : B, ∑ c : C, f a b c = ∑ c : C, ∑ a : A, ∑ b : B, f a b c

Move the outermost index of a three-fold nested sum inside.

theorem CommutingRepetition.sum4_swap {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] {D : Type u_4} [Fintype D] (f : A → B → C → D → ℝ) : ∑ a : A, ∑ b : B, ∑ c : C, ∑ d : D, f a b c d = ∑ c : C, ∑ d : D, ∑ a : A, ∑ b : B, f a b c d

Move the outer pair of a four-fold nested sum inside.

theorem CommutingRepetition.abs_prod_sub_prod_le {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (f g : ι → ℝ) (hf0 : ∀ i ∈ s, 0 ≤ f i) (hf1 : ∀ i ∈ s, f i ≤ 1) (hg0 : ∀ i ∈ s, 0 ≤ g i) (hg1 : ∀ i ∈ s, g i ≤ 1) : |∏ i ∈ s, f i - ∏ i ∈ s, g i| ≤ ∑ i ∈ s, |f i - g i|

Telescoping perturbation of a product of [0,1]-valued factors: |∏ f − ∏ g| ≤ ∑ |f − g|. [07_main_theorem.tex, "the second inequality follows by telescoping the product"]