English
There exists a finite set t such that near x, the partition of unity component is equal to the bump function times a finite product of (1 − f_j).
Русский
Существует конечное множество t, такое что в окрестности x компонент разложения по единице равен функции-импульсу, умноженной на конечное произведение (1 − f_j).
LaTeX
$$$\exists t:\ Finset\, ι,\ f.toPartitionOfUnity_i =_{\mathcal{N}(x)} f_i \cdot \prod_{j \in t \text{ with } WellOrderingRel(j,i)} (1 - f_j)$$$
Lean4
/-- The partition of unity defined by a `BumpCovering`.
The partition of unity is given by the formula `g i x = f i x * ∏ᶠ j < i, (1 - f j x)`. In other
words, `g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x)`, so
`∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x)`. If `x ∈ s`, then one of `f j x` equals one, hence the product
of `1 - f j x` vanishes, and `∑ᶠ i, g i x = 1`.
In order to avoid an assumption `LinearOrder ι`, we use `WellOrderingRel` instead of `(<)`. -/
def toPartitionOfUnity : PartitionOfUnity ι X s
where
toFun i := ⟨f.toPOUFun i, f.continuous_toPOUFun i⟩
locallyFinite' := f.locallyFinite.subset f.support_toPOUFun_subset
nonneg' i x := mul_nonneg (f.nonneg i x) (finprod_cond_nonneg fun j _ => sub_nonneg.2 <| f.le_one j x)
sum_eq_one' x
hx := by
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_eq_self]
apply finprod_eq_zero (fun i => 1 - f i x) (f.ind x hx)
· simp only [f.ind_apply x hx, sub_self]
· rw [mulSupport_one_sub]
exact f.point_finite x
sum_le_one'
x := by
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_le_self_iff]
exact finprod_nonneg fun i => sub_nonneg.2 <| f.le_one i x
