English
Taking the product of an indicator over a larger finset is the same as taking the original function over the original finset: prod_mulIndicator_subset_of_eq_one f g s t h hg.
Русский
Произведение индикации над большим подмножеством равно произведению по меньшему.
LaTeX
$$$\prod i \in t, \operatorname{mulIndicator}(\uparrow s)\, f(i) = \prod i \in s, f(i)$$$
Lean4
/-- Consider a product of `g i (f i)` over a finset. Suppose `g` is a function such as
`n ↦ (· ^ n)`, which maps a second argument of `1` to `1`. Then if `f` is replaced by the
corresponding multiplicative indicator function, the finset may be replaced by a possibly larger
finset without changing the value of the product. -/
@[to_additive /-- Consider a sum of `g i (f i)` over a finset. Suppose `g` is a function such as
`n ↦ (n • ·)`, which maps a second argument of `0` to `0` (or a weighted sum of `f i * h i` or
`f i • h i`, where `f` gives the weights that are multiplied by some other function `h`). Then if
`f` is replaced by the corresponding indicator function, the finset may be replaced by a possibly
larger finset without changing the value of the sum. -/
]
theorem prod_mulIndicator_subset_of_eq_one [One α] (f : ι → α) (g : ι → α → β) {s t : Finset ι} (h : s ⊆ t)
(hg : ∀ a, g a 1 = 1) : ∏ i ∈ t, g i (mulIndicator (↑s) f i) = ∏ i ∈ s, g i (f i) := by
calc
_ = ∏ i ∈ s, g i (mulIndicator (↑s) f i) := by rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
_ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f
