Mathlib.Data.Finsupp.Indicator

Module docstring

{"# Building finitely supported functions off finsets

This file defines Finsupp.indicator to help create finsupps from finsets.

Main declarations

Finsupp.indicator: Turns a map from a Finset into a Finsupp from the entire type. "}

Finsupp.indicator definition

(s : Finset ι) (f : ∀ i ∈ s, α) : ι →₀ α

Full source

/-- Create an element of `ι →₀ α` from a finset `s` and a function `f` defined on this finset. -/
def indicator (s : Finset ι) (f : ∀ i ∈ s, α) : ι →₀ α where
  toFun i :=
    haveI := Classical.decEq ι
    if H : i ∈ s then f i H else 0
  support :=
    haveI := Classical.decEq α
    ({i | f i.1 i.2 ≠ 0} : Finset s).map (Embedding.subtype _)
  mem_support_toFun i := by
    classical simp

Indicator function with finite support

Informal description

Given a finite set $s$ of type $\iota$ and a function $f$ defined on $s$ (i.e., for each $i \in s$, $f$ provides a value in $\alpha$), the function `Finsupp.indicator` constructs a finitely supported function from $\iota$ to $\alpha$ that equals $f(i)$ when $i \in s$ and zero otherwise. The support of this function is the subset of $s$ where $f$ is non-zero.

Finsupp.indicator_of_mem theorem

(hi : i ∈ s) (f : ∀ i ∈ s, α) : indicator s f i = f i hi

Full source

theorem indicator_of_mem (hi : i ∈ s) (f : ∀ i ∈ s, α) : indicator s f i = f i hi :=
  @dif_pos _ (id _) hi _ _ _

Value of Indicator Function on Supporting Set

Informal description

For any element $i$ in a finite set $s \subseteq \iota$ and any function $f$ defined on $s$, the indicator function $\text{indicator}(s, f)$ evaluated at $i$ equals $f(i)$.

Finsupp.indicator_of_not_mem theorem

(hi : i ∉ s) (f : ∀ i ∈ s, α) : indicator s f i = 0

Full source

theorem indicator_of_not_mem (hi : i ∉ s) (f : ∀ i ∈ s, α) : indicator s f i = 0 :=
  @dif_neg _ (id _) hi _ _ _

Indicator Function Vanishes Outside Supporting Set

Informal description

For any element $i$ not in a finite set $s \subseteq \iota$ and any function $f$ defined on $s$, the indicator function $\text{indicator}(s, f)$ evaluated at $i$ equals $0$.

Finsupp.indicator_apply theorem

[DecidableEq ι] : indicator s f i = if hi : i ∈ s then f i hi else 0

Full source

@[simp]
theorem indicator_apply [DecidableEq ι] : indicator s f i = if hi : i ∈ s then f i hi else 0 := by
  simp only [indicator, ne_eq, coe_mk]
  congr

Evaluation of Indicator Function on Finite Support

Informal description

Given a finite set $s \subseteq \iota$, a function $f$ defined on $s$, and an element $i \in \iota$, the indicator function $\text{indicator}(s, f)$ evaluated at $i$ equals $f(i)$ if $i \in s$ and zero otherwise. Here, the condition $i \in s$ is decidable.

Finsupp.indicator_injective theorem

: Injective fun f : ∀ i ∈ s, α => indicator s f

Full source

theorem indicator_injective : Injective fun f : ∀ i ∈ s, α => indicator s f := by
  intro a b h
  ext i hi
  rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]
  exact DFunLike.congr_fun h i

Injectivity of the Indicator Function Construction on Finite Support

Informal description

The map that sends a function $f$ defined on a finite set $s \subseteq \iota$ to the finitely supported indicator function $\text{indicator}(s, f)$ is injective. In other words, if $\text{indicator}(s, f) = \text{indicator}(s, g)$, then $f(i) = g(i)$ for all $i \in s$.

Finsupp.support_indicator_subset theorem

: ((indicator s f).support : Set ι) ⊆ s

Full source

theorem support_indicator_subset : ((indicator s f).support : Set ι) ⊆ s := by
  intro i hi
  rw [mem_coe, mem_support_iff] at hi
  by_contra h
  exact hi (indicator_of_not_mem h _)

Support of Indicator Function is Subset of Defining Set

Informal description

For any finite set $s \subseteq \iota$ and any function $f$ defined on $s$, the support of the finitely supported indicator function $\text{indicator}(s, f)$ is a subset of $s$.

Finsupp.single_eq_indicator theorem

(b : α) : single i b = indicator { i } (fun _ _ => b)

Full source

lemma single_eq_indicator (b : α) : single i b = indicator {i} (fun _ _ => b) := by
  classical
  ext j
  simp [single_apply, indicator_apply, @eq_comm _ j]

Single-Point Function as Indicator on Singleton Set

Informal description

For any element $i \in \alpha$ and any value $b \in M$, the finitely supported function `single i b` is equal to the indicator function on the singleton set $\{i\}$ with constant value $b$. In mathematical notation: $$\text{single } i \, b = \text{indicator}(\{i\}, \lambda \_ \_, b)$$