Dependent functions with finite support
For a non-dependent version see data/finsupp.lean.
@[instance]
def
dfinsupp.inhabited_pre
(ι : Type u)
(β : ι → Type v)
[Π (i : ι), has_zero (β i)] :
inhabited (dfinsupp.pre ι β)
Equations
- dfinsupp.inhabited_pre ι β = {default := {to_fun := λ (i : ι), 0, pre_support := ∅, zero := _}}
@[instance]
def
dfinsupp.setoid
(ι : Type u)
(β : ι → Type v)
[Π (i : ι), has_zero (β i)] :
setoid (dfinsupp.pre ι β)
Equations
- dfinsupp.setoid ι β = {r := λ (x y : dfinsupp.pre ι β), ∀ (i : ι), x.to_fun i = y.to_fun i, iseqv := _}
@[instance]
def
dfinsupp.has_coe_to_fun
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)] :
has_coe_to_fun (Π₀ (i : ι), β i)
Equations
- dfinsupp.has_coe_to_fun = {F := λ (_x : Π₀ (i : ι), β i), Π (i : ι), β i, coe := λ (f : Π₀ (i : ι), β i), quotient.lift_on f dfinsupp.pre.to_fun dfinsupp.has_coe_to_fun._proof_1}
@[instance]
def
dfinsupp.has_zero
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)] :
has_zero (Π₀ (i : ι), β i)
@[instance]
def
dfinsupp.inhabited
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)] :
inhabited (Π₀ (i : ι), β i)
Equations
- dfinsupp.inhabited = {default := 0}
@[simp]
def
dfinsupp.map_range
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i) :
(∀ (i : ι), f i 0 = 0) → (Π₀ (i : ι), β₁ i) → (Π₀ (i : ι), β₂ i)
The composition of f : β₁ → β₂ and g : Π₀ i, β₁ i is
map_range f hf g : Π₀ i, β₂ i, well defined when f 0 = 0.
Equations
- dfinsupp.map_range f hf g = quotient.lift_on g (λ (x : dfinsupp.pre ι (λ (i : ι), β₁ i)), ⟦{to_fun := λ (i : ι), f i (x.to_fun i), pre_support := x.pre_support, zero := _}⟧) _
@[simp]
theorem
dfinsupp.map_range_apply
{ι : Type u}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i}
{i : ι} :
⇑(dfinsupp.map_range f hf g) i = f i (⇑g i)
def
dfinsupp.zip_with
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
(f : Π (i : ι), β₁ i → β₂ i → β i) :
(∀ (i : ι), f i 0 0 = 0) → (Π₀ (i : ι), β₁ i) → (Π₀ (i : ι), β₂ i) → (Π₀ (i : ι), β i)
Let f i be a binary operation β₁ i → β₂ i → β i such that f i 0 0 = 0.
Then zip_with f hf is a binary operation Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i.
Equations
- dfinsupp.zip_with f hf g₁ g₂ = quotient.lift_on₂ g₁ g₂ (λ (x : dfinsupp.pre ι (λ (i : ι), β₁ i)) (y : dfinsupp.pre ι (λ (i : ι), β₂ i)), ⟦{to_fun := λ (i : ι), f i (x.to_fun i) (y.to_fun i), pre_support := x.pre_support + y.pre_support, zero := _}⟧) _
@[simp]
theorem
dfinsupp.zip_with_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
{f : Π (i : ι), β₁ i → β₂ i → β i}
{hf : ∀ (i : ι), f i 0 0 = 0}
{g₁ : Π₀ (i : ι), β₁ i}
{g₂ : Π₀ (i : ι), β₂ i}
{i : ι} :
⇑(dfinsupp.zip_with f hf g₁ g₂) i = f i (⇑g₁ i) (⇑g₂ i)
@[instance]
def
dfinsupp.has_add
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)] :
has_add (Π₀ (i : ι), β i)
Equations
- dfinsupp.has_add = {add := dfinsupp.zip_with (λ (_x : ι), has_add.add) dfinsupp.has_add._proof_1}
@[simp]
theorem
dfinsupp.add_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)]
{g₁ g₂ : Π₀ (i : ι), β i}
{i : ι} :
@[instance]
def
dfinsupp.add_monoid
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)] :
add_monoid (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_monoid = {add := has_add.add dfinsupp.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _}
@[instance]
def
dfinsupp.is_add_monoid_hom
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)]
{i : ι} :
is_add_monoid_hom (λ (g : Π₀ (i : ι), β i), ⇑g i)
Equations
@[instance]
def
dfinsupp.has_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)] :
has_neg (Π₀ (i : ι), β i)
Equations
- dfinsupp.has_neg = {neg := λ (f : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_neg.neg) dfinsupp.has_neg._proof_1 f}
@[instance]
def
dfinsupp.add_comm_monoid
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_comm_monoid (β i)] :
add_comm_monoid (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_comm_monoid = {add := add_monoid.add dfinsupp.add_monoid, add_assoc := _, zero := add_monoid.zero dfinsupp.add_monoid, zero_add := _, add_zero := _, add_comm := _}
@[instance]
def
dfinsupp.add_group
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)] :
add_group (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_group = {add := add_monoid.add dfinsupp.add_monoid, add_assoc := _, zero := add_monoid.zero dfinsupp.add_monoid, zero_add := _, add_zero := _, neg := has_neg.neg infer_instance, add_left_neg := _}
@[instance]
def
dfinsupp.add_comm_group
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_comm_group (β i)] :
add_comm_group (Π₀ (i : ι), β i)
Equations
- dfinsupp.add_comm_group = {add := add_group.add dfinsupp.add_group, add_assoc := _, zero := add_group.zero dfinsupp.add_group, zero_add := _, add_zero := _, neg := add_group.neg dfinsupp.add_group, add_left_neg := _, add_comm := _}
def
dfinsupp.to_has_scalar
{ι : Type u}
{β : ι → Type v}
{γ : Type w}
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)] :
has_scalar γ (Π₀ (i : ι), β i)
Dependent functions with finite support inherit a semiring action from an action on each coordinate.
Equations
- dfinsupp.to_has_scalar = {smul := λ (c : γ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_scalar.smul c) _ v}
@[simp]
theorem
dfinsupp.smul_apply
{ι : Type u}
{β : ι → Type v}
{γ : Type w}
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
{i : ι}
{b : γ}
{v : Π₀ (i : ι), β i} :
def
dfinsupp.to_semimodule
{ι : Type u}
{β : ι → Type v}
{γ : Type w}
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)] :
semimodule γ (Π₀ (i : ι), β i)
Dependent functions with finite support inherit a semimodule structure from such a structure on each coordinate.
Equations
- dfinsupp.to_semimodule = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul infer_instance}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
def
dfinsupp.filter
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p] :
(Π₀ (i : ι), β i) → (Π₀ (i : ι), β i)
filter p f is the function which is f i if p i is true and 0 otherwise.
Equations
- dfinsupp.filter p f = quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), ⟦{to_fun := λ (i : ι), ite (p i) (x.to_fun i) 0, pre_support := x.pre_support, zero := _}⟧) _
@[simp]
theorem
dfinsupp.filter_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
{i : ι}
{f : Π₀ (i : ι), β i} :
⇑(dfinsupp.filter p f) i = ite (p i) (⇑f i) 0
theorem
dfinsupp.filter_apply_pos
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
{f : Π₀ (i : ι), β i}
{i : ι} :
p i → ⇑(dfinsupp.filter p f) i = ⇑f i
theorem
dfinsupp.filter_apply_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
{f : Π₀ (i : ι), β i}
{i : ι} :
¬p i → ⇑(dfinsupp.filter p f) i = 0
theorem
dfinsupp.filter_pos_add_filter_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)]
{f : Π₀ (i : ι), β i}
{p : ι → Prop}
[decidable_pred p] :
dfinsupp.filter p f + dfinsupp.filter (λ (i : ι), ¬p i) f = f
def
dfinsupp.subtype_domain
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
(p : ι → Prop)
[decidable_pred p] :
subtype_domain p f is the restriction of the finitely supported function
f to the subtype p.
Equations
- dfinsupp.subtype_domain p f = quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), ⟦{to_fun := λ (i : subtype p), x.to_fun ↑i, pre_support := multiset.map (λ (j : {x_1 // x_1 ∈ multiset.filter p x.pre_support}), ⟨↑j, _⟩) (multiset.filter p x.pre_support).attach, zero := _}⟧) _
@[simp]
theorem
dfinsupp.subtype_domain_zero
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p] :
dfinsupp.subtype_domain p 0 = 0
@[simp]
theorem
dfinsupp.subtype_domain_apply
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), has_zero (β i)]
{p : ι → Prop}
[decidable_pred p]
{i : subtype p}
{v : Π₀ (i : ι), β i} :
⇑(dfinsupp.subtype_domain p v) i = ⇑v i.val
@[simp]
theorem
dfinsupp.subtype_domain_add
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)]
{p : ι → Prop}
[decidable_pred p]
{v v' : Π₀ (i : ι), β i} :
dfinsupp.subtype_domain p (v + v') = dfinsupp.subtype_domain p v + dfinsupp.subtype_domain p v'
@[instance]
def
dfinsupp.subtype_domain.is_add_monoid_hom
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_monoid (β i)]
{p : ι → Prop}
[decidable_pred p] :
Equations
@[simp]
theorem
dfinsupp.subtype_domain_neg
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
{p : ι → Prop}
[decidable_pred p]
{v : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.subtype_domain_sub
{ι : Type u}
{β : ι → Type v}
[Π (i : ι), add_group (β i)]
{p : ι → Prop}
[decidable_pred p]
{v v' : Π₀ (i : ι), β i} :
dfinsupp.subtype_domain p (v - v') = dfinsupp.subtype_domain p v - dfinsupp.subtype_domain p v'
def
dfinsupp.mk
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(s : finset ι) :
Create an element of Π₀ i, β i from a finset s and a function x
defined on this finset.
theorem
dfinsupp.mk_injective
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(s : finset ι) :
def
dfinsupp.single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
(i : ι) :
β i → (Π₀ (i : ι), β i)
The function single i b : Π₀ i, β i sends i to b
and all other points to 0.
Equations
- dfinsupp.single i b = dfinsupp.mk {i} (λ (j : ↥↑{i}), _.rec_on b)
@[simp]
theorem
dfinsupp.single_apply
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i i' : ι}
{b : β i} :
@[simp]
theorem
dfinsupp.single_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι} :
dfinsupp.single i 0 = 0
@[simp]
theorem
dfinsupp.single_eq_same
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι}
{b : β i} :
⇑(dfinsupp.single i b) i = b
theorem
dfinsupp.single_eq_of_ne
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i i' : ι}
{b : β i} :
i ≠ i' → ⇑(dfinsupp.single i b) i' = 0
def
dfinsupp.erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)] :
ι → (Π₀ (i : ι), β i) → (Π₀ (i : ι), β i)
Redefine f i to be 0.
Equations
- dfinsupp.erase i f = quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), ⟦{to_fun := λ (j : ι), ite (j = i) 0 (x.to_fun j), pre_support := x.pre_support, zero := _}⟧) _
@[simp]
theorem
dfinsupp.erase_apply
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i j : ι}
{f : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.erase_same
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i : ι}
{f : Π₀ (i : ι), β i} :
⇑(dfinsupp.erase i f) i = 0
theorem
dfinsupp.erase_ne
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{i i' : ι}
{f : Π₀ (i : ι), β i} :
i' ≠ i → ⇑(dfinsupp.erase i f) i' = ⇑f i'
@[simp]
theorem
dfinsupp.single_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
{i : ι}
{b₁ b₂ : β i} :
dfinsupp.single i (b₁ + b₂) = dfinsupp.single i b₁ + dfinsupp.single i b₂
theorem
dfinsupp.single_add_erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
{i : ι}
{f : Π₀ (i : ι), β i} :
dfinsupp.single i (⇑f i) + dfinsupp.erase i f = f
theorem
dfinsupp.erase_add_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
{i : ι}
{f : Π₀ (i : ι), β i} :
dfinsupp.erase i f + dfinsupp.single i (⇑f i) = f
theorem
dfinsupp.induction
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
{p : (Π₀ (i : ι), β i) → Prop}
(f : Π₀ (i : ι), β i) :
p 0 → (∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), ⇑f i = 0 → b ≠ 0 → p f → p (dfinsupp.single i b + f)) → p f
theorem
dfinsupp.induction₂
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
{p : (Π₀ (i : ι), β i) → Prop}
(f : Π₀ (i : ι), β i) :
p 0 → (∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), ⇑f i = 0 → b ≠ 0 → p f → p (f + dfinsupp.single i b)) → p f
@[simp]
theorem
dfinsupp.mk_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
{s : finset ι}
{x y : Π (i : ↥↑s), β ↑i} :
dfinsupp.mk s (x + y) = dfinsupp.mk s x + dfinsupp.mk s y
@[simp]
theorem
dfinsupp.mk_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
{s : finset ι} :
dfinsupp.mk s 0 = 0
@[simp]
theorem
dfinsupp.mk_neg
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
{s : finset ι}
{x : Π (i : ↥↑s), β i.val} :
dfinsupp.mk s (-x) = -dfinsupp.mk s x
@[simp]
theorem
dfinsupp.mk_sub
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
{s : finset ι}
{x y : Π (i : ↥↑s), β i.val} :
dfinsupp.mk s (x - y) = dfinsupp.mk s x - dfinsupp.mk s y
@[instance]
def
dfinsupp.is_add_group_hom
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
{s : finset ι} :
Equations
@[simp]
theorem
dfinsupp.mk_smul
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
(γ : Type w)
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
{s : finset ι}
{c : γ}
(x : Π (i : ↥↑s), β i.val) :
dfinsupp.mk s (c • x) = c • dfinsupp.mk s x
@[simp]
theorem
dfinsupp.single_smul
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
(γ : Type w)
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
{i : ι}
{c : γ}
{x : β i} :
dfinsupp.single i (c • x) = c • dfinsupp.single i x
def
dfinsupp.lmk
{ι : Type u}
(β : ι → Type v)
[dec : decidable_eq ι]
(γ : Type w)
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
(s : finset ι) :
dfinsupp.mk as a linear_map.
Equations
- dfinsupp.lmk β γ s = {to_fun := dfinsupp.mk s, map_add' := _, map_smul' := _}
def
dfinsupp.lsingle
{ι : Type u}
(β : ι → Type v)
[dec : decidable_eq ι]
(γ : Type w)
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
(i : ι) :
dfinsupp.single as a linear_map
Equations
- dfinsupp.lsingle β γ i = {to_fun := dfinsupp.single i, map_add' := _, map_smul' := _}
@[simp]
theorem
dfinsupp.lmk_apply
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
(γ : Type w)
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
{s : finset ι}
{x : Π (i : ↥↑s), β i.val} :
⇑(dfinsupp.lmk β γ s) x = dfinsupp.mk s x
@[simp]
theorem
dfinsupp.lsingle_apply
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
(γ : Type w)
[semiring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), semimodule γ (β i)]
{i : ι}
{x : β i} :
⇑(dfinsupp.lsingle β γ i) x = dfinsupp.single i x
def
dfinsupp.support
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)] :
(Π₀ (i : ι), β i) → finset ι
Set {i | f x ≠ 0} as a finset.
Equations
- f.support = quotient.lift_on f (λ (x : dfinsupp.pre ι (λ (i : ι), β i)), finset.filter (λ (i : ι), x.to_fun i ≠ 0) x.pre_support.to_finset) dfinsupp.support._proof_1
@[simp]
theorem
dfinsupp.support_mk_subset
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{s : finset ι}
{x : Π (i : ↥↑s), β i.val} :
(dfinsupp.mk s x).support ⊆ s
theorem
dfinsupp.eq_mk_support
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(f : Π₀ (i : ι), β i) :
@[simp]
theorem
dfinsupp.support_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)] :
@[instance]
def
dfinsupp.decidable_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)] :
decidable_pred (eq 0)
Equations
- dfinsupp.decidable_zero = λ (f : Π₀ (i : ι), β i), decidable_of_iff (f.support = ∅) _
theorem
dfinsupp.support_single_ne_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{i : ι}
{b : β i} :
b ≠ 0 → (dfinsupp.single i b).support = {i}
theorem
dfinsupp.support_single_subset
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{i : ι}
{b : β i} :
(dfinsupp.single i b).support ⊆ {i}
theorem
dfinsupp.map_range_def
{ι : Type u}
[dec : decidable_eq ι]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i} :
dfinsupp.map_range f hf g = dfinsupp.mk g.support (λ (i : ↥↑(g.support)), f i.val (⇑g i.val))
@[simp]
theorem
dfinsupp.map_range_single
{ι : Type u}
[dec : decidable_eq ι]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{i : ι}
{b : β₁ i} :
dfinsupp.map_range f hf (dfinsupp.single i b) = dfinsupp.single i (f i b)
theorem
dfinsupp.support_map_range
{ι : Type u}
[dec : decidable_eq ι]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i} :
(dfinsupp.map_range f hf g).support ⊆ g.support
theorem
dfinsupp.zip_with_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i → β i}
{hf : ∀ (i : ι), f i 0 0 = 0}
{g₁ : Π₀ (i : ι), β₁ i}
{g₂ : Π₀ (i : ι), β₂ i} :
theorem
dfinsupp.support_zip_with
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
{f : Π (i : ι), β₁ i → β₂ i → β i}
{hf : ∀ (i : ι), f i 0 0 = 0}
{g₁ : Π₀ (i : ι), β₁ i}
{g₂ : Π₀ (i : ι), β₂ i} :
theorem
dfinsupp.erase_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(i : ι)
(f : Π₀ (i : ι), β i) :
@[simp]
theorem
dfinsupp.support_erase
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
(i : ι)
(f : Π₀ (i : ι), β i) :
(dfinsupp.erase i f).support = f.support.erase i
theorem
dfinsupp.filter_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
dfinsupp.filter p f = dfinsupp.mk (finset.filter p f.support) (λ (i : ↥↑(finset.filter p f.support)), ⇑f i.val)
@[simp]
theorem
dfinsupp.support_filter
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
(dfinsupp.filter p f).support = finset.filter p f.support
theorem
dfinsupp.subtype_domain_def
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
(f : Π₀ (i : ι), β i) :
dfinsupp.subtype_domain p f = dfinsupp.mk (finset.subtype p f.support) (λ (i : ↥↑(finset.subtype p f.support)), ⇑f ↑(i.val))
@[simp]
theorem
dfinsupp.support_subtype_domain
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{p : ι → Prop}
[decidable_pred p]
{f : Π₀ (i : ι), β i} :
(dfinsupp.subtype_domain p f).support = finset.subtype p f.support
theorem
dfinsupp.support_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{g₁ g₂ : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.support_neg
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{f : Π₀ (i : ι), β i} :
theorem
dfinsupp.support_smul
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[ring γ]
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι), module γ (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{b : γ}
{v : Π₀ (i : ι), β i} :
@[instance]
def
dfinsupp.decidable_eq
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), has_zero (β i)]
[Π (i : ι), decidable_eq (β i)] :
decidable_eq (Π₀ (i : ι), β i)
def
dfinsupp.sum
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ] :
(Π₀ (i : ι), β i) → (Π (i : ι), β i → γ) → γ
sum f g is the sum of g i (f i) over the support of f.
def
dfinsupp.prod
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ] :
(Π₀ (i : ι), β i) → (Π (i : ι), β i → γ) → γ
prod f g is the product of g i (f i) over the support of f.
theorem
dfinsupp.prod_map_range_index
{ι : Type u}
[dec : decidable_eq ι]
{γ : Type w}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
[comm_monoid γ]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i}
{h : Π (i : ι), β₂ i → γ} :
(∀ (i : ι), h i 0 = 1) → (dfinsupp.map_range f hf g).prod h = g.prod (λ (i : ι) (b : β₁ i), h i (f i b))
theorem
dfinsupp.sum_map_range_index
{ι : Type u}
[dec : decidable_eq ι]
{γ : Type w}
{β₁ : ι → Type v₁}
{β₂ : ι → Type v₂}
[Π (i : ι), has_zero (β₁ i)]
[Π (i : ι), has_zero (β₂ i)]
[Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π (i : ι), β₁ i → β₂ i}
{hf : ∀ (i : ι), f i 0 = 0}
{g : Π₀ (i : ι), β₁ i}
{h : Π (i : ι), β₂ i → γ} :
(∀ (i : ι), h i 0 = 0) → (dfinsupp.map_range f hf g).sum h = g.sum (λ (i : ι) (b : β₁ i), h i (f i b))
theorem
dfinsupp.sum_zero_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_zero_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_single_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{i : ι}
{b : β i}
{h : Π (i : ι), β i → γ} :
h i 0 = 1 → (dfinsupp.single i b).prod h = h i b
theorem
dfinsupp.sum_single_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{i : ι}
{b : β i}
{h : Π (i : ι), β i → γ} :
h i 0 = 0 → (dfinsupp.single i b).sum h = h i b
theorem
dfinsupp.sum_neg_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_neg_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
@[simp]
theorem
dfinsupp.sum_apply
{ι : Type u}
{β : ι → Type v}
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)}
{i₂ : ι} :
theorem
dfinsupp.support_sum
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)} :
@[simp]
theorem
dfinsupp.sum_zero
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π₀ (i : ι), β i} :
@[simp]
theorem
dfinsupp.sum_add
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π₀ (i : ι), β i}
{h₁ h₂ : Π (i : ι), β i → γ} :
@[simp]
theorem
dfinsupp.sum_neg
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_group γ]
{f : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.sum_add_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_add_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{f g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.sum_sub_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), add_comm_group (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_group γ]
{f g : Π₀ (i : ι), β i}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_finset_sum_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
{α : Type x}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{s : finset α}
{g : α → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.sum_finset_sum_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
{α : Type x}
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{s : finset α}
{g : α → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_sum_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.sum_sum_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
{ι₁ : Type u₁}
[decidable_eq ι₁]
{β₁ : ι₁ → Type v₁}
[Π (i₁ : ι₁), has_zero (β₁ i₁)]
[Π (i : ι₁) (x : β₁ i), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{f : Π₀ (i₁ : ι₁), β₁ i₁}
{g : Π (i₁ : ι₁), β₁ i₁ → (Π₀ (i : ι), β i)}
{h : Π (i : ι), β i → γ} :
@[simp]
theorem
dfinsupp.sum_single
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
[Π (i : ι), add_comm_monoid (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
{f : Π₀ (i : ι), β i} :
f.sum dfinsupp.single = f
theorem
dfinsupp.sum_subtype_domain_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[add_comm_monoid γ]
{v : Π₀ (i : ι), β i}
{p : ι → Prop}
[decidable_pred p]
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.prod_subtype_domain_index
{ι : Type u}
{β : ι → Type v}
[dec : decidable_eq ι]
{γ : Type w}
[Π (i : ι), has_zero (β i)]
[Π (i : ι) (x : β i), decidable (x ≠ 0)]
[comm_monoid γ]
{v : Π₀ (i : ι), β i}
{p : ι → Prop}
[decidable_pred p]
{h : Π (i : ι), β i → γ} :
theorem
dfinsupp.subtype_domain_sum
{ι : Type u}
{β : ι → Type v}
{γ : Type w}
[Π (i : ι), add_comm_monoid (β i)]
{s : finset γ}
{h : γ → (Π₀ (i : ι), β i)}
{p : ι → Prop}
[decidable_pred p] :
dfinsupp.subtype_domain p (s.sum (λ (c : γ), h c)) = s.sum (λ (c : γ), dfinsupp.subtype_domain p (h c))
theorem
dfinsupp.subtype_domain_finsupp_sum
{ι : Type u}
{β : ι → Type v}
{γ : Type w}
{δ : γ → Type x}
[decidable_eq γ]
[Π (c : γ), has_zero (δ c)]
[Π (c : γ) (x : δ c), decidable (x ≠ 0)]
[Π (i : ι), add_comm_monoid (β i)]
{p : ι → Prop}
[decidable_pred p]
{s : Π₀ (c : γ), δ c}
{h : Π (c : γ), δ c → (Π₀ (i : ι), β i)} :
dfinsupp.subtype_domain p (s.sum h) = s.sum (λ (c : γ) (d : δ c), dfinsupp.subtype_domain p (h c d))