Module docstring
{"# Interaction of big operators with indicator functions "}
Finset.prod_mulIndicator_subset_of_eq_one
theorem
[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)
Full source
/-- 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."]
lemma 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 fInformal description
Let $M$ be a commutative monoid with identity element $1$, and let $\alpha$ and $\beta$ be types. Given functions $f \colon \iota \to \alpha$ and $g \colon \iota \to \alpha \to \beta$ such that $g(a)(1) = 1$ for all $a \in \iota$, and finite subsets $s \subseteq t$ of $\iota$, we have:
\[
\prod_{i \in t} g(i)\left(\text{mulIndicator}_s f (i)\right) = \prod_{i \in s} g(i)(f(i)),
\]
where $\text{mulIndicator}_s f$ is the multiplicative indicator function of $f$ with respect to $s$, defined as:
\[
\text{mulIndicator}_s f (i) =
\begin{cases}
f(i) & \text{if } i \in s, \\
1 & \text{otherwise.}
\end{cases}
\]
Finset.prod_mulIndicator_subset
theorem
(f : ι → β) {s t : Finset ι} (h : s ⊆ t) : ∏ i ∈ t, mulIndicator (↑s) f i = ∏ i ∈ s, f i
Full source
/-- Taking the product of an indicator function over a possibly larger finset is the same as
taking the original function over the original finset. -/
@[to_additive "Summing an indicator function over a possibly larger `Finset` is the same as summing
the original function over the original finset."]
lemma prod_mulIndicator_subset (f : ι → β) {s t : Finset ι} (h : s ⊆ t) :
∏ i ∈ t, mulIndicator (↑s) f i = ∏ i ∈ s, f i :=
prod_mulIndicator_subset_of_eq_one _ (fun _ ↦ id) h fun _ ↦ rflInformal description
Let $M$ be a commutative monoid with identity element $1$, and let $\beta$ be a type. Given a function $f \colon \iota \to \beta$ and finite subsets $s \subseteq t$ of $\iota$, we have:
\[
\prod_{i \in t} \text{mulIndicator}_s f (i) = \prod_{i \in s} f(i),
\]
where $\text{mulIndicator}_s f$ is the multiplicative indicator function of $f$ with respect to $s$, defined as:
\[
\text{mulIndicator}_s f (i) =
\begin{cases}
f(i) & \text{if } i \in s, \\
1 & \text{otherwise.}
\end{cases}
\]
Finset.prod_mulIndicator_eq_prod_filter
theorem
(s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun i ↦ g i ∈ t i] :
∏ i ∈ s, mulIndicator (t i) (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i)
Full source
@[to_additive]
lemma prod_mulIndicator_eq_prod_filter (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ)
[DecidablePred fun i ↦ g i ∈ t i] :
∏ i ∈ s, mulIndicator (t i) (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i) := by
refine (prod_filter_mul_prod_filter_not s (fun i ↦ g i ∈ t i) _).symm.trans <|
Eq.trans (congr_arg₂ (· * ·) ?_ ?_) (mul_one _)
· exact prod_congr rfl fun x hx ↦ mulIndicator_of_mem (mem_filter.1 hx).2 _
· exact prod_eq_one fun x hx ↦ mulIndicator_of_not_mem (mem_filter.1 hx).2 _Informal description
Let $s$ be a finite set of indices of type $\iota$, $f : \iota \to \kappa \to \beta$ a function, $t : \iota \to \text{Set } \kappa$ a family of sets, and $g : \iota \to \kappa$ a function. Then the product over $s$ of the multiplicative indicator functions $\text{mulIndicator}_{t(i)} (f i) (g i)$ equals the product over the subset of $s$ where $g(i) \in t(i)$ of $f i (g i)$.
In mathematical notation:
\[
\prod_{i \in s} \text{mulIndicator}_{t(i)} (f i) (g i) = \prod_{\substack{i \in s \\ g(i) \in t(i)}} f i (g i).
\]
Finset.prod_mulIndicator_eq_prod_inter
theorem
[DecidableEq ι] (s t : Finset ι) (f : ι → β) : ∏ i ∈ s, (t : Set ι).mulIndicator f i = ∏ i ∈ s ∩ t, f i
Full source
@[to_additive]
lemma prod_mulIndicator_eq_prod_inter [DecidableEq ι] (s t : Finset ι) (f : ι → β) :
∏ i ∈ s, (t : Set ι).mulIndicator f i = ∏ i ∈ s ∩ t, f i := by
rw [← filter_mem_eq_inter, prod_mulIndicator_eq_prod_filter]; rflInformal description
Let $s$ and $t$ be finite sets of type $\iota$ with decidable equality, and let $f \colon \iota \to \beta$ be a function where $\beta$ is a commutative monoid. Then the product over $s$ of the multiplicative indicator functions of $f$ with respect to $t$ equals the product of $f$ over the intersection $s \cap t$.
In mathematical notation:
\[
\prod_{i \in s} \text{mulIndicator}_t f (i) = \prod_{i \in s \cap t} f(i),
\]
where the multiplicative indicator function is defined as:
\[
\text{mulIndicator}_t f (i) =
\begin{cases}
f(i) & \text{if } i \in t, \\
1 & \text{otherwise.}
\end{cases}
\]
Finset.mulIndicator_prod
theorem
(s : Finset ι) (t : Set κ) (f : ι → κ → β) : mulIndicator t (∏ i ∈ s, f i) = ∏ i ∈ s, mulIndicator t (f i)
Full source
@[to_additive]
lemma mulIndicator_prod (s : Finset ι) (t : Set κ) (f : ι → κ → β) :
mulIndicator t (∏ i ∈ s, f i) = ∏ i ∈ s, mulIndicator t (f i) :=
map_prod (mulIndicatorHom _ _) _ _Informal description
Let $s$ be a finite set of indices of type $\iota$, $t$ a subset of $\kappa$, and $f : \iota \to \kappa \to \beta$ a function where $\beta$ is a commutative monoid. Then the multiplicative indicator function of $t$ applied to the product of $f$ over $s$ equals the product over $s$ of the multiplicative indicator functions of $t$ applied to $f i$.
In mathematical notation:
\[
\text{mulIndicator}_t \left( \prod_{i \in s} f i \right) = \prod_{i \in s} \text{mulIndicator}_t (f i).
\]
Finset.mulIndicator_biUnion
theorem
(s : Finset ι) (t : ι → Set κ) {f : κ → β} (hs : (s : Set ι).PairwiseDisjoint t) :
mulIndicator (⋃ i ∈ s, t i) f = fun a ↦ ∏ i ∈ s, mulIndicator (t i) f a
Full source
@[to_additive]
lemma mulIndicator_biUnion (s : Finset ι) (t : ι → Set κ) {f : κ → β}
(hs : (s : Set ι).PairwiseDisjoint t) :
mulIndicator (⋃ i ∈ s, t i) f = fun a ↦ ∏ i ∈ s, mulIndicator (t i) f a := by
induction s using Finset.cons_induction with
| empty => simp
| cons i s hi ih =>
ext j
rw [coe_cons, Set.pairwiseDisjoint_insert_of_not_mem (Finset.mem_coe.not.2 hi)] at hs
classical
rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_not_mem_inter, ih hs.1]
exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)Informal description
Let $s$ be a finite set of indices of type $\iota$, $t \colon \iota \to \mathcal{P}(\kappa)$ a family of subsets of $\kappa$, and $f \colon \kappa \to \beta$ a function where $\beta$ is a commutative monoid. If the family $t$ is pairwise disjoint on $s$ (i.e., for any distinct $i, j \in s$, $t(i) \cap t(j) = \emptyset$), then the multiplicative indicator function of the union $\bigcup_{i \in s} t(i)$ applied to $f$ equals the pointwise product over $s$ of the multiplicative indicator functions of $t(i)$ applied to $f$.
In mathematical notation:
\[
\text{mulIndicator}_{\bigcup_{i \in s} t(i)} f = \left( a \mapsto \prod_{i \in s} \text{mulIndicator}_{t(i)} f (a) \right),
\]
where the multiplicative indicator function is defined as:
\[
\text{mulIndicator}_S f (a) =
\begin{cases}
f(a) & \text{if } a \in S, \\
1 & \text{otherwise.}
\end{cases}
\]
Finset.mulIndicator_biUnion_apply
theorem
(s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (s : Set ι).PairwiseDisjoint t) (x : κ) :
mulIndicator (⋃ i ∈ s, t i) f x = ∏ i ∈ s, mulIndicator (t i) f x
Full source
@[to_additive]
lemma mulIndicator_biUnion_apply (s : Finset ι) (t : ι → Set κ) {f : κ → β}
(h : (s : Set ι).PairwiseDisjoint t) (x : κ) :
mulIndicator (⋃ i ∈ s, t i) f x = ∏ i ∈ s, mulIndicator (t i) f x := by
rw [mulIndicator_biUnion s t h]Informal description
Let $s$ be a finite set of indices of type $\iota$, $t \colon \iota \to \mathcal{P}(\kappa)$ a family of subsets of $\kappa$, and $f \colon \kappa \to \beta$ a function where $\beta$ is a commutative monoid. If the family $t$ is pairwise disjoint on $s$ (i.e., for any distinct $i, j \in s$, $t(i) \cap t(j) = \emptyset$), then for any $x \in \kappa$, the multiplicative indicator function of the union $\bigcup_{i \in s} t(i)$ evaluated at $x$ equals the product over $s$ of the multiplicative indicator functions of $t(i)$ evaluated at $x$.
In mathematical notation:
\[
\text{mulIndicator}_{\bigcup_{i \in s} t(i)} f (x) = \prod_{i \in s} \text{mulIndicator}_{t(i)} f (x),
\]
where the multiplicative indicator function is defined as:
\[
\text{mulIndicator}_S f (x) =
\begin{cases}
f(x) & \text{if } x \in S, \\
1 & \text{otherwise.}
\end{cases}
\]