English
For every x, the finite sum of the i-th particles of the partition of unity equals 1 minus the finite product over i of (1 − f_i(x)).
Русский
Для каждого x сумма по i компонент разложения по единице равна 1 минус произведение по i из (1 − f_i(x)).
LaTeX
$$$\sum_i f^{\mathrm{POU}}_i(x) = 1 - \prod_i (1 - f_i(x))$$$
Lean4
theorem sum_toPOUFun_eq (x : X) : ∑ᶠ i, f.toPOUFun i x = 1 - ∏ᶠ i, (1 - f i x) :=
by
set s := (f.point_finite x).toFinset
have hs : (s : Set ι) = {i | f i x ≠ 0} := Finite.coe_toFinset _
have A : (support fun i => toPOUFun f i x) ⊆ s := by
rw [hs]
exact fun i hi => f.support_toPOUFun_subset i hi
have B : (mulSupport fun i => 1 - f i x) ⊆ s :=
by
rw [hs, mulSupport_one_sub]
exact fun i => id
classical
letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B, Finset.prod_one_sub_ordered,
sub_sub_cancel]
refine Finset.sum_congr rfl fun i _ => ?_
convert f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
rwa [Finite.mem_toFinset]
