English
A partition of unity defined by a bump covering assigns to each i a real-valued function g_i given by g_i(x) = f_i(x) ∏ᶠ j WellOrderingRel j i (1 − f_j(x)).
Русский
Разбиение единиц, определяемое по.bump-покрытию, задаёт для каждого i вещественную функцию g_i(x) = f_i(x) ∏ᶠ j WellOrderingRel j i (1 − f_j(x)).
LaTeX
$$$$ g_i(x) = f_i(x) \cdot \prod^{\mathrm{WO}}_{j} (1 - f_j(x)). $$$$
Lean4
/-- Partition of unity defined by a `BumpCovering`. We use this auxiliary definition to prove some
properties of the new family of functions before bundling it into a `PartitionOfUnity`. Do not use
this definition, use `BumpCovering.toPartitionOfUnity` instead.
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 toPOUFun (i : ι) (x : X) : ℝ :=
f i x * ∏ᶠ (j) (_ : WellOrderingRel j i), (1 - f j x)
