Module docstring
{"# Indicator functions and support of a function in groups with zero "}
Set.indicator_mul
theorem
(s : Set ι) (f g : ι → M₀) : indicator s (fun i ↦ f i * g i) = fun i ↦ indicator s f i * indicator s g i
Informal description
For any set $s$ over a type $\iota$ and any functions $f, g \colon \iota \to M₀$ (where $M₀$ is a type with zero), the indicator function of $s$ applied to the pointwise product of $f$ and $g$ is equal to the pointwise product of the indicator functions of $s$ applied to $f$ and $g$ separately. In other words:
\[
\mathbf{1}_s (f \cdot g) = \mathbf{1}_s f \cdot \mathbf{1}_s g,
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.indicator_mul_left
theorem
(s : Set ι) (f g : ι → M₀) : indicator s (fun j ↦ f j * g j) i = indicator s f i * g i
Informal description
For any set $s \subseteq \iota$, functions $f, g \colon \iota \to M_0$ (where $M_0$ is a type with zero), and any $i \in \iota$, the indicator function of $s$ evaluated at the pointwise product $f \cdot g$ at $i$ equals the product of the indicator function of $s$ evaluated at $f$ at $i$ and $g(i)$. That is:
\[
\mathbf{1}_s(f \cdot g)(i) = \mathbf{1}_s(f)(i) \cdot g(i),
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.indicator_mul_right
theorem
(s : Set ι) (f g : ι → M₀) : indicator s (fun j ↦ f j * g j) i = f i * indicator s g i
Informal description
For any set $s$ over a type $\iota$, any functions $f, g \colon \iota \to M₀$ (where $M₀$ is a type with zero), and any element $i \in \iota$, the indicator function of $s$ evaluated at the pointwise product $f \cdot g$ at $i$ equals the product of $f(i)$ and the indicator function of $s$ evaluated at $g$ at $i$. That is:
\[
\mathbf{1}_s(f \cdot g)(i) = f(i) \cdot \mathbf{1}_s(g)(i),
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.indicator_mul_const
theorem
(s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) : s.indicator (f · * a) i = s.indicator f i * a
Full source
lemma indicator_mul_const (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
s.indicator (f · * a) i = s.indicator f i * a := by rw [indicator_mul_left]Informal description
For any set $s \subseteq \iota$, any function $f \colon \iota \to M_0$ (where $M_0$ is a type with zero), any element $a \in M_0$, and any $i \in \iota$, the indicator function of $s$ evaluated at the pointwise product $f \cdot a$ at $i$ equals the product of the indicator function of $s$ evaluated at $f$ at $i$ and $a$. That is:
\[
\mathbf{1}_s(f \cdot a)(i) = \mathbf{1}_s(f)(i) \cdot a,
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.indicator_const_mul
theorem
(s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) : s.indicator (a * f ·) i = a * s.indicator f i
Full source
lemma indicator_const_mul (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
s.indicator (a * f ·) i = a * s.indicator f i := by rw [indicator_mul_right]Informal description
For any set $s$ over a type $\iota$, any function $f \colon \iota \to M₀$ (where $M₀$ is a type with zero), any element $a \in M₀$, and any $i \in \iota$, the indicator function of $s$ evaluated at the pointwise product $a \cdot f$ at $i$ equals the product of $a$ and the indicator function of $s$ evaluated at $f$ at $i$. That is:
\[
\mathbf{1}_s(a \cdot f)(i) = a \cdot \mathbf{1}_s(f)(i),
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.inter_indicator_mul
theorem
(f g : ι → M₀) (i : ι) : (s ∩ t).indicator (fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i
Full source
lemma inter_indicator_mul (f g : ι → M₀) (i : ι) :
(s ∩ t).indicator (fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i := by
rw [← Set.indicator_indicator]
simp_rw [indicator]
split_ifs <;> simpInformal description
For any functions $f, g \colon \iota \to M_0$ (where $M_0$ is a type with zero), any element $i \in \iota$, and any sets $s, t \subseteq \iota$, the indicator function of the intersection $s \cap t$ evaluated at the pointwise product $f \cdot g$ at $i$ equals the product of the indicator function of $s$ evaluated at $f$ at $i$ and the indicator function of $t$ evaluated at $g$ at $i$. That is:
\[
\mathbf{1}_{s \cap t}(f \cdot g)(i) = \mathbf{1}_s(f)(i) \cdot \mathbf{1}_t(g)(i),
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.inter_indicator_one
theorem
: (s ∩ t).indicator (1 : ι → M₀) = s.indicator 1 * t.indicator 1
Full source
lemma inter_indicator_one : (s ∩ t).indicator (1 : ι → M₀) = s.indicator 1 * t.indicator 1 :=
funext fun _ ↦ by simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]; congrInformal description
For any sets $s$ and $t$ over a type $\iota$, the indicator function of the intersection $s \cap t$ applied to the constant function $1$ equals the pointwise product of the indicator functions of $s$ and $t$ applied to $1$. That is:
\[
\mathbf{1}_{s \cap t}(1) = \mathbf{1}_s(1) \cdot \mathbf{1}_t(1),
\]
where $\mathbf{1}_s$ denotes the indicator function of $s$ and $\cdot$ denotes pointwise multiplication.
Set.indicator_prod_one
theorem
{t : Set κ} {j : κ} : (s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j
Full source
lemma indicator_prod_one {t : Set κ} {j : κ} :
(s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j := by
simp_rw [indicator, mem_prod_eq]
split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tautoInformal description
For any sets $s \subseteq \iota$ and $t \subseteq \kappa$, and any elements $i \in \iota$ and $j \in \kappa$, the indicator function of the product set $s \times t$ evaluated at $(i,j)$ equals the product of the indicator functions of $s$ at $i$ and $t$ at $j$. That is, $\mathbf{1}_{s \times t}(i,j) = \mathbf{1}_s(i) \cdot \mathbf{1}_t(j)$.
Set.indicator_eq_zero_iff_not_mem
theorem
: indicator s 1 i = (0 : M₀) ↔ i ∉ s
Full source
lemma indicator_eq_zero_iff_not_mem : indicatorindicator s 1 i = (0 : M₀) ↔ i ∉ s := by
classical simp [indicator_apply, imp_false]Informal description
For a set $s$ over a type $\alpha$ and an element $i \in \alpha$, the indicator function of $s$ evaluated at $i$ equals the zero element of $M₀$ if and only if $i$ does not belong to $s$. In other words, $\mathbf{1}_s(i) = 0 \leftrightarrow i \notin s$.
Set.indicator_eq_one_iff_mem
theorem
: indicator s 1 i = (1 : M₀) ↔ i ∈ s
Full source
lemma indicator_eq_one_iff_mem : indicatorindicator s 1 i = (1 : M₀) ↔ i ∈ s := by
classical simp [indicator_apply, imp_false]Informal description
For a set $s$ over a type $\alpha$ and an element $i \in \alpha$, the indicator function $\mathbf{1}_s(i)$ equals the multiplicative identity $1$ of $M₀$ if and only if $i$ belongs to $s$. In other words, $\mathbf{1}_s(i) = 1 \leftrightarrow i \in s$.
Set.indicator_one_inj
theorem
(h : indicator s (1 : ι → M₀) = indicator t 1) : s = t
Full source
lemma indicator_one_inj (h : indicator s (1 : ι → M₀) = indicator t 1) : s = t := by
ext; simp_rw [← indicator_eq_one_iff_mem M₀, h]Informal description
For any two sets $s$ and $t$ over a type $\alpha$, if the indicator functions $\mathbf{1}_s$ and $\mathbf{1}_t$ (with value $1$ in $M₀$) are equal, then $s = t$.
Function.support_one
theorem
: support (1 : ι → R) = univ
Full source
@[simp] lemma support_one : support (1 : ι → R) = univ := support_const one_ne_zeroInformal description
The support of the constant function $1 : \iota \to R$ (where $1$ is the multiplicative identity in $R$) is equal to the universal set $\text{univ}$ (the set of all elements of type $\iota$).
Function.mulSupport_zero
theorem
: mulSupport (0 : ι → R) = univ
Full source
@[simp] lemma mulSupport_zero : mulSupport (0 : ι → R) = univ := mulSupport_const zero_ne_oneInformal description
For the zero function $0 : \iota \to R$, the multiplicative support is equal to the universal set $\text{univ}$, i.e., $\operatorname{mulSupport} 0 = \text{univ}$.
Function.support_mul_subset_left
theorem
(f g : ι → M₀) : support (fun x ↦ f x * g x) ⊆ support f
Full source
lemma support_mul_subset_left (f g : ι → M₀) : supportsupport (fun x ↦ f x * g x) ⊆ support f :=
fun x hfg hf ↦ hfg <| by simp only [hf, zero_mul]Informal description
For any functions $f, g : \iota \to M_0$ with values in a monoid with zero $M_0$, the support of the pointwise product function $x \mapsto f(x) \cdot g(x)$ is a subset of the support of $f$, i.e., $\mathrm{supp}(f \cdot g) \subseteq \mathrm{supp}(f)$.
Function.support_mul_subset_right
theorem
(f g : ι → M₀) : support (fun x ↦ f x * g x) ⊆ support g
Full source
lemma support_mul_subset_right (f g : ι → M₀) : supportsupport (fun x ↦ f x * g x) ⊆ support g :=
fun x hfg hg => hfg <| by simp only [hg, mul_zero]Informal description
For any functions $f, g : \iota \to M_0$ with values in a monoid with zero $M_0$, the support of the pointwise product function $x \mapsto f(x) \cdot g(x)$ is a subset of the support of $g$, i.e., $\mathrm{supp}(f \cdot g) \subseteq \mathrm{supp}(g)$.
Function.support_mul
theorem
(f g : ι → M₀) : support (fun x ↦ f x * g x) = support f ∩ support g
Full source
@[simp] lemma support_mul (f g : ι → M₀) : support (fun x ↦ f x * g x) = supportsupport f ∩ support g :=
ext fun x ↦ by simp [not_or]Informal description
For any functions $f, g : \iota \to M_0$ with values in a monoid with zero $M_0$, the support of the pointwise product function $x \mapsto f(x) \cdot g(x)$ is equal to the intersection of the supports of $f$ and $g$, i.e., $\mathrm{supp}(f \cdot g) = \mathrm{supp}(f) \cap \mathrm{supp}(g)$.
Function.support_mul'
theorem
(f g : ι → M₀) : support (f * g) = support f ∩ support g
Full source
@[simp] lemma support_mul' (f g : ι → M₀) : support (f * g) = supportsupport f ∩ support g :=
support_mul _ _Informal description
For any functions $f, g : \iota \to M_0$ with values in a monoid with zero $M_0$, the support of the pointwise product function $f \cdot g$ is equal to the intersection of the supports of $f$ and $g$, i.e., $\mathrm{supp}(f \cdot g) = \mathrm{supp}(f) \cap \mathrm{supp}(g)$.
Function.support_pow
theorem
(f : ι → M₀) (hn : n ≠ 0) : support (fun a ↦ f a ^ n) = support f
Full source
@[simp] lemma support_pow (f : ι → M₀) (hn : n ≠ 0) : support (fun a ↦ f a ^ n) = support f := by
ext; exact (pow_eq_zero_iff hn).notInformal description
For any function $f : \iota \to M_0$ with values in a monoid with zero $M_0$ and any nonzero natural number $n$, the support of the function $a \mapsto f(a)^n$ is equal to the support of $f$, i.e., $\{a \in \iota \mid f(a)^n \neq 0\} = \{a \in \iota \mid f(a) \neq 0\}$.
Function.support_pow'
theorem
(f : ι → M₀) (hn : n ≠ 0) : support (f ^ n) = support f
Full source
@[simp] lemma support_pow' (f : ι → M₀) (hn : n ≠ 0) : support (f ^ n) = support f :=
support_pow _ hnInformal description
For any function $f : \iota \to M_0$ with values in a monoid with zero $M_0$ and any nonzero natural number $n$, the support of the $n$-th power function $f^n$ is equal to the support of $f$, i.e., $\mathrm{supp}(f^n) = \mathrm{supp}(f)$.
Function.support_inv
theorem
(f : ι → G₀) : support (fun a ↦ (f a)⁻¹) = support f
Full source
@[simp] lemma support_inv (f : ι → G₀) : support (fun a ↦ (f a)⁻¹) = support f :=
Set.ext fun _ ↦ not_congr inv_eq_zeroInformal description
For any function $f$ from a type $\iota$ to a group with zero $G_0$, the support of the function $a \mapsto (f(a))^{-1}$ is equal to the support of $f$, i.e., $\{a \in \iota \mid f(a)^{-1} \neq 0\} = \{a \in \iota \mid f(a) \neq 0\}$.
Function.support_inv'
theorem
(f : ι → G₀) : support f⁻¹ = support f
Full source
@[simp] lemma support_inv' (f : ι → G₀) : support f⁻¹ = support f := support_inv _Informal description
For any function $f$ from a type $\iota$ to a group with zero $G_0$, the support of the pointwise inverse function $f^{-1}$ is equal to the support of $f$, i.e., $\{a \in \iota \mid f^{-1}(a) \neq 0\} = \{a \in \iota \mid f(a) \neq 0\}$.
Function.support_div
theorem
(f g : ι → G₀) : support (fun a ↦ f a / g a) = support f ∩ support g
Full source
@[simp] lemma support_div (f g : ι → G₀) : support (fun a ↦ f a / g a) = supportsupport f ∩ support g := by
simp [div_eq_mul_inv]Informal description
For any functions $f, g : \iota \to G_0$ with values in a group with zero $G_0$, the support of the pointwise division function $a \mapsto f(a) / g(a)$ is equal to the intersection of the supports of $f$ and $g$, i.e., $\mathrm{supp}(f / g) = \mathrm{supp}(f) \cap \mathrm{supp}(g)$.
Function.support_div'
theorem
(f g : ι → G₀) : support (f / g) = support f ∩ support g
Full source
@[simp] lemma support_div' (f g : ι → G₀) : support (f / g) = supportsupport f ∩ support g :=
support_div _ _Informal description
For any functions $f, g : \iota \to G_0$ with values in a group with zero $G_0$, the support of the pointwise division function $f / g$ is equal to the intersection of the supports of $f$ and $g$, i.e., $\mathrm{supp}(f / g) = \mathrm{supp}(f) \cap \mathrm{supp}(g)$.
Function.mulSupport_one_add
theorem
[AddLeftCancelMonoid R] (f : ι → R) : mulSupport (fun x ↦ 1 + f x) = support f
Full source
lemma mulSupport_one_add [AddLeftCancelMonoid R] (f : ι → R) :
mulSupport (fun x ↦ 1 + f x) = support f :=
Set.ext fun _ ↦ not_congr add_eq_leftInformal description
Let $R$ be a left-cancellative additive monoid and $f : \iota \to R$ be a function. The multiplicative support of the function $x \mapsto 1 + f(x)$ is equal to the support of $f$, i.e., $\{x \mid 1 + f(x) \neq 1\} = \{x \mid f(x) \neq 0\}$.
Function.mulSupport_one_add'
theorem
[AddLeftCancelMonoid R] (f : ι → R) : mulSupport (1 + f) = support f
Full source
lemma mulSupport_one_add' [AddLeftCancelMonoid R] (f : ι → R) : mulSupport (1 + f) = support f :=
mulSupport_one_add fInformal description
Let $R$ be a left-cancellative additive monoid and $f : \iota \to R$ be a function. The multiplicative support of the function $1 + f$ is equal to the support of $f$, i.e., $\{x \mid (1 + f)(x) \neq 1\} = \{x \mid f(x) \neq 0\}$.
Function.mulSupport_add_one
theorem
[AddRightCancelMonoid R] (f : ι → R) : mulSupport (fun x ↦ f x + 1) = support f
Full source
lemma mulSupport_add_one [AddRightCancelMonoid R] (f : ι → R) :
mulSupport (fun x ↦ f x + 1) = support f := Set.ext fun _ ↦ not_congr add_eq_rightInformal description
Let $R$ be a right-cancellative additive monoid and $f : \iota \to R$ be a function. The multiplicative support of the function $x \mapsto f(x) + 1$ is equal to the support of $f$, i.e., $\{x \mid f(x) + 1 \neq 1\} = \{x \mid f(x) \neq 0\}$.
Function.mulSupport_add_one'
theorem
[AddRightCancelMonoid R] (f : ι → R) : mulSupport (f + 1) = support f
Full source
lemma mulSupport_add_one' [AddRightCancelMonoid R] (f : ι → R) : mulSupport (f + 1) = support f :=
mulSupport_add_one fInformal description
Let $R$ be a right-cancellative additive monoid and $f : \iota \to R$ be a function. The multiplicative support of the function $f + 1$ is equal to the support of $f$, i.e., $\{x \mid f(x) + 1 \neq 1\} = \{x \mid f(x) \neq 0\}$.
Function.mulSupport_one_sub'
theorem
[AddGroup R] (f : ι → R) : mulSupport (1 - f) = support f
Full source
lemma mulSupport_one_sub' [AddGroup R] (f : ι → R) : mulSupport (1 - f) = support f := by
rw [sub_eq_add_neg, mulSupport_one_add', support_neg']Informal description
Let $R$ be an additive group and $f : \iota \to R$ be a function. The multiplicative support of the function $1 - f$ is equal to the support of $f$, i.e., $\{x \mid (1 - f)(x) \neq 1\} = \{x \mid f(x) \neq 0\}$.
Function.mulSupport_one_sub
theorem
[AddGroup R] (f : ι → R) : mulSupport (fun x ↦ 1 - f x) = support f
Full source
lemma mulSupport_one_sub [AddGroup R] (f : ι → R) :
mulSupport (fun x ↦ 1 - f x) = support f := mulSupport_one_sub' fInformal description
Let $R$ be an additive group and $f : \iota \to R$ be a function. The multiplicative support of the function $x \mapsto 1 - f(x)$ is equal to the support of $f$, i.e.,
$$\{x \mid 1 - f(x) \neq 1\} = \{x \mid f(x) \neq 0\}.$$