English
If nonzero weights occur only outside a predicate, the weighted sum over the filter equals the full sum.
Русский
Если веса не равны нулю только вне предиката, сумма по фильтру равна полной сумме.
LaTeX
$$$ w i \\neq 0 \\Rightarrow pred i \\text{ false } \\Rightarrow {x \\in s | pred x}.weightedVSubOfPoint p b w = s.weightedVSubOfPoint p b w $$$
Lean4
/-- A weighted sum over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices in `s`
not satisfying `pred` are zero. -/
theorem weightedVSubOfPoint_filter_of_ne (w : ι → k) (p : ι → P) (b : P) {pred : ι → Prop} [DecidablePred pred]
(h : ∀ i ∈ s, w i ≠ 0 → pred i) : {x ∈ s | pred x}.weightedVSubOfPoint p b w = s.weightedVSubOfPoint p b w :=
by
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, sum_filter_of_ne]
intro i hi hne
refine h i hi ?_
intro hw
simp [hw] at hne
