Comparing two products of elements of the unit ball

For families taking values in the closed unit ball of a seminormed commutative ring, the difference of the products is controlled by the sum of the pointwise differences:

‖∏ i ∈ s, a i - ∏ i ∈ s, b i‖ ≤ ∑ i ∈ s, ‖a i - b i‖

Only ‖a i‖ ≤ 1 and ‖b i‖ ≤ 1 are needed; the argument uses subadditivity and submultiplicativity of the norm and nothing else, so it holds over ℂ as well as ℝ, and norm definiteness is never used — hence SeminormedCommRing rather than NormedCommRing. The unit-ball bound is what makes the constant 1; the same telescoping argument with a uniform bound C gives C ^ (s.card - 1) and is not needed here.

abs_prod_sub_prod_le_sum_abs_sub is the real-valued corollary, phrased with |·|, which is the form the probability consumers use.

This is the elementary step that turns coordinatewise convergence of finitely many bounded observables into convergence of their product, without Hölder or dominated-convergence machinery. It is motivated by TauCetiRoadmap/Exchangeability/README.md, Layer 3 (the L² averaging library and the standard-Borel de Finetti route): both that route and the Layer 5 Koopman route reduce a block factorization to convergence of a product of finitely many block averages.

theorem TauCeti.norm_prod_le_one {ι : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormOneClass R] {s : Finset ι} {b : ι → R} (hb : ∀ i ∈ s, ‖b i‖ ≤ 1) : ‖∏ i ∈ s, b i‖ ≤ 1

A finite product of unit-ball elements lies in the unit ball. Mathlib's Finset.norm_prod_le gives this over a NormedCommRing, but only submultiplicativity of the norm and ‖1‖ = 1 are used, so it holds over a seminormed ring.

theorem TauCeti.norm_prod_sub_prod_le_sum_norm_sub {ι : Type u_1} {R : Type u_2} [SeminormedCommRing R] [NormOneClass R] (s : Finset ι) {a b : ι → R} (ha : ∀ i ∈ s, ‖a i‖ ≤ 1) (hb : ∀ i ∈ s, ‖b i‖ ≤ 1) : ‖∏ i ∈ s, a i - ∏ i ∈ s, b i‖ ≤ ∑ i ∈ s, ‖a i - b i‖

Telescoping bound for a product of unit-ball elements. If ‖a i‖ ≤ 1 and ‖b i‖ ≤ 1 for every i ∈ s, then the difference of the products is at most the sum of the pointwise differences.

theorem TauCeti.abs_prod_sub_prod_le_sum_abs_sub {ι : Type u_1} (s : Finset ι) {a b : ι → ℝ} (ha : ∀ i ∈ s, |a i| ≤ 1) (hb : ∀ i ∈ s, |b i| ≤ 1) : |∏ i ∈ s, a i - ∏ i ∈ s, b i| ≤ ∑ i ∈ s, |a i - b i|

Real-valued form, phrased with |·|: the shape the probability consumers use, where the factors are block averages and conditional expectations of indicators, all in [0, 1].