English
In a NormedCommRing, for a finite t, ‖∏_{i∈t} (1+f_i) − 1‖ ≤ exp(∑_{i∈t} ‖f_i‖) − 1.
Русский
В нормированном кольце произведение ≈ 1 с bound: ‖∏(1+f_i) − 1‖ ≤ exp(∑ ‖f_i‖) − 1.
LaTeX
$$$\left\|\prod_{i\in t} (1+f_i) - 1\right\| \le \exp\left(\sum_{i\in t} \|f_i\|\right) - 1$$$
Lean4
theorem norm_prod_one_add_sub_one_le (t : Finset ι) (f : ι → R) :
‖∏ i ∈ t, (1 + f i) - 1‖ ≤ Real.exp (∑ i ∈ t, ‖f i‖) - 1 := by
classical
induction t using Finset.induction_on with
| empty => simp
| insert x t hx
IH =>
rw [Finset.prod_insert hx, Finset.sum_insert hx, Real.exp_add,
show (1 + f x) * ∏ i ∈ t, (1 + f i) - 1 = (∏ i ∈ t, (1 + f i) - 1) + f x * ∏ x ∈ t, (1 + f x) by ring]
refine (norm_add_le_of_le IH (norm_mul_le _ _)).trans ?_
generalize h : Real.exp (∑ i ∈ t, ‖f i‖) = A at ⊢ IH
rw [sub_add_eq_add_sub, sub_le_sub_iff_right]
transitivity A + ‖f x‖ * A
· gcongr
rw [← sub_add_cancel (∏ x ∈ t, (1 + f x)) 1]
refine (norm_add_le _ _).trans <| (add_le_add_right IH _).trans ?_
rw [norm_one, sub_add_cancel]
rw [← one_add_mul, add_comm]
exact mul_le_mul_of_nonneg_right (Real.add_one_le_exp _) (h ▸ Real.exp_nonneg _)
