Interaction of big operators with indicator functions

theorem Finset.prod_mulIndicator_subset_of_eq_one {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid β] [One α] (f : ι → α) (g : ι → α → β) {s t : Finset ι} (h : s ⊆ t) (hg : ∀ (a : ι), g a 1 = 1) : ∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)

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.

theorem Finset.sum_indicator_subset_of_eq_zero {ι : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Zero α] (f : ι → α) (g : ι → α → β) {s t : Finset ι} (h : s ⊆ t) (hg : ∀ (a : ι), g a 0 = 0) : ∑ i ∈ t, g i ((↑s).indicator f i) = ∑ i ∈ s, g i (f i)

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 Finset.prod_mulIndicator_subset {ι : Type u_1} {β : Type u_4} [CommMonoid β] (f : ι → β) {s t : Finset ι} (h : s ⊆ t) : ∏ i ∈ t, (↑s).mulIndicator f i = ∏ i ∈ s, f i

Taking the product of an indicator function over a possibly larger finset is the same as taking the original function over the original finset.

theorem Finset.sum_indicator_subset {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] (f : ι → β) {s t : Finset ι} (h : s ⊆ t) : ∑ i ∈ t, (↑s).indicator f i = ∑ i ∈ s, f i

Summing an indicator function over a possibly larger Finset is the same as summing the original function over the original finset.

theorem Finset.prod_mulIndicator_eq_prod_filter {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun (i : ι) => g i ∈ t i] : ∏ i ∈ s, (t i).mulIndicator (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i)

theorem Finset.sum_indicator_eq_sum_filter {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun (i : ι) => g i ∈ t i] : ∑ i ∈ s, (t i).indicator (f i) (g i) = ∑ i ∈ s with g i ∈ t i, f i (g i)

theorem Finset.prod_mulIndicator_eq_prod_inter {ι : Type u_1} {β : Type u_4} [CommMonoid β] [DecidableEq ι] (s t : Finset ι) (f : ι → β) : ∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i

theorem Finset.sum_indicator_eq_sum_inter {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] [DecidableEq ι] (s t : Finset ι) (f : ι → β) : ∑ i ∈ s, (↑t).indicator f i = ∑ i ∈ s ∩ t, f i

theorem Finset.mulIndicator_prod {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (s : Finset ι) (t : Set κ) (f : ι → κ → β) : t.mulIndicator (∏ i ∈ s, f i) = ∏ i ∈ s, t.mulIndicator (f i)

theorem Finset.indicator_sum {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (t : Set κ) (f : ι → κ → β) : t.indicator (∑ i ∈ s, f i) = ∑ i ∈ s, t.indicator (f i)

theorem Finset.mulIndicator_biUnion {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β} (hs : (↑s).PairwiseDisjoint t) : (⋃ i ∈ s, t i).mulIndicator f = fun (a : κ) => ∏ i ∈ s, (t i).mulIndicator f a

theorem Finset.indicator_biUnion {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β} (hs : (↑s).PairwiseDisjoint t) : (⋃ i ∈ s, t i).indicator f = fun (a : κ) => ∑ i ∈ s, (t i).indicator f a

theorem Finset.mulIndicator_biUnion_apply {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (↑s).PairwiseDisjoint t) (x : κ) : (⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x

theorem Finset.indicator_biUnion_apply {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (↑s).PairwiseDisjoint t) (x : κ) : (⋃ i ∈ s, t i).indicator f x = ∑ i ∈ s, (t i).indicator f x