Finsupp.embDomain_eq_mapDomain
theorem Finsupp.embDomain_eq_mapDomain :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α ↪ β) (v : α →₀ M),
Finsupp.embDomain f v = Finsupp.mapDomain (⇑f) v
The theorem `Finsupp.embDomain_eq_mapDomain` states that for any types `α`, `β` and `M`, with `M` being an additive commutative monoid, and for any injective function `f` from `α` to `β` and any finitely supported function `v` from `α` to `M`, the function obtained by embedding the domain of `v` in `β` using `f` (`Finsupp.embDomain f v`) is equal to the function obtained by mapping the domain of `v` to `β` using `f` (`Finsupp.mapDomain (⇑f) v`). In other words, if we treat an injective function as a regular function, then the processes of embedding the domain and mapping the domain yield the same result.
More concisely: For any injective function `f` and finitely supported function `v`, the embedding of the domain of `v` in `β` using `f` equals the mapping of the domain of `v` to `β` using `f` in the context of additive commutative monoids `M` over types `α` and `β`.
|
Finsupp.filter_apply_pos
theorem Finsupp.filter_apply_pos :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M) {a : α},
p a → (Finsupp.filter p f) a = f a
The theorem `Finsupp.filter_apply_pos` states that for any types `α` and `M` with `M` having a zero element, given a decidable predicate `p` over `α` and a finitely supported function `f` from `α` to `M`, for any element `a` in `α`, if the predicate `p` holds true for `a`, then the value of `Finsupp.filter p f` at `a` is the same as the value of `f` at `a`. Essentially, if the predicate is true for a specific input, the filtering function doesn't change the value of the original function at that input.
More concisely: For any decidable predicate `p` and finitely supported function `f` from a type `α` with zero element, `Finsupp.filter p f a = f a` whenever `p(a)` holds.
|
Finsupp.mapDomain_mapRange
theorem Finsupp.mapDomain_mapRange :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
(f : α → β) (v : α →₀ M) (g : M → N) (h0 : g 0 = 0),
(∀ (x y : M), g (x + y) = g x + g y) →
Finsupp.mapDomain f (Finsupp.mapRange g h0 v) = Finsupp.mapRange g h0 (Finsupp.mapDomain f v)
This theorem states that for any two types `α` and `β`, and two additive commutative monoids `M` and `N`, given a function `f` from `α` to `β`, a finitely supported function `v` from `α` to `M`, and a function `g` from `M` to `N` that preserves the additive structure (i.e., maps 0 to 0 and preserves addition), the operations `mapDomain` and `mapRange` on finitely supported functions commute. This means that you can first map the range of `v` using `g` and then map the domain using `f`, or you can first map the domain of `v` using `f` and then map the range using `g`, and either way, the result will be the same.
More concisely: Given additive commutative monoids M and N, functions f: α → β, g: M → N preserving additive structure, and finitely supported functions v: α → M, the functions g ∘ mapDomain (v) and mapRange (f) ∘ v are equal.
|
Finsupp.equivMapDomain_single
theorem Finsupp.equivMapDomain_single :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (a : α) (b : M),
(Finsupp.equivMapDomain f fun₀ | a => b) = fun₀ | f a => b
The theorem `Finsupp.equivMapDomain_single` states that for any given types `α`, `β` and `M`, where `M` is equipped with a zero element, any equivalence `f` from `α` to `β`, and any elements `a` of `α` and `b` of `M`, mapping the domain of the single-valued function, that assigns `b` to `a` and zero to anything else, using `f` (i.e., applying `Finsupp.equivMapDomain f`) results in a single-valued function that assigns `b` to `f(a)` and zero to anything else. In other words, the resulting function's support is just `{f(a)}` where it assigns `b`, and zero elsewhere.
More concisely: For any equivalence `f` from type `α` to type `β` and any `a ∈ α` and `b ∈ M`, the function `Finsupp.equivMapDomain f (λ (x : α), if h : x = a then b else 0)` is the single-valued function that assigns `b` to `f(a)` and zero elsewhere.
|
Finsupp.mapDomain_comp
theorem Finsupp.mapDomain_comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {v : α →₀ M} {f : α → β}
{g : β → γ}, Finsupp.mapDomain (g ∘ f) v = Finsupp.mapDomain g (Finsupp.mapDomain f v)
This theorem states that for any types `α`, `β`, `γ`, and `M` with `M` being an additive commutative monoid, and any finitely supported function `v` from `α` to `M`, and any functions `f` from `α` to `β` and `g` from `β` to `γ`, the composition of the `f` and `g` functions after mapping the domain of `v` is equal to the result of first mapping the domain of `v` with `f`, and then mapping the domain of the result with `g`. In simple terms, it's stating that the "mapDomain" operation in the context of finitely supported functions is compatible with function composition - a property commonly known as functoriality in mathematics.
More concisely: For any additive commutative monoids M, types α, β, γ, finitely supported functions v from α to M, and functions f : α -> β and g : β -> γ, the map of the composition g . f of the domains of v is equal to the map of f followed by g of the domain of v. In other words, (g . f) ^^ v = g ^^ (f ^^ v).
|
Finsupp.smul_single
theorem Finsupp.smul_single :
∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] (c : R) (a : α)
(b : M), (c • fun₀ | a => b) = fun₀ | a => c • b
This theorem states that for any types `α`, `M`, and `R`, given the fact that `M` is a zero type and there exists a scalar multiplication by zero for `R` and `M`, for any scalar `c` of type `R`, any element `a` of type `α`, and any element `b` of type `M`, scalar multiplication distributes over the function `fun₀` which maps `a` to `b`. More specifically, `c` times the function `fun₀` that maps `a` to `b` equals the function `fun₀` that maps `a` to `c` times `b`. This essentially states the property of scalar multiplication regarding functions in the context of a single function mapping.
More concisely: For any type `α`, scalar ring `R`, zero type `M`, scalar multiplication on `R` and `M`, scalar `c` in `R`, element `a` in `α`, and element `b` in `M`, we have `(c • fun₀ a) = fun₀ a • c • b`, where `fun₀` is the function mapping `a` to `b`.
|
Finsupp.sum_mapDomain_index
theorem Finsupp.sum_mapDomain_index :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
{f : α → β} {s : α →₀ M} {h : β → M → N},
(∀ (b : β), h b 0 = 0) →
(∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) →
(Finsupp.mapDomain f s).sum h = s.sum fun a m => h (f a) m
The theorem `Finsupp.sum_mapDomain_index` states that for any types `α`, `β`, `M`, and `N`, and given an addition-commutative monoid structure on `M` and `N`, a function `f` from `α` to `β`, a finitely supported function `s` from `α` to `M`, and a function `h` from `β` and `M` to `N` satisfying two properties - `h` of `b` and `0` equals `0` for all `b` in `β`, and `h` of `b` and the sum of `m₁` and `m₂` equals the sum of `h` of `b` and `m₁`, and `h` of `b` and `m₂`, for any `b` in `β` and `m₁`, `m₂` in `M`, then the sum of `h` over the map domain of `f` and `s` is equal to the sum of the function taking `a` and `m` to `h` of `f` of `a` and `m`, over the support of `s`.
In simpler terms, this theorem relates the summation of a function `h` over the elements of a finitely supported function `s`, transformed by `f`, to the direct summation of a function over the elements of `s`. The properties of `h` ensure that it interacts well with the addition in `M` and `N`, making the equality hold.
More concisely: For any addition-commutative monoids M and N, function f : α → β, finitely supported function s : α → M, and function h : β × M → N satisfying h(b, 0) = 0 and h(b, m₁ + m₂) = h(b, m₁) + h(b, m₂) for all b and m₁, m₂ in M, the sum of h over the image of s under f equals the sum of the function taking (a, m) to h(f a, m) over the support of s.
|
Finsupp.comapDomain_zero
theorem Finsupp.comapDomain_zero :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β)
(hif : optParam (Set.InjOn f (f ⁻¹' ↑(Finsupp.support 0))) ⋯), Finsupp.comapDomain f 0 hif = 0
This theorem, `Finsupp.comapDomain_zero`, states that for any function `f` mapping from type `α` to type `β`, and for any type `M` equipped with a zero element, if `f` is injective on the preimage of the support of the zero element in the space of finitely supported functions from `β` to `M`, then the comapDomain of `f` and the zero element under this injective condition is the zero element. In other words, it's saying that the operation of comapping the domain of `f` onto the zero element within these conditions will always yield the zero element. The optional parameter `hif` is an injective constraint on `f` that is required for the rewrite operation to apply in the Lean 4 theorem prover.
More concisely: If `f: α → β` is injective on the preimage of the support of the zero element in the space of finitely supported functions from `β` to a type `M` equipped with a zero element, then the comapDomain of `f` and the zero element is the zero element.
|
Finsupp.comapSMul_apply
theorem Finsupp.comapSMul_apply :
∀ {α : Type u_1} {M : Type u_5} {G : Type u_9} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : AddCommMonoid M]
(g : G) (f : α →₀ M) (a : α), (g • f) a = f (g⁻¹ • a)
This theorem states that for any group `G`, a given `g` in `G`, a function `f` from `α` to `M` and any `a` in `α`, the action of `g` on `f` evaluated at `a` is the same as evaluating `f` at `g⁻¹` acting on `a`. Here `α` and `M` are generic types, `G` is a group, `MulAction G α` is a multiplication action of `G` on `α`, and `AddCommMonoid M` suggests that `M` is an additive commutative monoid.
More concisely: For any group `G`, any element `g` in `G`, any function `f` from `α` to `M` (where `α` is a set and `M` is an additive commutative monoid), and any element `a` in `α`, the action of `g` on `f` at `a` is equal to evaluating `f` at the inverse of `g` acting on `a`. In mathematical notation, `(g • f) a = f (g⁻¹ • a)`.
|
Finsupp.mapDomain_support
theorem Finsupp.mapDomain_support :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq β] {f : α → β}
{s : α →₀ M}, (Finsupp.mapDomain f s).support ⊆ Finset.image f s.support
The theorem `Finsupp.mapDomain_support` states that for any two types `α` and `β`, any type `M` that forms an additive commutative monoid, any function `f` from `α` to `β`, and any finitely supported function `s` from `α` to `M`, the support of the function obtained by mapping the domain of `s` using `f` is a subset of the image of the support of `s` under the function `f`. Here, the support of a function is a finitely supported function that represents the set of elements in the domain that map to non-zero values. The image of a set under a function is the set of values the function takes on that set.
More concisely: For any additive commutative monoid M, any function f : α → β, and finitely supported functions s : α → M and t : α → ⊤ with supp s = {x : α | s x ≠ 0} and supp (f ∘ s) ∋ im(x : α | s x ≠ 0), we have im(supp s) ⊆ supp (f ∘ s).
|
Finsupp.mem_graph_iff
theorem Finsupp.mem_graph_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {c : α × M} {f : α →₀ M}, c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0 := by
sorry
The theorem `Finsupp.mem_graph_iff` states that for any types `α` and `M`, where `M` has an instance of Zero, and for any pair `c` of type α × M and finitely supported function `f` of type α →₀ M, the pair `c` is in the graph of `f` if and only if the result of applying `f` to the first element of `c` is equal to the second element of `c` and the second element of `c` is not zero. This theorem essentially gives the condition for a pair to belong to the graph of a finitely supported function.
More concisely: A pair `(a, m)` belongs to the graph of a finitely supported function `f : α →₀ M` if and only if `f a = m` and `m ≠ 0`.
|
Finsupp.mem_splitSupport_iff_nonzero
theorem Finsupp.mem_splitSupport_iff_nonzero :
∀ {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_13} [inst : Zero M] (l : (i : ι) × αs i →₀ M) (i : ι),
i ∈ l.splitSupport ↔ l.split i ≠ 0
The theorem `Finsupp.mem_splitSupport_iff_nonzero` states that for any type `ι`, a type `M` with a zero element, a type function `αs` from `ι`, a finitely supported function `l` from the sigma type `(i : ι) × αs i` to `M`, and an index `i` of type `ι`, `i` is in the split support of `l` if and only if the `i`th component of `l` is non-zero. Essentially, this theorem is providing a condition for membership in the split support set in terms of the non-zeroness of the corresponding component of the function `l`.
More concisely: For any type `ι`, type function `αs` from `ι`, finitely supported function `l` from `(i : ι) × αs i` to a type `M` with a zero element, and `i` in `ι`, `i` is in the split support of `l` if and only if `l i` is non-zero.
|
Finsupp.comapDomain_apply
theorem Finsupp.comapDomain_apply :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β) (l : β →₀ M)
(hf : Set.InjOn f (f ⁻¹' ↑l.support)) (a : α), (Finsupp.comapDomain f l hf) a = l (f a)
The theorem `Finsupp.comapDomain_apply` states that for any types `α`, `β`, and `M` (with `M` being a type with a zero element), given a function `f` from `α` to `β`, a finitely supported function `l` from `β` to `M`, a proof `hf` that `f` is injective on the preimage of the support of `l`, and any element `a` of `α`, the value of `Finsupp.comapDomain f l hf` at `a` is equal to `l` of `f(a)`. In other words, when you apply the finitely supported function derived from `l` and `f` to an element `a`, it's equivalent to applying `l` to the image of `a` under `f`.
More concisely: For injective functions `f: α → β` and finitely supported functions `l: β → M`, `Finsupp.comapDomain f l hf(a) = l (f a)` for all `a ∈ α`.
|
Finsupp.sum_mapDomain_index_addMonoidHom
theorem Finsupp.sum_mapDomain_index_addMonoidHom :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
{f : α → β} {s : α →₀ M} (h : β → M →+ N),
((Finsupp.mapDomain f s).sum fun b m => (h b) m) = s.sum fun a m => (h (f a)) m
This theorem, `Finsupp.sum_mapDomain_index_addMonoidHom`, is about the sum over the domain of a finitely supported function after a mapping. Given types `α`, `β`, `M`, and `N`, with `M` and `N` being additive commutative monoids, and a function `f : α → β`, the theorem states that for any finitely supported function `s : α →₀ M` and an additive monoid homomorphism `h : β → M →+ N`, the sum of applying `h` to each element in the image of `f` applied to the domain of `s` is equal to the sum of applying `h` to each element in `s` after `f` is applied. In other words, the mapping and the summation commute with each other.
More concisely: For any additive commutative monoids M, N, type α, and an additive monoid homomorphism h : β -> M ->+ N, the sum of applying h to the image of a finitely supported function f : α -> β under the domain of another finitely supported function s : α ->₀ M is equal to the sum of applying h to each element in s after applying f.
|
Finsupp.filter_eq_indicator
theorem Finsupp.filter_eq_indicator :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
⇑(Finsupp.filter p f) = {x | p x}.indicator ⇑f
This theorem states that for any type `α`, an additional type `M` that has a zero element, a decidable predicate `p` on `α`, and a finitely supported function `f` from `α` to `M`, the function obtained by applying the `Finsupp.filter` operation on `f` with predicate `p` is equivalent to applying the `Set.indicator` on `f` with the set of elements of `α` satisfying the predicate `p`. In other words, both operations produce the same function that takes an element of `α` and returns the corresponding value of `f` if the element satisfies the predicate `p`, and zero otherwise.
More concisely: For any type `α`, decidable predicate `p` on `α`, and a finitely supported function `f` from `α` to a type `M` with a zero element, `Finsupp.filter p f` equals `Set.indicator {x : α | p x} f`.
|
Finsupp.mapDomain_injective
theorem Finsupp.mapDomain_injective :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
Function.Injective f → Function.Injective (Finsupp.mapDomain f)
The theorem `Finsupp.mapDomain_injective` states that for all types `α`, `β`, and `M`, given an additive commutative monoid instance on `M` and a function `f : α → β`, if the function `f` is injective (meaning that if `f(x)` equals `f(y)` then `x` must equal `y`), then the function `Finsupp.mapDomain f`, which creates a finitely supported function by mapping the domain of `f` and summing the values for each `β` that shares the same `α`, is also injective. Essentially, it says that if distinct inputs to `f` produce distinct outputs, then distinct finitely supported functions also produce distinct outputs under the domain mapping operation.
More concisely: If `f : α → β` is an injective function between types, then `Finsupp.mapDomain f` is an injective function between the corresponding finitely supported functions.
|
Mathlib.Data.Finsupp.Basic._auxLemma.23
theorem Mathlib.Data.Finsupp.Basic._auxLemma.23 :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Finset β} {hf : Set.InjOn f (f ⁻¹' ↑s)} {x : α},
(x ∈ s.preimage f hf) = (f x ∈ s)
The theorem `Mathlib.Data.Finsupp.Basic._auxLemma.23` states that, given any types `α` and `β`, a function `f` from `α` to `β`, a finite set `s` of elements of type `β`, and a property `hf` asserting that `f` is injective on the preimage of `s` under `f`, for every element `x` of type `α`, `x` is in the preimage of `s` under `f` if and only if `f(x)` is in `s`. This theorem essentially describes a property of the preimage of a set under an injective function.
More concisely: Given an injective function `f` from type `α` to type `β` and a finite set `s` of elements in `β`, for every `x` in `α`, `x` is in the preimage of `s` under `f` if and only if `f(x)` is in `s`.
|
Finsupp.equivMapDomain_refl
theorem Finsupp.equivMapDomain_refl :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (l : α →₀ M), Finsupp.equivMapDomain (Equiv.refl α) l = l := by
sorry
This theorem states that for any given type `α` and any module `M` over a ring, if we have a function `l` from `α` to `M` that returns `0` when the input is not in the domain of `l` (denoted as `α →₀ M`), then mapping the domain of `l` to itself using the identity equivalence (i.e., each element is equivalent to itself, represented by `Equiv.refl α`) via the `Finsupp.equivMapDomain` function, results in the original function `l`. In other words, applying the identity equivalence does not change the function.
More concisely: For any type `α` and ring module `M`, the function `Finsupp.equivMapDomain (Equiv.refl _)` applied to a function `l : α →₀ M` equals `l` itself.
|
Finsupp.mapDomain_smul
theorem Finsupp.mapDomain_smul :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} {x : Monoid R} [inst : AddCommMonoid M]
[inst_1 : DistribMulAction R M] {f : α → β} (b : R) (v : α →₀ M),
Finsupp.mapDomain f (b • v) = b • Finsupp.mapDomain f v
The theorem `Finsupp.mapDomain_smul` states that for any types `α`, `β`, `M`, `R`, a monoid `x` on `R`, an additive commutative monoid `M`, and a distributive multiplication action of `R` on `M`, and given a function `f` from `α` to `β`, a scalar `b` from `R`, and a function `v` from `α` to `M` that is finitely supported, the map domain of the scalar multiplication of `b` and `v` is equal to the scalar multiplication of `b` and the map domain of `f` and `v`. In other words, scalar multiplication commutes with the map domain operation.
In mathematical terms, this can be written as for any `f : α → β`, `b : R` and `v : α →₀ M`, we have `Finsupp.mapDomain f (b • v) = b • Finsupp.mapDomain f v`.
More concisely: For any monoid action of a ring `R` on an additive commutative monoid `M`, function `f : α → β`, scalar `b : R`, and finitely supported function `v : α → M`, we have `Finsupp.mapDomain (f :: α → β) (b • v) = b • Finsupp.mapDomain f v`.
|
Finsupp.sum_smul_index_addMonoidHom
theorem Finsupp.sum_smul_index_addMonoidHom :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [inst : AddMonoid M] [inst_1 : AddCommMonoid N]
[inst_2 : DistribSMul R M] {g : α →₀ M} {b : R} {h : α → M →+ N},
((b • g).sum fun a => ⇑(h a)) = g.sum fun i c => (h i) (b • c)
This theorem, `Finsupp.sum_smul_index_addMonoidHom`, provides a version of the `Finsupp.sum_smul_index'` theorem but particularly for bundled additive maps. It states that for any types `α`, `M`, `N`, and `R`, with `M` as an additive monoid, `N` as a commutative additive monoid, and `R` as a distributive scalar multiplication type over `M`, given a finite sum `g` from `α` to `M`, a scalar `b` in `R`, and a map `h` from `α` and `M` to `N`, the scalar multiplication of `b` with `g` then summed using `h` is equal to the sum of `g` applied to the function that maps each index and coefficient to the product of `h` at that index and the scalar multiplication of `b` with that coefficient.
More concisely: For any additive monoid M, commutative additive monoid N, distributive scalar multiplication R over M, finite sum g from α to M, scalar b in R, and map h from α × M to N, the scalar multiplication of b with g followed by h is equal to the sum of g applied to the map that maps each index and coefficient to the product of h at that index and b times that coefficient.
|
Mathlib.Data.Finsupp.Basic._auxLemma.2
theorem Mathlib.Data.Finsupp.Basic._auxLemma.2 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, (a ∈ f.support) = (f a ≠ 0)
This theorem states that for any type `α` and any type `M` equipped with a zero-element (denoted by `Zero M`), given a function `f` from `α` to `M` and an element `a` of type `α`, `a` is in the support of `f` if and only if the function `f` evaluated at `a` is not equal to zero. In mathematical terms, the support of a function is the set of points where the function is not zero. Therefore, this theorem provides a condition to check whether a point is in the support of a function.
More concisely: The theorem asserts that for any function `f` from type `α` to type `M` equipped with a zero-element, an element `a` in `α` is in the support of `f` if and only if `f a ≠ Zero M`.
|
Finsupp.mapDomain_apply
theorem Finsupp.mapDomain_apply :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
Function.Injective f → ∀ (x : α →₀ M) (a : α), (Finsupp.mapDomain f x) (f a) = x a
The theorem `Finsupp.mapDomain_apply` states that for every types `α`, `β`, and `M`, where `M` is endowed with an additive commutative monoid structure, and given an injective function `f` from `α` to `β`, and every finitely supported function `x` from `α` to `M`, and for every element `a` of `α`, applying the function `f` to `a` and then applying the finitely supported function obtained from `mapDomain` applied to `f` and `x`, results in the same value as applying `x` directly to `a`. Essentially, it means that `mapDomain` preserves the values of the original function at each point when the domain mapping function is injective.
More concisely: For an injective function `f:` α --> β, and a finitely supported function `x:` α --> M with an additive commutative monoid structure, the application of `x` to `a` is equal to the application of `(mapDomain f x)` to `(f a)` for every `a` in α.
|
Finsupp.smul_single_one
theorem Finsupp.smul_single_one :
∀ {α : Type u_1} {R : Type u_11} [inst : Semiring R] (a : α) (b : R), (b • fun₀ | a => 1) = fun₀ | a => b := by
sorry
This theorem states that for any types `α` and `R`, where `R` is a semiring, any element `a` of type `α` and `b` of type `R`, the scalar multiplication of `b` and a function from `a` to `1` (denoted as `fun₀ | a => 1`) is equal to a function from `a` to `b` (denoted as `fun₀ | a => b`). In mathematical terms, it's saying that for any scalar `b` and any single-element function mapping to `1`, the scaled function maps to `b` instead.
More concisely: For any semiring `R` and type `α`, the function `fun₀ | a => b` from `α` to `R` is equal to the scalar multiplication of `b` and the constant function `fun₀ | a => 1` from `α` to `R`.
|
Finsupp.equivMapDomain_eq_mapDomain
theorem Finsupp.equivMapDomain_eq_mapDomain :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_13} [inst : AddCommMonoid M] (f : α ≃ β) (l : α →₀ M),
Finsupp.equivMapDomain f l = Finsupp.mapDomain (⇑f) l
This theorem establishes the equality between two methods of mapping the domain of a finitely supported function. Given a bijection `f` between types `α` and `β`, and a finitely supported function `l` from `α` to a monoidal type `M`, the theorem states that `Finsupp.equivMapDomain f l`, which applies the bijection to the support of `l` and the inverse of the bijection to the function values, is equal to `Finsupp.mapDomain (⇑f) l`, which replaces each input of `l` with its image under `f` and sums the results for each `β`.
More concisely: Given a finitely supported function `l` from type `α` to a monoidal type `M`, a bijection `f` between `α` and `β`, the theorem states that `Finsupp.equivMapDomain f l` equals `Finsupp.mapDomain (f.continuous_apply l)`.
|
Finsupp.comapDomain_add_of_injective
theorem Finsupp.comapDomain_add_of_injective :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] {f : α → β} (hf : Function.Injective f)
(v₁ v₂ : β →₀ M), Finsupp.comapDomain f (v₁ + v₂) ⋯ = Finsupp.comapDomain f v₁ ⋯ + Finsupp.comapDomain f v₂ ⋯
This theorem, `Finsupp.comapDomain_add_of_injective`, states that for any injective function `f` mapping from type `α` to `β`, and for any two finitely supported functions `v₁` and `v₂` from `β` to a type `M` equipped with an addition operation and a zero element, the finitely supported function from `α` to `M` obtained by composing the sum of `v₁` and `v₂` with `f` is equal to the sum of the finitely supported functions obtained by composing `v₁` and `v₂` individually with `f`. In simpler words, the composition operation distributes over the addition of finitely supported functions under the condition that the function being composed is injective.
More concisely: For injective functions $f : \alpha \to \beta$ and finitely supported functions $v\_1, v\_2 : \beta \to M$ with $M$ having an addition operation and zero element, $(v\_1 + v\_2) \circ f = v\_1 \circ f + v\_2 \circ f$.
|
Finsupp.graph_injective
theorem Finsupp.graph_injective : ∀ (α : Type u_13) (M : Type u_14) [inst : Zero M], Function.Injective Finsupp.graph
This theorem states that for all types `α` and `M`, where `M` additionally has a zero element, the function `Finsupp.graph` is injective. In other words, given two finitely supported functions `f` and `g` over `α` with values in `M`, if their graphs (i.e., the finite sets of pairs `(a, f a)` and `(a, g a)` with non-zero `f a` and `g a`) are the same, then the functions `f` and `g` are identical. This function is crucial in scenarios where we need to identify a function uniquely by its non-zero values and their corresponding inputs.
More concisely: Given types `α` and `M` with `M` having a zero element, the function `Finsupp.graph` is an injection from the set of finitely supported functions from `α` to `M`.
|
Finsupp.mapDomain_add
theorem Finsupp.mapDomain_add :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {v₁ v₂ : α →₀ M} {f : α → β},
Finsupp.mapDomain f (v₁ + v₂) = Finsupp.mapDomain f v₁ + Finsupp.mapDomain f v₂
The theorem `Finsupp.mapDomain_add` asserts that for any two finitely supported functions `v₁` and `v₂` from a type `α` to a type `M` (under the structure of an additive commutative monoid), and a function `f` from `α` to `β`, the operation of mapping the domain of the sum of `v₁` and `v₂` through `f` is equivalent to the sum of the operations of mapping the domain of `v₁` and `v₂` separately through `f`. In mathematical terms, it captures the property that the mapDomain function distributes over the addition of finitely supported functions.
More concisely: For any additive commutative monoids M and types α and β, given finitely supported functions v₁, v₂ from α to M and a function f from α to β, the map of the domain of v₁ + v₂ along f is equal to the map of the domains of v₁ and v₂ along f added pointwise.
|
Finsupp.coe_smul
theorem Finsupp.coe_smul :
∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] (b : R) (v : α →₀ M),
⇑(b • v) = b • ⇑v
This theorem, `Finsupp.coe_smul`, states that for any types `α`, `M`, and `R` given that `M` has a zero element and `R` and `M` form a scalar multiplication zero class, for any scalar `b` of type `R` and any function `v` from `α` to `M`, the result of applying (or 'coercing') the function resulting from scalar multiplication of `b` and `v` is equivalent to the result of scalar multiplication of `b` and the result of applying `v`. In other words, it describes a property of scalar multiplication with respect to function application which is distributive in nature.
More concisely: For any type `α`, scalar ring `R`, zero element `0` of `R`, and function `v` from `α` to an `R`-module `M`, the coercion of the scalar multiplication of `b` in `R` with the function `v` is equal to the function obtained by applying scalar multiplication to each element in the domain of `v` with `b` and then applying `v`.
|
Finsupp.comapDomain_smul_of_injective
theorem Finsupp.comapDomain_smul_of_injective :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [inst : AddMonoid M] [inst_1 : Monoid R]
[inst_2 : DistribMulAction R M] {f : α → β} (hf : Function.Injective f) (r : R) (v : β →₀ M),
Finsupp.comapDomain f (r • v) ⋯ = r • Finsupp.comapDomain f v ⋯
This theorem, named `Finsupp.comapDomain_smul_of_injective`, states that, for all types `α`, `β`, `M`, and `R`, given an additive monoid structure on `M`, a monoid structure on `R`, and a distributive multiplication action of `R` on `M`, if we have an injective function `f` from `α` to `β`, a scalar `r` from `R`, and a finitely supported function `v` from `β` to `M`, then the result of mapping the scalar multiplication of `r` and `v` through the function `f` using `Finsupp.comapDomain` is the same as first mapping `v` through `f` using `Finsupp.comapDomain` and then performing the scalar multiplication by `r`. In other words, scalar multiplication can be interchanged with the `comapDomain` operation when the function `f` is injective.
More concisely: For injective functions `f` between types `α` and `β`, and finitely supported functions `v` from `β` to an additive monoid `M` with a distributive action of a monoid `R`, the scalar multiplication `r • (Finsupp.comapDomain v f)` is equal to `Finsupp.comapDomain (r • v) f`.
|
Finsupp.mapDomain_equiv_apply
theorem Finsupp.mapDomain_equiv_apply :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α ≃ β} (x : α →₀ M) (a : β),
(Finsupp.mapDomain (⇑f) x) a = x (f.symm a)
The theorem `Finsupp.mapDomain_equiv_apply` states that for all types `α`, `β`, `M` where `M` is an additive commutative monoid, and for all equivariant functions `f : α ≃ β`, if `x` is a finitely supported function from `α` to `M` and `a` is a value in `β`, then applying the function `Finsupp.mapDomain` to `f` and `x` (which results in a new finitely supported function), and then applying this function to `a`, is equivalent to directly applying the original finitely supported function `x` to the inverse image of `a` under the function `f`. In other words, the mapped domain function applied to `a` is equal to the original function applied to the preimage of `a` under the equivalence `f`.
More concisely: For all equivariant functions `f : α ≃ β`, finitely supported functions `x : α →ℙF M`, and values `a : β`, `Finsupp.mapDomain x f a = x (f⁻¹' a)`.
|
Finsupp.support_filter
theorem Finsupp.support_filter :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
(Finsupp.filter p f).support = Finset.filter p f.support
The theorem `Finsupp.support_filter` states that for all types `α` and `M`, given a zero instance for `M`, a predicate `p` on `α` that is decidable, and a function `f` from `α` to `M` with finite support, the support of the function obtained by filtering `f` using `p` (i.e., keeping only those elements of `f` for which `p` holds and setting the rest to zero) is equal to the set obtained by filtering the support of `f` (i.e., the set of `α` where `f` is non-zero) using the same predicate `p`. In other words, applying the filter to the function has the same effect on its support as applying the filter directly to the support set.
More concisely: For any type `α` and decidable predicate `p` on `α`, and given a function `f` from `α` to a type `M` with finite support, the support of the filtered function `\{x | p x ∧ f x ≠ 0\} → ⊤ -> ∫ x, p x → f x` is equal to the filtered set `\{x | p x\} ∩ supp f`.
|
Finsupp.mapDomain_single
theorem Finsupp.mapDomain_single :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {a : α} {b : M},
(Finsupp.mapDomain f fun₀ | a => b) = fun₀ | f a => b
The theorem `Finsupp.mapDomain_single` states that for any types `α`, `β`, and `M`, where `M` is an additive commutative monoid, and any function `f` from `α` to `β`, and any elements `a` of `α` and `b` of `M`, the application of the function `mapDomain` with `f` to a finite support function that only takes value `b` at `a` and zero elsewhere, yields another finite support function that takes the value `b` at `f(a)` and zero elsewhere. In mathematical terms, this can be written as $(\text{{mapDomain}}\, f\, (\lambda x . \text{{if }} x=a \text{{ then }} b \text{{ else }} 0)) (f(a)) = b$.
More concisely: For any additive commutative monoid M, function f from type α to β, and elements a in α and b in M, the application of mapDomain with f to the finite support function that maps a to b and zero elsewhere yields the finite support function that maps f(a) to b and zero elsewhere. In other words, mapDomain (f) (λx. if x = a then b else 0) (fa) = b.
|
Finsupp.smul_single'
theorem Finsupp.smul_single' :
∀ {α : Type u_1} {R : Type u_11} {x : Semiring R} (c : R) (a : α) (b : R),
(c • fun₀ | a => b) = fun₀ | a => c * b
This theorem, `Finsupp.smul_single'`, asserts that for any given types `α` and `R`, with `R` being a semiring, and any elements `c` and `b` of `R` and `a` of `α`, the scalar multiplication of `c` and the function `$\text{fun₀ } | a \Rightarrow b$` (which maps `a` to `b` and all other elements of `α` to zero) is equal to the function `$\text{fun₀ } | a \Rightarrow c * b$`. This essentially means that scalar multiplication distributes over the function, specifically the scalar multiples the value that the function maps to.
More concisely: For any semiring `R`, scalar multiplication by an element `c` of `R` distributes over the function that maps every element `a` of a type `α` to an element `b` of `R`, yielding the function that maps `a` to `c * b` and all other elements of `α` to zero.
|
Finsupp.mapDomain_id
theorem Finsupp.mapDomain_id :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {v : α →₀ M}, Finsupp.mapDomain id v = v
The theorem `Finsupp.mapDomain_id` states that for all types `α` and `M` where `M` is a type with an additive commutative monoid structure, and for all finitely supported functions `v` from `α` to `M`, mapping the identity function over the domain of `v` leaves `v` unchanged. In other words, if you map each element in the domain of `v` to itself (which is what the identity function does), the resulting finitely supported function is the same as the original function `v`.
More concisely: For any type `α` and additive commutative monoid `M`, the function `Finsupp.mapDomain id v` equals `v`, where `id` is the identity function on the domain of `v` and `v` is a finitely supported function from `α` to `M`.
|
Finsupp.distribMulActionHom_ext'
theorem Finsupp.distribMulActionHom_ext' :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N]
{f g : (α →₀ M) →+[R] N},
(∀ (a : α), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) →
f = g
This theorem, `Finsupp.distribMulActionHom_ext'`, establishes an extensionality principle for the distribution of multiplicative actions in the context of finitely supported functions, or `Finsupp`. If we have a semiring `R` and two abelian commutative monoids `M` and `N`, both of which have the structure of an `R`-module (or `R`-distributive multiplicative action), then for any two `R`-module homomorphisms `f` and `g` from `M` to `N`, if they are equal when composed with the `Finsupp.DistribMulActionHom.single` function for every element of the domain `α`, then `f` and `g` must be equal. This essentially states that to establish equality between such `f` and `g`, it suffices to check their equality on the `Finsupp.DistribMulActionHom.single` functions.
More concisely: If `R` is a semiring, and `M` and `N` are commutative abelian monoids with `R`-module structures, then two `R`-module homomorphisms `f` and `g` from `M` to `N` are equal if and only if they agree on the `Finsupp.DistribMulActionHom.single` functions for all elements in the domain `α`.
|