Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".
License: APACHE
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
Type of functions with finite support.
Functions with finite support provide the basis for the following concrete instances:
* ℕ →₀ α: Polynomials (where α is a ring)
* (σ →₀ ℕ) →₀ α: Multivariate Polynomials (again α is a ring, and σ are variable names)
* α →₀ ℕ: Multisets
* α →₀ ℤ: Abelian groups freely generated by α
* β →₀ α: Linear combinations over β where α is the scalar ring
Most of the theory assumes that the range is a commutative monoid. This gives us the big sum
operator as a powerful way to construct `finsupp` elements.
A general advice is to not use α →₀ β directly, as the type class setup might not be fitting.
The best is to define a copy and select the instances best suited.
-/
import data.finset data.set.finite algebra.big_operators algebra.module
noncomputable theory
open_locale classical
open finset
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ι : Type*}
{α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*}
/-- `finsupp α β`, denoted `α →₀ β`, is the type of functions `f : α → β` such that
`f x = 0` for all but finitely many `x`. -/
structure finsupp (α : Type*) (β : Type*) [has_zero β] :=
(support : finset α)
(to_fun : α → β)
(mem_support_to_fun : ∀a, a ∈ support ↔ to_fun a ≠ 0)
infixr ` →₀ `:25 := finsupp
namespace finsupp
section basic
variable [has_zero β]
instance : has_coe_to_fun (α →₀ β) := ⟨λ_, α → β, finsupp.to_fun⟩
instance : has_zero (α →₀ β) := ⟨⟨∅, (λ_, 0), λ _, ⟨false.elim, λ H, H rfl⟩⟩⟩
@[simp] lemma zero_apply {a : α} : (0 : α →₀ β) a = 0 := rfl
@[simp] lemma support_zero : (0 : α →₀ β).support = ∅ := rfl
instance : inhabited (α →₀ β) := ⟨0⟩
@[simp] lemma mem_support_iff {f : α →₀ β} : ∀{a:α}, a ∈ f.support ↔ f a ≠ 0 :=
f.mem_support_to_fun
lemma not_mem_support_iff {f : α →₀ β} {a} : a ∉ f.support ↔ f a = 0 :=
not_iff_comm.1 mem_support_iff.symm
@[ext]
lemma ext : ∀{f g : α →₀ β}, (∀a, f a = g a) → f = g
| ⟨s, f, hf⟩ ⟨t, g, hg⟩ h :=
begin
have : f = g, { funext a, exact h a },
subst this,
have : s = t, { ext a, exact (hf a).trans (hg a).symm },
subst this
end
lemma ext_iff {f g : α →₀ β} : f = g ↔ (∀a:α, f a = g a) :=
⟨by rintros rfl a; refl, ext⟩
@[simp] lemma support_eq_empty {f : α →₀ β} : f.support = ∅ ↔ f = 0 :=
⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext.1 h a).1 $
mem_support_iff.2 H, by rintro rfl; refl⟩
instance finsupp.decidable_eq [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a))
⟨assume ⟨h₁, h₂⟩, ext $ assume a,
if h : a ∈ f.support then h₂ a h else
have hf : f a = 0, by rwa [mem_support_iff, not_not] at h,
have hg : g a = 0, by rwa [h₁, mem_support_iff, not_not] at h,
by rw [hf, hg],
by rintro rfl; exact ⟨rfl, λ _ _, rfl⟩⟩
lemma finite_supp (f : α →₀ β) : set.finite {a | f a ≠ 0} :=
⟨fintype.of_finset f.support (λ _, mem_support_iff)⟩
lemma support_subset_iff {s : set α} {f : α →₀ β} :
↑f.support ⊆ s ↔ (∀a∉s, f a = 0) :=
by simp only [set.subset_def, mem_coe, mem_support_iff];
exact forall_congr (assume a, @not_imp_comm _ _ (classical.dec _) (classical.dec _))
def equiv_fun_on_fintype [fintype α] : (α →₀ β) ≃ (α → β) :=
⟨λf a, f a, λf, mk (finset.univ.filter $ λa, f a ≠ 0) f (by simp),
begin intro f, ext a, refl end,
begin intro f, ext a, refl end⟩
end basic
section single
variables [has_zero β] {a a' : α} {b : β}
/-- `single a b` is the finitely supported function which has
value `b` at `a` and zero otherwise. -/
def single (a : α) (b : β) : α →₀ β :=
⟨if b = 0 then ∅ else finset.singleton a, λ a', if a = a' then b else 0, λ a', begin
by_cases hb : b = 0; by_cases a = a';
simp only [hb, h, if_pos, if_false, mem_singleton],
{ exact ⟨false.elim, λ H, H rfl⟩ },
{ exact ⟨false.elim, λ H, H rfl⟩ },
{ exact ⟨λ _, hb, λ _, rfl⟩ },
{ exact ⟨λ H _, h H.symm, λ H, (H rfl).elim⟩ }
end⟩
lemma single_apply : (single a b : α →₀ β) a' = if a = a' then b else 0 := rfl
@[simp] lemma single_eq_same : (single a b : α →₀ β) a = b := if_pos rfl
@[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ β) a' = 0 := if_neg h
@[simp] lemma single_zero : (single a 0 : α →₀ β) = 0 :=
ext $ assume a',
begin
by_cases h : a = a',
{ rw [h, single_eq_same, zero_apply] },
{ rw [single_eq_of_ne h, zero_apply] }
end
lemma support_single_ne_zero (hb : b ≠ 0) : (single a b).support = {a} :=
if_neg hb
lemma support_single_subset : (single a b).support ⊆ {a} :=
show ite _ _ _ ⊆ _, by split_ifs; [exact empty_subset _, exact subset.refl _]
lemma injective_single (a : α) : function.injective (single a : β → α →₀ β) :=
assume b₁ b₂ eq,
have (single a b₁ : α →₀ β) a = (single a b₂ : α →₀ β) a, by rw eq,
by rwa [single_eq_same, single_eq_same] at this
lemma single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : β) :
single a₁ b₁ = single a₂ b₂ ↔ ((a₁ = a₂ ∧ b₁ = b₂) ∨ (b₁ = 0 ∧ b₂ = 0)) :=
begin
split,
{ assume eq,
by_cases a₁ = a₂,
{ refine or.inl ⟨h, _⟩,
rwa [h, (injective_single a₂).eq_iff] at eq },
{ rw [finsupp.ext_iff] at eq,
have h₁ := eq a₁,
have h₂ := eq a₂,
simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (ne.symm h)] at h₁ h₂,
exact or.inr ⟨h₁, h₂.symm⟩ } },
{ rintros (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩),
{ refl },
{ rw [single_zero, single_zero] } }
end
lemma single_right_inj (h : b ≠ 0) :
single a b = single a' b ↔ a = a' :=
⟨λ H, by simpa [h, single_eq_single_iff] using H, λ H, by rw [H]⟩
lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
⟨λ h, by { rw ext_iff at h, simpa only [finsupp.single_eq_same, finsupp.zero_apply] using h a },
λ h, by rw [h, single_zero]⟩
lemma single_swap {α β : Type*} [has_zero β] (a₁ a₂ : α) (b : β) :
(single a₁ b : α → β) a₂ = (single a₂ b : α → β) a₁ :=
by simp [single_apply]; ac_refl
lemma unique_single [unique α] (x : α →₀ β) : x = single (default α) (x (default α)) :=
by ext i; simp [unique.eq_default i]
@[simp] lemma unique_single_eq_iff [unique α] {b' : β} :
single a b = single a' b' ↔ b = b' :=
begin
rw [single_eq_single_iff],
split,
{ rintros (⟨_, rfl⟩ | ⟨rfl, rfl⟩); refl },
{ intro h, left, exact ⟨subsingleton.elim _ _, h⟩ }
end
end single
section on_finset
variables [has_zero β]
/-- `on_finset s f hf` is the finsupp function representing `f` restricted to the set `s`.
The function needs to be 0 outside of `s`. Use this when the set needs filtered anyway, otherwise
often better set representation is available. -/
def on_finset (s : finset α) (f : α → β) (hf : ∀a, f a ≠ 0 → a ∈ s) : α →₀ β :=
⟨s.filter (λa, f a ≠ 0), f,
assume a, classical.by_cases
(assume h : f a = 0, by rw mem_filter; exact ⟨and.right, λ H, (H h).elim⟩)
(assume h : f a ≠ 0, by rw mem_filter; simp only [iff_true_intro h, hf a h, true_and])⟩
@[simp] lemma on_finset_apply {s : finset α} {f : α → β} {hf a} :
(on_finset s f hf : α →₀ β) a = f a :=
rfl
@[simp] lemma support_on_finset_subset {s : finset α} {f : α → β} {hf} :
(on_finset s f hf).support ⊆ s := filter_subset _
end on_finset
section map_range
variables [has_zero β₁] [has_zero β₂]
/-- The composition of `f : β₁ → β₂` and `g : α →₀ β₁` is
`map_range f hf g : α →₀ β₂`, well defined when `f 0 = 0`. -/
def map_range (f : β₁ → β₂) (hf : f 0 = 0) (g : α →₀ β₁) : α →₀ β₂ :=
on_finset g.support (f ∘ g) $
assume a, by rw [mem_support_iff, not_imp_not]; exact λ H, (congr_arg f H).trans hf
@[simp] lemma map_range_apply {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {a : α} :
map_range f hf g a = f (g a) :=
rfl
@[simp] lemma map_range_zero {f : β₁ → β₂} {hf : f 0 = 0} : map_range f hf (0 : α →₀ β₁) = 0 :=
finsupp.ext $ λ a, by simp [hf]
lemma support_map_range {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} :
(map_range f hf g).support ⊆ g.support :=
support_on_finset_subset
@[simp] lemma map_range_single {f : β₁ → β₂} {hf : f 0 = 0} {a : α} {b : β₁} :
map_range f hf (single a b) = single a (f b) :=
finsupp.ext $ λ a', show f (ite _ _ _) = ite _ _ _, by split_ifs; [refl, exact hf]
end map_range
section emb_domain
variables [has_zero β]
/-- Given `f : α₁ ↪ α₂` and `v : α₁ →₀ β`, `emb_domain f v : α₂ →₀ β` is the finitely supported
function whose value at `f a : α₂` is `v a`. For a `b : α₂` outside the range of `f` it is zero. -/
def emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) : α₂ →₀ β :=
begin
refine ⟨v.support.map f, λa₂,
if h : a₂ ∈ v.support.map f then v (v.support.choose (λa₁, f a₁ = a₂) _) else 0, _⟩,
{ rcases finset.mem_map.1 h with ⟨a, ha, rfl⟩,
exact exists_unique.intro a ⟨ha, rfl⟩ (assume b ⟨_, hb⟩, f.inj hb) },
{ assume a₂,
split_ifs,
{ simp [h],
rw [← finsupp.not_mem_support_iff, not_not],
apply finset.choose_mem },
{ simp [h] } }
end
lemma support_emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
(emb_domain f v).support = v.support.map f :=
rfl
lemma emb_domain_zero (f : α₁ ↪ α₂) : (emb_domain f 0 : α₂ →₀ β) = 0 :=
rfl
lemma emb_domain_apply (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₁) :
emb_domain f v (f a) = v a :=
begin
change dite _ _ _ = _,
split_ifs; rw [finset.mem_map' f] at h,
{ refine congr_arg (v : α₁ → β) (f.inj' _),
exact finset.choose_property (λa₁, f a₁ = f a) _ _ },
{ exact (finsupp.not_mem_support_iff.1 h).symm }
end
lemma emb_domain_notin_range (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₂) (h : a ∉ set.range f) :
emb_domain f v a = 0 :=
begin
refine dif_neg (mt (assume h, _) h),
rcases finset.mem_map.1 h with ⟨a, h, rfl⟩,
exact set.mem_range_self a
end
lemma emb_domain_inj {f : α₁ ↪ α₂} {l₁ l₂ : α₁ →₀ β} :
emb_domain f l₁ = emb_domain f l₂ ↔ l₁ = l₂ :=
⟨λ h, finsupp.ext $ λ a, by simpa [emb_domain_apply] using finsupp.ext_iff.1 h (f a),
λ h, by rw h⟩
lemma emb_domain_map_range
{β₁ β₂ : Type*} [has_zero β₁] [has_zero β₂]
(f : α₁ ↪ α₂) (g : β₁ → β₂) (p : α₁ →₀ β₁) (hg : g 0 = 0) :
emb_domain f (map_range g hg p) = map_range g hg (emb_domain f p) :=
begin
ext a,
by_cases a ∈ set.range f,
{ rcases h with ⟨a', rfl⟩,
rw [map_range_apply, emb_domain_apply, emb_domain_apply, map_range_apply] },
{ rw [map_range_apply, emb_domain_notin_range, emb_domain_notin_range, ← hg]; assumption }
end
lemma single_of_emb_domain_single
(l : α₁ →₀ β) (f : α₁ ↪ α₂) (a : α₂) (b : β) (hb : b ≠ 0)
(h : l.emb_domain f = finsupp.single a b) :
∃ x, l = finsupp.single x b ∧ f x = a :=
begin
have h_map_support : finset.map f (l.support) = finset.singleton a,
by rw [←finsupp.support_emb_domain, h, finsupp.support_single_ne_zero hb]; refl,
have ha : a ∈ finset.map f (l.support),
by simp [h_map_support],
rcases finset.mem_map.1 ha with ⟨c, hc₁, hc₂⟩,
use c,
split,
{ ext d,
rw [← finsupp.emb_domain_apply f l, h],
by_cases h_cases : c = d,
{ simp [h_cases.symm, hc₂] },
{ rw [finsupp.single_apply, finsupp.single_apply, if_neg, if_neg h_cases],
by_contra hfd,
exact h_cases (f.inj (hc₂.trans hfd)) } },
{ exact hc₂ }
end
end emb_domain
section zip_with
variables [has_zero β] [has_zero β₁] [has_zero β₂]
/-- `zip_with f hf g₁ g₂` is the finitely supported function satisfying
`zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, and well defined when `f 0 0 = 0`. -/
def zip_with (f : β₁ → β₂ → β) (hf : f 0 0 = 0) (g₁ : α →₀ β₁) (g₂ : α →₀ β₂) : (α →₀ β) :=
on_finset (g₁.support ∪ g₂.support) (λa, f (g₁ a) (g₂ a)) $ λ a H, begin
simp only [mem_union, mem_support_iff, ne], rw [← not_and_distrib],
rintro ⟨h₁, h₂⟩, rw [h₁, h₂] at H, exact H hf
end
@[simp] lemma zip_with_apply
{f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} {a : α} :
zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a) := rfl
lemma support_zip_with {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} :
(zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=
support_on_finset_subset
end zip_with
section erase
def erase [has_zero β] (a : α) (f : α →₀ β) : α →₀ β :=
⟨f.support.erase a, (λa', if a' = a then 0 else f a'),
assume a', by rw [mem_erase, mem_support_iff]; split_ifs;
[exact ⟨λ H _, H.1 h, λ H, (H rfl).elim⟩,
exact and_iff_right h]⟩
@[simp] lemma support_erase [has_zero β] {a : α} {f : α →₀ β} :
(f.erase a).support = f.support.erase a :=
rfl
@[simp] lemma erase_same [has_zero β] {a : α} {f : α →₀ β} : (f.erase a) a = 0 :=
if_pos rfl
@[simp] lemma erase_ne [has_zero β] {a a' : α} {f : α →₀ β} (h : a' ≠ a) : (f.erase a) a' = f a' :=
if_neg h
end erase
-- [to_additive sum] for finsupp.prod doesn't work, the equation lemmas are not generated
/-- `sum f g` is the sum of `g a (f a)` over the support of `f`. -/
def sum [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
f.support.sum (λa, g a (f a))
/-- `prod f g` is the product of `g a (f a)` over the support of `f`. -/
@[to_additive]
def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
f.support.prod (λa, g a (f a))
@[to_additive]
lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ]
{f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {h : α → β₂ → γ} (h0 : ∀a, h a 0 = 1) :
(map_range f hf g).prod h = g.prod (λa b, h a (f b)) :=
finset.prod_subset support_map_range $ λ _ _ H,
by rw [not_mem_support_iff.1 H, h0]
@[to_additive]
lemma prod_zero_index [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} :
(0 : α →₀ β).prod h = 1 := rfl
section nat_sub
instance nat_sub : has_sub (α →₀ ℕ) := ⟨zip_with (λ m n, m - n) (nat.sub_zero 0)⟩
@[simp] lemma nat_sub_apply {g₁ g₂ : α →₀ ℕ} {a : α} :
(g₁ - g₂) a = g₁ a - g₂ a := rfl
end nat_sub
section add_monoid
variables [add_monoid β]
@[to_additive]
lemma prod_single_index [comm_monoid γ] {a : α} {b : β} {h : α → β → γ} (h_zero : h a 0 = 1) :
(single a b).prod h = h a b :=
begin
by_cases h : b = 0,
{ simp only [h, h_zero, single_zero]; refl },
{ simp only [finsupp.prod, support_single_ne_zero h, insert_empty_eq_singleton,
prod_singleton, single_eq_same] }
end
instance : has_add (α →₀ β) := ⟨zip_with (+) (add_zero 0)⟩
@[simp] lemma add_apply {g₁ g₂ : α →₀ β} {a : α} : (g₁ + g₂) a = g₁ a + g₂ a :=
rfl
lemma support_add {g₁ g₂ : α →₀ β} : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
support_zip_with
lemma support_add_eq {g₁ g₂ : α →₀ β} (h : disjoint g₁.support g₂.support) :
(g₁ + g₂).support = g₁.support ∪ g₂.support :=
le_antisymm support_zip_with $ assume a ha,
(finset.mem_union.1 ha).elim
(assume ha, have a ∉ g₂.support, from disjoint_left.1 h ha,
by simp only [mem_support_iff, not_not] at *;
simpa only [add_apply, this, add_zero])
(assume ha, have a ∉ g₁.support, from disjoint_right.1 h ha,
by simp only [mem_support_iff, not_not] at *;
simpa only [add_apply, this, zero_add])
@[simp] lemma single_add {a : α} {b₁ b₂ : β} : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
ext $ assume a',
begin
by_cases h : a = a',
{ rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same] },
{ rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add] }
end
instance : add_monoid (α →₀ β) :=
{ add_monoid .
zero := 0,
add := (+),
add_assoc := assume ⟨s, f, hf⟩ ⟨t, g, hg⟩ ⟨u, h, hh⟩, ext $ assume a, add_assoc _ _ _,
zero_add := assume ⟨s, f, hf⟩, ext $ assume a, zero_add _,
add_zero := assume ⟨s, f, hf⟩, ext $ assume a, add_zero _ }
instance (a : α) : is_add_monoid_hom (λ g : α →₀ β, g a) :=
{ map_add := λ _ _, add_apply, map_zero := zero_apply }
lemma single_add_erase {a : α} {f : α →₀ β} : single a (f a) + f.erase a = f :=
ext $ λ a',
if h : a = a' then by subst h; simp only [add_apply, single_eq_same, erase_same, add_zero]
else by simp only [add_apply, single_eq_of_ne h, zero_add, erase_ne (ne.symm h)]
lemma erase_add_single {a : α} {f : α →₀ β} : f.erase a + single a (f a) = f :=
ext $ λ a',
if h : a = a' then by subst h; simp only [add_apply, single_eq_same, erase_same, zero_add]
else by simp only [add_apply, single_eq_of_ne h, add_zero, erase_ne (ne.symm h)]
@[elab_as_eliminator]
protected theorem induction {p : (α →₀ β) → Prop} (f : α →₀ β)
(h0 : p 0) (ha : ∀a b (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)) :
p f :=
suffices ∀s (f : α →₀ β), f.support = s → p f, from this _ _ rfl,
assume s, finset.induction_on s (λ f hf, by rwa [support_eq_empty.1 hf]) $
assume a s has ih f hf,
suffices p (single a (f a) + f.erase a), by rwa [single_add_erase] at this,
begin
apply ha,
{ rw [support_erase, mem_erase], exact λ H, H.1 rfl },
{ rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
{ apply ih _ _,
rw [support_erase, hf, finset.erase_insert has] }
end
lemma induction₂ {p : (α →₀ β) → Prop} (f : α →₀ β)
(h0 : p 0) (ha : ∀a b (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)) :
p f :=
suffices ∀s (f : α →₀ β), f.support = s → p f, from this _ _ rfl,
assume s, finset.induction_on s (λ f hf, by rwa [support_eq_empty.1 hf]) $
assume a s has ih f hf,
suffices p (f.erase a + single a (f a)), by rwa [erase_add_single] at this,
begin
apply ha,
{ rw [support_erase, mem_erase], exact λ H, H.1 rfl },
{ rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
{ apply ih _ _,
rw [support_erase, hf, finset.erase_insert has] }
end
lemma map_range_add [add_monoid β₁] [add_monoid β₂]
{f : β₁ → β₂} {hf : f 0 = 0} (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : α →₀ β₁) :
map_range f hf (v₁ + v₂) = map_range f hf v₁ + map_range f hf v₂ :=
finsupp.ext $ λ a, by simp [hf']
end add_monoid
instance [add_comm_monoid β] : add_comm_monoid (α →₀ β) :=
{ add_comm := assume ⟨s, f, _⟩ ⟨t, g, _⟩, ext $ assume a, add_comm _ _,
.. finsupp.add_monoid }
instance [add_group β] : add_group (α →₀ β) :=
{ neg := map_range (has_neg.neg) neg_zero,
add_left_neg := assume ⟨s, f, _⟩, ext $ assume x, add_left_neg _,
.. finsupp.add_monoid }
lemma single_multiset_sum [add_comm_monoid β] (s : multiset β) (a : α) :
single a s.sum = (s.map (single a)).sum :=
multiset.induction_on s single_zero $ λ a s ih,
by rw [multiset.sum_cons, single_add, ih, multiset.map_cons, multiset.sum_cons]
lemma single_finset_sum [add_comm_monoid β] (s : finset γ) (f : γ → β) (a : α) :
single a (s.sum f) = s.sum (λb, single a (f b)) :=
begin
transitivity,
apply single_multiset_sum,
rw [multiset.map_map],
refl
end
lemma single_sum [has_zero γ] [add_comm_monoid β] (s : δ →₀ γ) (f : δ → γ → β) (a : α) :
single a (s.sum f) = s.sum (λd c, single a (f d c)) :=
single_finset_sum _ _ _
@[to_additive]
lemma prod_neg_index [add_group β] [comm_monoid γ]
{g : α →₀ β} {h : α → β → γ} (h0 : ∀a, h a 0 = 1) :
(-g).prod h = g.prod (λa b, h a (- b)) :=
prod_map_range_index h0
@[simp] lemma neg_apply [add_group β] {g : α →₀ β} {a : α} : (- g) a = - g a := rfl
@[simp] lemma sub_apply [add_group β] {g₁ g₂ : α →₀ β} {a : α} : (g₁ - g₂) a = g₁ a - g₂ a := rfl
@[simp] lemma support_neg [add_group β] {f : α →₀ β} : support (-f) = support f :=
finset.subset.antisymm
support_map_range
(calc support f = support (- (- f)) : congr_arg support (neg_neg _).symm
... ⊆ support (- f) : support_map_range)
instance [add_comm_group β] : add_comm_group (α →₀ β) :=
{ add_comm := add_comm, ..finsupp.add_group }
@[simp] lemma sum_apply [has_zero β₁] [add_comm_monoid β]
{f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β} {a₂ : α} :
(f.sum g) a₂ = f.sum (λa₁ b, g a₁ b a₂) :=
(f.support.sum_hom (λf : α →₀ β, f a₂)).symm
lemma support_sum [has_zero β₁] [add_comm_monoid β]
{f : α₁ →₀ β₁} {g : α₁ → β₁ → (α →₀ β)} :
(f.sum g).support ⊆ f.support.bind (λa, (g a (f a)).support) :=
have ∀a₁ : α, f.sum (λ (a : α₁) (b : β₁), (g a b) a₁) ≠ 0 →
(∃ (a : α₁), f a ≠ 0 ∧ ¬ (g a (f a)) a₁ = 0),
from assume a₁ h,
let ⟨a, ha, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
⟨a, mem_support_iff.mp ha, ne⟩,
by simpa only [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply, exists_prop] using this
@[simp] lemma sum_zero [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β} :
f.sum (λa b, (0 : γ)) = 0 :=
finset.sum_const_zero
@[simp] lemma sum_add [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β}
{h₁ h₂ : α → β → γ} :
f.sum (λa b, h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂ :=
finset.sum_add_distrib
@[simp] lemma sum_neg [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
{h : α → β → γ} : f.sum (λa b, - h a b) = - f.sum h :=
f.support.sum_hom (@has_neg.neg γ _)
@[simp] lemma sum_sub [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
{h₁ h₂ : α → β → γ} :
f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl
@[simp] lemma sum_single [add_comm_monoid β] (f : α →₀ β) :
f.sum single = f :=
have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =
({a} : finset α).sum (λa', ite (a' = a) (f a') 0),
begin
intro a,
by_cases h : a ∈ f.support,
{ have : (finset.singleton a : finset α) ⊆ f.support,
{ simpa only [finset.subset_iff, mem_singleton, forall_eq] },
refine (finset.sum_subset this (λ _ _ H, _)).symm,
exact if_neg (mt mem_singleton.2 H) },
{ transitivity (f.support.sum (λa, (0 : β))),
{ refine (finset.sum_congr rfl $ λ a' ha', if_neg _),
rintro rfl, exact h ha' },
{ rw [sum_const_zero, insert_empty_eq_singleton, sum_singleton,
if_pos rfl, not_mem_support_iff.1 h] } }
end,
ext $ assume a, by simp only [sum_apply, single_apply, this,
insert_empty_eq_singleton, sum_singleton, if_pos]
@[to_additive]
lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α →₀ β}
{h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
(f + g).prod h = f.prod h * g.prod h :=
have f_eq : (f.support ∪ g.support).prod (λa, h a (f a)) = f.prod h,
from (finset.prod_subset (finset.subset_union_left _ _) $
by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
have g_eq : (f.support ∪ g.support).prod (λa, h a (g a)) = g.prod h,
from (finset.prod_subset (finset.subset_union_right _ _) $
by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
calc (f + g).support.prod (λa, h a ((f + g) a)) =
(f.support ∪ g.support).prod (λa, h a ((f + g) a)) :
finset.prod_subset support_add $
by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]
... = (f.support ∪ g.support).prod (λa, h a (f a)) *
(f.support ∪ g.support).prod (λa, h a (g a)) :
by simp only [add_apply, h_add, finset.prod_mul_distrib]
... = _ : by rw [f_eq, g_eq]
lemma sum_sub_index [add_comm_group β] [add_comm_group γ] {f g : α →₀ β}
{h : α → β → γ} (h_sub : ∀a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) :
(f - g).sum h = f.sum h - g.sum h :=
have h_zero : ∀a, h a 0 = 0,
from assume a,
have h a (0 - 0) = h a 0 - h a 0, from h_sub a 0 0,
by simpa only [sub_self] using this,
have h_neg : ∀a b, h a (- b) = - h a b,
from assume a b,
have h a (0 - b) = h a 0 - h a b, from h_sub a 0 b,
by simpa only [h_zero, zero_sub] using this,
have h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂,
from assume a b₁ b₂,
have h a (b₁ - (- b₂)) = h a b₁ - h a (- b₂), from h_sub a b₁ (-b₂),
by simpa only [h_neg, sub_neg_eq_add] using this,
calc (f - g).sum h = (f + - g).sum h : rfl
... = f.sum h + - g.sum h : by simp only [sum_add_index h_zero h_add, sum_neg_index h_zero, h_neg, sum_neg]
... = f.sum h - g.sum h : rfl
@[to_additive]
lemma prod_finset_sum_index [add_comm_monoid β] [comm_monoid γ]
{s : finset ι} {g : ι → α →₀ β}
{h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
s.prod (λi, (g i).prod h) = (s.sum g).prod h :=
finset.induction_on s rfl $ λ a s has ih,
by rw [prod_insert has, ih, sum_insert has, prod_add_index h_zero h_add]
@[to_additive]
lemma prod_sum_index
[add_comm_monoid β₁] [add_comm_monoid β] [comm_monoid γ]
{f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β}
{h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
(f.sum g).prod h = f.prod (λa b, (g a b).prod h) :=
(prod_finset_sum_index h_zero h_add).symm
lemma multiset_sum_sum_index
[add_comm_monoid β] [add_comm_monoid γ]
(f : multiset (α →₀ β)) (h : α → β → γ)
(h₀ : ∀a, h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
(f.sum.sum h) = (f.map $ λg:α →₀ β, g.sum h).sum :=
multiset.induction_on f rfl $ assume a s ih,
by rw [multiset.sum_cons, multiset.map_cons, multiset.sum_cons, sum_add_index h₀ h₁, ih]
lemma multiset_map_sum [has_zero β] {f : α →₀ β} {m : γ → δ} {h : α → β → multiset γ} :
multiset.map m (f.sum h) = f.sum (λa b, (h a b).map m) :=
(f.support.sum_hom _).symm
lemma multiset_sum_sum [has_zero β] [add_comm_monoid γ] {f : α →₀ β} {h : α → β → multiset γ} :
multiset.sum (f.sum h) = f.sum (λa b, multiset.sum (h a b)) :=
(f.support.sum_hom multiset.sum).symm
section map_range
variables
[add_comm_monoid β₁] [add_comm_monoid β₂]
(f : β₁ → β₂) [hf : is_add_monoid_hom f]
instance is_add_monoid_hom_map_range :
is_add_monoid_hom (map_range f hf.map_zero : (α →₀ β₁) → (α →₀ β₂)) :=
{ map_zero := map_range_zero, map_add := λ a b, map_range_add hf.map_add _ _ }
lemma map_range_multiset_sum (m : multiset (α →₀ β₁)) :
map_range f hf.map_zero m.sum = (m.map $ λx, map_range f hf.map_zero x).sum :=
(m.sum_hom (map_range f hf.map_zero)).symm
lemma map_range_finset_sum {ι : Type*} (s : finset ι) (g : ι → (α →₀ β₁)) :
map_range f hf.map_zero (s.sum g) = s.sum (λx, map_range f hf.map_zero (g x)) :=
by rw [finset.sum.equations._eqn_1, map_range_multiset_sum, multiset.map_map]; refl
end map_range
section map_domain
variables [add_comm_monoid β] {v v₁ v₂ : α →₀ β}
/-- Given `f : α₁ → α₂` and `v : α₁ →₀ β`, `map_domain f v : α₂ →₀ β`
is the finitely supported function whose value at `a : α₂` is the sum
of `v x` over all `x` such that `f x = a`. -/
def map_domain (f : α₁ → α₂) (v : α₁ →₀ β) : α₂ →₀ β :=
v.sum $ λa, single (f a)
lemma map_domain_apply {f : α₁ → α₂} (hf : function.injective f) (x : α₁ →₀ β) (a : α₁) :
map_domain f x (f a) = x a :=
begin
rw [map_domain, sum_apply, sum, finset.sum_eq_single a, single_eq_same],
{ assume b _ hba, exact single_eq_of_ne (hf.ne hba) },
{ simp only [(∉), (≠), not_not, mem_support_iff],
assume h,
rw [h, single_zero],
refl }
end
lemma map_domain_notin_range {f : α₁ → α₂} (x : α₁ →₀ β) (a : α₂) (h : a ∉ set.range f) :
map_domain f x a = 0 :=
begin
rw [map_domain, sum_apply, sum],
exact finset.sum_eq_zero
(assume a' h', single_eq_of_ne $ assume eq, h $ eq ▸ set.mem_range_self _)
end
lemma map_domain_id : map_domain id v = v := sum_single _
lemma map_domain_comp {f : α → α₁} {g : α₁ → α₂} :
map_domain (g ∘ f) v = map_domain g (map_domain f v) :=
begin
refine ((sum_sum_index _ _).trans _).symm,
{ intros, exact single_zero },
{ intros, exact single_add },
refine sum_congr rfl (λ _ _, sum_single_index _),
{ exact single_zero }
end
lemma map_domain_single {f : α → α₁} {a : α} {b : β} : map_domain f (single a b) = single (f a) b :=
sum_single_index single_zero
@[simp] lemma map_domain_zero {f : α → α₂} : map_domain f 0 = (0 : α₂ →₀ β) :=
sum_zero_index
lemma map_domain_congr {f g : α → α₂} (h : ∀x∈v.support, f x = g x) :
v.map_domain f = v.map_domain g :=
finset.sum_congr rfl $ λ _ H, by simp only [h _ H]
lemma map_domain_add {f : α → α₂} : map_domain f (v₁ + v₂) = map_domain f v₁ + map_domain f v₂ :=
sum_add_index (λ _, single_zero) (λ _ _ _, single_add)
lemma map_domain_finset_sum {f : α → α₂} {s : finset ι} {v : ι → α →₀ β} :
map_domain f (s.sum v) = s.sum (λi, map_domain f (v i)) :=
eq.symm $ sum_finset_sum_index (λ _, single_zero) (λ _ _ _, single_add)
lemma map_domain_sum [has_zero β₁] {f : α → α₂} {s : α →₀ β₁} {v : α → β₁ → α →₀ β} :
map_domain f (s.sum v) = s.sum (λa b, map_domain f (v a b)) :=
eq.symm $ sum_finset_sum_index (λ _, single_zero) (λ _ _ _, single_add)
lemma map_domain_support {f : α → α₂} {s : α →₀ β} :
(s.map_domain f).support ⊆ s.support.image f :=
finset.subset.trans support_sum $
finset.subset.trans (finset.bind_mono $ assume a ha, support_single_subset) $
by rw [finset.bind_singleton]; exact subset.refl _
@[to_additive]
lemma prod_map_domain_index [comm_monoid γ] {f : α → α₂} {s : α →₀ β}
{h : α₂ → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
(s.map_domain f).prod h = s.prod (λa b, h (f a) b) :=
(prod_sum_index h_zero h_add).trans $ prod_congr rfl $ λ _ _, prod_single_index (h_zero _)
lemma emb_domain_eq_map_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
emb_domain f v = map_domain f v :=
begin
ext a,
by_cases a ∈ set.range f,
{ rcases h with ⟨a, rfl⟩,
rw [map_domain_apply (function.embedding.inj' _), emb_domain_apply] },
{ rw [map_domain_notin_range, emb_domain_notin_range]; assumption }
end
lemma injective_map_domain {f : α₁ → α₂} (hf : function.injective f) :
function.injective (map_domain f : (α₁ →₀ β) → (α₂ →₀ β)) :=
begin
assume v₁ v₂ eq, ext a,
have : map_domain f v₁ (f a) = map_domain f v₂ (f a), { rw eq },
rwa [map_domain_apply hf, map_domain_apply hf] at this,
end
end map_domain
section comap_domain
noncomputable def comap_domain {α₁ α₂ γ : Type*} [has_zero γ]
(f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) : α₁ →₀ γ :=
{ support := l.support.preimage hf,
to_fun := (λ a, l (f a)),
mem_support_to_fun :=
begin
intros a,
simp only [finset.mem_def.symm, finset.mem_preimage],
exact l.mem_support_to_fun (f a),
end }
lemma comap_domain_apply {α₁ α₂ γ : Type*} [has_zero γ]
(f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) (a : α₁) :
comap_domain f l hf a = l (f a) :=
begin
unfold_coes,
unfold comap_domain,
simp,
refl
end
lemma sum_comap_domain {α₁ α₂ β γ : Type*} [has_zero β] [add_comm_monoid γ]
(f : α₁ → α₂) (l : α₂ →₀ β) (g : α₂ → β → γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set):
(comap_domain f l (set.inj_on_of_bij_on hf)).sum (g ∘ f) = l.sum g :=
begin
unfold sum,
haveI := classical.dec_eq α₂,
simp only [comap_domain, comap_domain_apply, finset.sum_preimage f _ _ (λ (x : α₂), g x (l x))],
end
lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid γ]
(f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set) :
comap_domain f l (set.inj_on_of_bij_on hf) = 0 → l = 0 :=
begin
rw [← support_eq_empty, ← support_eq_empty, comap_domain],
simp only [finset.ext, finset.not_mem_empty, iff_false, mem_preimage],
assume h a ha,
cases hf.2.2 ha with b hb,
exact h b (hb.2.symm ▸ ha)
end
lemma map_domain_comap_domain {α₁ α₂ γ : Type*} [add_comm_monoid γ]
(f : α₁ → α₂) (l : α₂ →₀ γ)
(hf : function.injective f) (hl : ↑l.support ⊆ set.range f):
map_domain f (comap_domain f l (set.inj_on_of_injective _ hf)) = l :=
begin
ext a,
haveI := classical.dec (a ∈ set.range f),
by_cases h_cases: a ∈ set.range f,
{ rcases set.mem_range.1 h_cases with ⟨b, hb⟩,
rw [hb.symm, map_domain_apply hf, comap_domain_apply] },
{ rw map_domain_notin_range _ _ h_cases,
by_contra h_contr,
apply h_cases (hl (finset.mem_coe.2 (mem_support_iff.2 (λ h, h_contr h.symm)))) }
end
end comap_domain
/-- The product of `f g : α →₀ β` is the finitely supported function
whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
such that `x + y = a`. (Think of the product of multivariate
polynomials where `α` is the monoid of monomial exponents.) -/
instance [has_add α] [semiring β] : has_mul (α →₀ β) :=
⟨λf g, f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ + a₂) (b₁ * b₂)⟩
lemma mul_def [has_add α] [semiring β] {f g : α →₀ β} :
f * g = (f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ + a₂) (b₁ * b₂)) := rfl
lemma support_mul [has_add α] [semiring β] (a b : α →₀ β) :
(a * b).support ⊆ a.support.bind (λa₁, b.support.bind $ λa₂, {a₁ + a₂}) :=
subset.trans support_sum $ bind_mono $ assume a₁ _,
subset.trans support_sum $ bind_mono $ assume a₂ _, support_single_subset
/-- The unit of the multiplication is `single 0 1`, i.e. the function
that is 1 at 0 and zero elsewhere. -/
instance [has_zero α] [has_zero β] [has_one β] : has_one (α →₀ β) :=
⟨single 0 1⟩
lemma one_def [has_zero α] [has_zero β] [has_one β] : 1 = (single 0 1 : α →₀ β) := rfl
section filter
section has_zero
variables [has_zero β] (p : α → Prop) (f : α →₀ β)
/-- `filter p f` is the function which is `f a` if `p a` is true and 0 otherwise. -/
def filter (p : α → Prop) (f : α →₀ β) : α →₀ β :=
on_finset f.support (λa, if p a then f a else 0) $ λ a H,
mem_support_iff.2 $ λ h, by rw [h, if_t_t] at H; exact H rfl
@[simp] lemma filter_apply_pos {a : α} (h : p a) : f.filter p a = f a :=
if_pos h
@[simp] lemma filter_apply_neg {a : α} (h : ¬ p a) : f.filter p a = 0 :=
if_neg h
@[simp] lemma support_filter : (f.filter p).support = f.support.filter p :=
finset.ext.mpr $ assume a, if H : p a
then by simp only [mem_support_iff, filter_apply_pos _ _ H, mem_filter, H, and_true]
else by simp only [mem_support_iff, filter_apply_neg _ _ H, mem_filter, H, and_false, ne.def, ne_self_iff_false]
lemma filter_zero : (0 : α →₀ β).filter p = 0 :=
by rw [← support_eq_empty, support_filter, support_zero, finset.filter_empty]
@[simp] lemma filter_single_of_pos
{a : α} {b : β} (h : p a) : (single a b).filter p = single a b :=
finsupp.ext $ λ x, begin
by_cases h' : p x; simp [h'],
rw single_eq_of_ne, rintro rfl, exact h' h
end
@[simp] lemma filter_single_of_neg
{a : α} {b : β} (h : ¬ p a) : (single a b).filter p = 0 :=
finsupp.ext $ λ x, begin
by_cases h' : p x; simp [h'],
rw single_eq_of_ne, rintro rfl, exact h h'
end
end has_zero
lemma filter_pos_add_filter_neg [add_monoid β] (f : α →₀ β) (p : α → Prop) :
f.filter p + f.filter (λa, ¬ p a) = f :=
finsupp.ext $ assume a, if H : p a
then by simp only [add_apply, filter_apply_pos, filter_apply_neg, H, not_not, add_zero]
else by simp only [add_apply, filter_apply_pos, filter_apply_neg, H, not_false_iff, zero_add]
end filter
section frange
variables [has_zero β]
def frange (f : α →₀ β) : finset β :=
finset.image f f.support
theorem mem_frange {f : α →₀ β} {y : β} :
y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y :=
finset.mem_image.trans
⟨λ ⟨x, hx1, hx2⟩, ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩,
λ ⟨hy, x, hx⟩, ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩
theorem zero_not_mem_frange {f : α →₀ β} : (0:β) ∉ f.frange :=
λ H, (mem_frange.1 H).1 rfl
theorem frange_single {x : α} {y : β} : frange (single x y) ⊆ {y} :=
λ r hr, let ⟨t, ht1, ht2⟩ := mem_frange.1 hr in ht2 ▸
(by rw single_apply at ht2 ⊢; split_ifs at ht2 ⊢; [exact finset.mem_singleton_self _, cc])
end frange
section subtype_domain
variables {α' : Type*} [has_zero δ] {p : α → Prop}
section zero
variables [has_zero β] {v v' : α' →₀ β}
/-- `subtype_domain p f` is the restriction of the finitely supported function
`f` to the subtype `p`. -/
def subtype_domain (p : α → Prop) (f : α →₀ β) : (subtype p →₀ β) :=
⟨f.support.subtype p, f ∘ subtype.val, λ a, by simp only [mem_subtype, mem_support_iff]⟩
@[simp] lemma support_subtype_domain {f : α →₀ β} :
(subtype_domain p f).support = f.support.subtype p :=
rfl
@[simp] lemma subtype_domain_apply {a : subtype p} {v : α →₀ β} :
(subtype_domain p v) a = v (a.val) :=
rfl
@[simp] lemma subtype_domain_zero : subtype_domain p (0 : α →₀ β) = 0 :=
rfl
@[to_additive]
lemma prod_subtype_domain_index [comm_monoid γ] {v : α →₀ β}
{h : α → β → γ} (hp : ∀x∈v.support, p x) :
(v.subtype_domain p).prod (λa b, h a.1 b) = v.prod h :=
prod_bij (λp _, p.val)
(λ _, mem_subtype.1)
(λ _ _, rfl)
(λ _ _ _ _, subtype.eq)
(λ b hb, ⟨⟨b, hp b hb⟩, mem_subtype.2 hb, rfl⟩)
end zero
section monoid
variables [add_monoid β] {v v' : α' →₀ β}
@[simp] lemma subtype_domain_add {v v' : α →₀ β} :
(v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=
ext $ λ _, rfl
instance subtype_domain.is_add_monoid_hom :
is_add_monoid_hom (subtype_domain p : (α →₀ β) → subtype p →₀ β) :=
{ map_add := λ _ _, subtype_domain_add, map_zero := subtype_domain_zero }
@[simp] lemma filter_add {v v' : α →₀ β} :
(v + v').filter p = v.filter p + v'.filter p :=
ext $ λ a, by by_cases p a; simp [h]
instance filter.is_add_monoid_hom (p : α → Prop) :
is_add_monoid_hom (filter p : (α →₀ β) → (α →₀ β)) :=
{ map_zero := filter_zero p, map_add := λ x y, filter_add }
end monoid
section comm_monoid
variables [add_comm_monoid β]
lemma subtype_domain_sum {s : finset γ} {h : γ → α →₀ β} :
(s.sum h).subtype_domain p = s.sum (λc, (h c).subtype_domain p) :=
eq.symm (s.sum_hom _)
lemma subtype_domain_finsupp_sum {s : γ →₀ δ} {h : γ → δ → α →₀ β} :
(s.sum h).subtype_domain p = s.sum (λc d, (h c d).subtype_domain p) :=
subtype_domain_sum
lemma filter_sum (s : finset γ) (f : γ → α →₀ β) :
(s.sum f).filter p = s.sum (λa, filter p (f a)) :=
(s.sum_hom (filter p)).symm
end comm_monoid
section group
variables [add_group β] {v v' : α' →₀ β}
@[simp] lemma subtype_domain_neg {v : α →₀ β} :
(- v).subtype_domain p = - v.subtype_domain p :=
ext $ λ _, rfl
@[simp] lemma subtype_domain_sub {v v' : α →₀ β} :
(v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=
ext $ λ _, rfl
end group
end subtype_domain
section multiset
def to_multiset (f : α →₀ ℕ) : multiset α :=
f.sum (λa n, add_monoid.smul n {a})
lemma to_multiset_zero : (0 : α →₀ ℕ).to_multiset = 0 :=
rfl
lemma to_multiset_add (m n : α →₀ ℕ) :
(m + n).to_multiset = m.to_multiset + n.to_multiset :=
sum_add_index (assume a, add_monoid.zero_smul _) (assume a b₁ b₂, add_monoid.add_smul _ _ _)
lemma to_multiset_single (a : α) (n : ℕ) : to_multiset (single a n) = add_monoid.smul n {a} :=
by rw [to_multiset, sum_single_index]; apply add_monoid.zero_smul
instance is_add_monoid_hom.to_multiset : is_add_monoid_hom (to_multiset : _ → multiset α) :=
{ map_zero := to_multiset_zero, map_add := to_multiset_add }
lemma card_to_multiset (f : α →₀ ℕ) : f.to_multiset.card = f.sum (λa, id) :=
begin
refine f.induction _ _,
{ rw [to_multiset_zero, multiset.card_zero, sum_zero_index] },
{ assume a n f _ _ ih,
rw [to_multiset_add, multiset.card_add, ih, sum_add_index, to_multiset_single,
sum_single_index, multiset.card_smul, multiset.singleton_eq_singleton,
multiset.card_singleton, mul_one]; intros; refl }
end
lemma to_multiset_map (f : α →₀ ℕ) (g : α → β) :
f.to_multiset.map g = (f.map_domain g).to_multiset :=
begin
refine f.induction _ _,
{ rw [to_multiset_zero, multiset.map_zero, map_domain_zero, to_multiset_zero] },
{ assume a n f _ _ ih,
rw [to_multiset_add, multiset.map_add, ih, map_domain_add, map_domain_single,
to_multiset_single, to_multiset_add, to_multiset_single,
is_add_monoid_hom.map_smul (multiset.map g)],
refl }
end
lemma prod_to_multiset [comm_monoid α] (f : α →₀ ℕ) :
f.to_multiset.prod = f.prod (λa n, a ^ n) :=
begin
refine f.induction _ _,
{ rw [to_multiset_zero, multiset.prod_zero, finsupp.prod_zero_index] },
{ assume a n f _ _ ih,
rw [to_multiset_add, multiset.prod_add, ih, to_multiset_single, finsupp.prod_add_index,
finsupp.prod_single_index, multiset.prod_smul, multiset.singleton_eq_singleton,
multiset.prod_singleton],
{ exact pow_zero a },
{ exact pow_zero },
{ exact pow_add } }
end
lemma to_finset_to_multiset (f : α →₀ ℕ) : f.to_multiset.to_finset = f.support :=
begin
refine f.induction _ _,
{ rw [to_multiset_zero, multiset.to_finset_zero, support_zero] },
{ assume a n f ha hn ih,
rw [to_multiset_add, multiset.to_finset_add, ih, to_multiset_single, support_add_eq,
support_single_ne_zero hn, multiset.to_finset_smul _ _ hn,
multiset.singleton_eq_singleton, multiset.to_finset_cons, multiset.to_finset_zero],
refl,
refine disjoint_mono support_single_subset (subset.refl _) _,
rwa [finset.singleton_eq_singleton, finset.singleton_disjoint] }
end
@[simp] lemma count_to_multiset (f : α →₀ ℕ) (a : α) :
f.to_multiset.count a = f a :=
calc f.to_multiset.count a = f.sum (λx n, (add_monoid.smul n {x} : multiset α).count a) :
(f.support.sum_hom $ multiset.count a).symm
... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_smul]
... = f.sum (λx n, n * (x :: 0 : multiset α).count a) : rfl
... = f a * (a :: 0 : multiset α).count a : sum_eq_single _
(λ a' _ H, by simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero])
(λ H, by simp only [not_mem_support_iff.1 H, zero_mul])
... = f a : by simp only [multiset.count_singleton, mul_one]
def of_multiset (m : multiset α) : α →₀ ℕ :=
on_finset m.to_finset (λa, m.count a) $ λ a H, multiset.mem_to_finset.2 $
by_contradiction (mt multiset.count_eq_zero.2 H)
@[simp] lemma of_multiset_apply (m : multiset α) (a : α) :
of_multiset m a = m.count a :=
rfl
def equiv_multiset : (α →₀ ℕ) ≃ (multiset α) :=
⟨ to_multiset, of_multiset,
assume f, finsupp.ext $ λ a, by rw [of_multiset_apply, count_to_multiset],
assume m, multiset.ext.2 $ λ a, by rw [count_to_multiset, of_multiset_apply] ⟩
lemma mem_support_multiset_sum [add_comm_monoid β]
{s : multiset (α →₀ β)} (a : α) :
a ∈ s.sum.support → ∃f∈s, a ∈ (f : α →₀ β).support :=
multiset.induction_on s false.elim
begin
assume f s ih ha,
by_cases a ∈ f.support,
{ exact ⟨f, multiset.mem_cons_self _ _, h⟩ },
{ simp only [multiset.sum_cons, mem_support_iff, add_apply,
not_mem_support_iff.1 h, zero_add] at ha,
rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩,
exact ⟨f', multiset.mem_cons_of_mem h₀, h₁⟩ }
end
lemma mem_support_finset_sum [add_comm_monoid β]
{s : finset γ} {h : γ → α →₀ β} (a : α) (ha : a ∈ (s.sum h).support) : ∃c∈s, a ∈ (h c).support :=
let ⟨f, hf, hfa⟩ := mem_support_multiset_sum a ha in
let ⟨c, hc, eq⟩ := multiset.mem_map.1 hf in
⟨c, hc, eq.symm ▸ hfa⟩
lemma mem_support_single [has_zero β] (a a' : α) (b : β) :
a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0 :=
⟨λ H : (a ∈ ite _ _ _), if h : b = 0
then by rw if_pos h at H; exact H.elim
else ⟨by rw if_neg h at H; exact mem_singleton.1 H, h⟩,
λ ⟨h1, h2⟩, show a ∈ ite _ _ _, by rw [if_neg h2]; exact mem_singleton.2 h1⟩
end multiset
section curry_uncurry
protected def curry [add_comm_monoid γ]
(f : (α × β) →₀ γ) : α →₀ (β →₀ γ) :=
f.sum $ λp c, single p.1 (single p.2 c)
lemma sum_curry_index
[add_comm_monoid γ] [add_comm_monoid δ]
(f : (α × β) →₀ γ) (g : α → β → γ → δ)
(hg₀ : ∀ a b, g a b 0 = 0) (hg₁ : ∀a b c₀ c₁, g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
f.curry.sum (λa f, f.sum (g a)) = f.sum (λp c, g p.1 p.2 c) :=
begin
rw [finsupp.curry],
transitivity,
{ exact sum_sum_index (assume a, sum_zero_index)
(assume a b₀ b₁, sum_add_index (assume a, hg₀ _ _) (assume c d₀ d₁, hg₁ _ _ _ _)) },
congr, funext p c,
transitivity,
{ exact sum_single_index sum_zero_index },
exact sum_single_index (hg₀ _ _)
end
protected def uncurry [add_comm_monoid γ] (f : α →₀ (β →₀ γ)) : (α × β) →₀ γ :=
f.sum $ λa g, g.sum $ λb c, single (a, b) c
def finsupp_prod_equiv [add_comm_monoid γ] : ((α × β) →₀ γ) ≃ (α →₀ (β →₀ γ)) :=
by refine ⟨finsupp.curry, finsupp.uncurry, λ f, _, λ f, _⟩; simp only [
finsupp.curry, finsupp.uncurry, sum_sum_index, sum_zero_index, sum_add_index,
sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff,
forall_3_true_iff, prod.mk.eta, (single_sum _ _ _).symm, sum_single]
lemma filter_curry [add_comm_monoid β] (f : α₁ × α₂ →₀ β) (p : α₁ → Prop) :
(f.filter (λa:α₁×α₂, p a.1)).curry = f.curry.filter p :=
begin
rw [finsupp.curry, finsupp.curry, finsupp.sum, finsupp.sum,
@filter_sum _ (α₂ →₀ β) _ p _ f.support _],
rw [support_filter, sum_filter],
refine finset.sum_congr rfl _,
rintros ⟨a₁, a₂⟩ ha,
dsimp only,
split_ifs,
{ rw [filter_apply_pos, filter_single_of_pos]; exact h },
{ rwa [filter_single_of_neg] }
end
lemma support_curry [add_comm_monoid β] (f : α₁ × α₂ →₀ β) :
f.curry.support ⊆ f.support.image prod.fst :=
begin
rw ← finset.bind_singleton,
refine finset.subset.trans support_sum _,
refine finset.bind_mono (assume a _, support_single_subset)
end
end curry_uncurry
section
variables [add_monoid α] [semiring β]
-- TODO: the simplifier unfolds 0 in the instance proof!
private lemma zero_mul (f : α →₀ β) : 0 * f = 0 := by simp only [mul_def, sum_zero_index]
private lemma mul_zero (f : α →₀ β) : f * 0 = 0 := by simp only [mul_def, sum_zero_index, sum_zero]
private lemma left_distrib (a b c : α →₀ β) : a * (b + c) = a * b + a * c :=
by simp only [mul_def, sum_add_index, mul_add, _root_.mul_zero, single_zero, single_add,
eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add]
private lemma right_distrib (a b c : α →₀ β) : (a + b) * c = a * c + b * c :=
by simp only [mul_def, sum_add_index, add_mul, _root_.mul_zero, _root_.zero_mul, single_zero, single_add,
eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, sum_add]
instance : semiring (α →₀ β) :=
{ one := 1,
mul := (*),
one_mul := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.zero_mul, single_zero, sum_zero,
zero_add, one_mul, sum_single],
mul_one := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.mul_zero, single_zero, sum_zero,
add_zero, mul_one, sum_single],
zero_mul := zero_mul,
mul_zero := mul_zero,
mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index, sum_single_index,
single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
add_mul, mul_add, add_assoc, mul_assoc, _root_.zero_mul, _root_.mul_zero, sum_zero, sum_add],
left_distrib := left_distrib,
right_distrib := right_distrib,
.. finsupp.add_comm_monoid }
end
instance [add_comm_monoid α] [comm_semiring β] : comm_semiring (α →₀ β) :=
{ mul_comm := assume f g,
begin
simp only [mul_def, finsupp.sum, mul_comm],
rw [finset.sum_comm],
simp only [add_comm]
end,
.. finsupp.semiring }
instance [add_monoid α] [ring β] : ring (α →₀ β) :=
{ neg := has_neg.neg,
add_left_neg := add_left_neg,
.. finsupp.semiring }
instance [add_comm_monoid α] [comm_ring β] : comm_ring (α →₀ β) :=
{ mul_comm := mul_comm, .. finsupp.ring}
lemma single_mul_single [has_add α] [semiring β] {a₁ a₂ : α} {b₁ b₂ : β}:
single a₁ b₁ * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
(sum_single_index (by simp only [_root_.zero_mul, single_zero, sum_zero])).trans
(sum_single_index (by rw [_root_.mul_zero, single_zero]))
lemma prod_single [add_comm_monoid α] [comm_semiring β]
{s : finset ι} {a : ι → α} {b : ι → β} :
s.prod (λi, single (a i) (b i)) = single (s.sum a) (s.prod b) :=
finset.induction_on s rfl $ λ a s has ih, by rw [prod_insert has, ih,
single_mul_single, sum_insert has, prod_insert has]
section
instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : has_scalar γ (α →₀ β) := ⟨λa v, v.map_range ((•) a) (smul_zero _)⟩
variables (α β)
@[simp] lemma smul_apply' {R:semiring γ} [add_comm_monoid β] [semimodule γ β] {a : α} {b : γ} {v : α →₀ β} :
(b • v) a = b • (v a) := rfl
instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : semimodule γ (α →₀ β) :=
{ smul := (•),
smul_add := λ a x y, finsupp.ext $ λ _, smul_add _ _ _,
add_smul := λ a x y, finsupp.ext $ λ _, add_smul _ _ _,
one_smul := λ x, finsupp.ext $ λ _, one_smul _ _,
mul_smul := λ r s x, finsupp.ext $ λ _, mul_smul _ _ _,
zero_smul := λ x, finsupp.ext $ λ _, zero_smul _ _,
smul_zero := λ x, finsupp.ext $ λ _, smul_zero _ }
instance [ring γ] [add_comm_group β] [module γ β] : module γ (α →₀ β) :=
{ ..finsupp.semimodule α β }
instance [discrete_field γ] [add_comm_group β] [vector_space γ β] : vector_space γ (α →₀ β) :=
{ ..finsupp.module α β }
variables {α β}
lemma support_smul {R:semiring γ} [add_comm_monoid β] [semimodule γ β] {b : γ} {g : α →₀ β} :
(b • g).support ⊆ g.support :=
λ a, by simp; exact mt (λ h, h.symm ▸ smul_zero _)
section
variables {α' : Type*} [has_zero δ] {p : α → Prop}
@[simp] lemma filter_smul {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
{b : γ} {v : α →₀ β} : (b • v).filter p = b • v.filter p :=
ext $ λ a, by by_cases p a; simp [h]
end
lemma map_domain_smul {α'} {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
{f : α → α'} (b : γ) (v : α →₀ β) : map_domain f (b • v) = b • map_domain f v :=
begin
change map_domain f (map_range _ _ _) = map_range _ _ _,
apply finsupp.induction v, {simp},
intros a b v' hv₁ hv₂ IH,
rw [map_range_add, map_domain_add, IH, map_domain_add, map_range_add,
map_range_single, map_domain_single, map_domain_single, map_range_single];
apply smul_add
end
@[simp] lemma smul_single {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
(c : γ) (a : α) (b : β) : c • finsupp.single a b = finsupp.single a (c • b) :=
ext $ λ a', by by_cases a = a'; [{subst h, simp}, simp [h]]
end
@[simp] lemma smul_apply [ring β] {a : α} {b : β} {v : α →₀ β} :
(b • v) a = b • (v a) := rfl
lemma sum_smul_index [ring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ}
(h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) :=
finsupp.sum_map_range_index h0
section
variables [semiring β] [semiring γ]
lemma sum_mul (b : γ) (s : α →₀ β) {f : α → β → γ} :
(s.sum f) * b = s.sum (λ a c, (f a (s a)) * b) :=
by simp only [finsupp.sum, finset.sum_mul]
lemma mul_sum (b : γ) (s : α →₀ β) {f : α → β → γ} :
b * (s.sum f) = s.sum (λ a c, b * (f a (s a))) :=
by simp only [finsupp.sum, finset.mul_sum]
protected lemma eq_zero_of_zero_eq_one
(zero_eq_one : (0 : β) = 1) (l : α →₀ β) : l = 0 :=
by ext i; simp [eq_zero_of_zero_eq_one β zero_eq_one (l i)]
end
def restrict_support_equiv [add_comm_monoid β] (s : set α) :
{f : α →₀ β // ↑f.support ⊆ s } ≃ (s →₀ β):=
begin
refine ⟨λf, subtype_domain (λx, x ∈ s) f.1, λ f, ⟨f.map_domain subtype.val, _⟩, _, _⟩,
{ refine set.subset.trans (finset.coe_subset.2 map_domain_support) _,
rw [finset.coe_image, set.image_subset_iff],
exact assume x hx, x.2 },
{ rintros ⟨f, hf⟩,
apply subtype.eq,
ext a,
dsimp only,
refine classical.by_cases (assume h : a ∈ set.range (subtype.val : s → α), _) (assume h, _),
{ rcases h with ⟨x, rfl⟩,
rw [map_domain_apply subtype.val_injective, subtype_domain_apply] },
{ convert map_domain_notin_range _ _ h,
rw [← not_mem_support_iff],
refine mt _ h,
exact assume ha, ⟨⟨a, hf ha⟩, rfl⟩ } },
{ assume f,
ext ⟨a, ha⟩,
dsimp only,
rw [subtype_domain_apply, map_domain_apply subtype.val_injective] }
end
protected def dom_congr [add_comm_monoid β] (e : α₁ ≃ α₂) : (α₁ →₀ β) ≃ (α₂ →₀ β) :=
⟨map_domain e, map_domain e.symm,
begin
assume v,
simp only [map_domain_comp.symm, (∘), equiv.symm_apply_apply],
exact map_domain_id
end,
begin
assume v,
simp only [map_domain_comp.symm, (∘), equiv.apply_symm_apply],
exact map_domain_id
end⟩
section sigma
variables {αs : ι → Type*} [has_zero β] (l : (Σ i, αs i) →₀ β)
noncomputable def split (i : ι) : αs i →₀ β :=
l.comap_domain (sigma.mk i) (λ x1 x2 _ _ hx, heq_iff_eq.1 (sigma.mk.inj hx).2)
lemma split_apply (i : ι) (x : αs i) : split l i x = l ⟨i, x⟩ :=
begin
dunfold split,
rw comap_domain_apply
end
def split_support : finset ι := l.support.image sigma.fst
lemma mem_split_support_iff_nonzero (i : ι) :
i ∈ split_support l ↔ split l i ≠ 0 :=
begin
classical,
rw [split_support, mem_image, ne.def, ← support_eq_empty, ← ne.def,
← finset.nonempty_iff_ne_empty, split, comap_domain, finset.nonempty],
simp
end
noncomputable def split_comp [has_zero γ] (g : Π i, (αs i →₀ β) → γ)
(hg : ∀ i x, x = 0 ↔ g i x = 0) : ι →₀ γ :=
{ support := split_support l,
to_fun := λ i, g i (split l i),
mem_support_to_fun :=
begin
intros i,
rw mem_split_support_iff_nonzero,
haveI := classical.dec,
rwa not_iff_not,
exact hg _ _,
end }
lemma sigma_support : l.support = l.split_support.sigma (λ i, (l.split i).support) :=
by simp [finset.ext, split_support, split, comap_domain]; tauto
lemma sigma_sum [add_comm_monoid γ] (f : (Σ (i : ι), αs i) → β → γ) :
l.sum f = (split_support l).sum (λ (i : ι), (split l i).sum (λ (a : αs i) b, f ⟨i, a⟩ b)) :=
by simp [sum, sigma_support, sum_sigma,split_apply]
end sigma
end finsupp
namespace multiset
def to_finsupp (s : multiset α) : α →₀ ℕ :=
{ support := s.to_finset,
to_fun := λ a, s.count a,
mem_support_to_fun := λ a,
begin
rw mem_to_finset,
convert not_iff_not_of_iff (count_eq_zero.symm),
rw not_not
end }
@[simp] lemma to_finsupp_support (s : multiset α) :
s.to_finsupp.support = s.to_finset := rfl
@[simp] lemma to_finsupp_apply (s : multiset α) (a : α) :
s.to_finsupp a = s.count a := rfl
@[simp] lemma to_finsupp_zero :
to_finsupp (0 : multiset α) = 0 :=
finsupp.ext $ λ a, count_zero a
@[simp] lemma to_finsupp_add (s t : multiset α) :
to_finsupp (s + t) = to_finsupp s + to_finsupp t :=
finsupp.ext $ λ a, count_add a s t
lemma to_finsupp_singleton (a : α) :
to_finsupp {a} = finsupp.single a 1 :=
finsupp.ext $ λ b,
if h : a = b then by simp [finsupp.single_apply, h] else
begin
rw [to_finsupp_apply, finsupp.single_apply, if_neg h, count_eq_zero,
singleton_eq_singleton, mem_singleton],
rintro rfl, exact h rfl
end
namespace to_finsupp
instance : is_add_monoid_hom (to_finsupp : multiset α → α →₀ ℕ) :=
{ map_zero := to_finsupp_zero,
map_add := to_finsupp_add }
end to_finsupp
@[simp] lemma to_finsupp_to_multiset (s : multiset α) :
s.to_finsupp.to_multiset = s :=
ext.2 $ λ a, by rw [finsupp.count_to_multiset, to_finsupp_apply]
end multiset
namespace finsupp
variables {σ : Type*}
instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
{ le := λ f g, ∀ s, f s ≤ g s,
le_refl := λ f s, le_refl _,
le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }
instance [partial_order α] [has_zero α] : partial_order (σ →₀ α) :=
{ le_antisymm := λ f g hfg hgf, finsupp.ext $ λ s, le_antisymm (hfg s) (hgf s),
.. finsupp.preorder }
instance [ordered_cancel_comm_monoid α] :
add_left_cancel_semigroup (σ →₀ α) :=
{ add_left_cancel := λ a b c h, finsupp.ext $ λ s,
by { rw finsupp.ext_iff at h, exact add_left_cancel (h s) },
.. finsupp.add_monoid }
instance [ordered_cancel_comm_monoid α] :
add_right_cancel_semigroup (σ →₀ α) :=
{ add_right_cancel := λ a b c h, finsupp.ext $ λ s,
by { rw finsupp.ext_iff at h, exact add_right_cancel (h s) },
.. finsupp.add_monoid }
instance [ordered_cancel_comm_monoid α] :
ordered_cancel_comm_monoid (σ →₀ α) :=
{ add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
le_of_add_le_add_left := λ a b c h s, le_of_add_le_add_left (h s),
.. finsupp.add_comm_monoid, .. finsupp.partial_order,
.. finsupp.add_left_cancel_semigroup, .. finsupp.add_right_cancel_semigroup }
lemma le_iff [canonically_ordered_monoid α] (f g : σ →₀ α) :
f ≤ g ↔ ∀ s ∈ f.support, f s ≤ g s :=
⟨λ h s hs, h s,
λ h s, if H : s ∈ f.support then h s H else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩
@[simp] lemma add_eq_zero_iff [canonically_ordered_monoid α] (f g : σ →₀ α) :
f + g = 0 ↔ f = 0 ∧ g = 0 :=
begin
split,
{ assume h,
split,
all_goals
{ ext s,
suffices H : f s + g s = 0,
{ rw add_eq_zero_iff at H, cases H, assumption },
show (f + g) s = 0,
rw h, refl } },
{ rintro ⟨rfl, rfl⟩, simp }
end
attribute [simp] to_multiset_zero to_multiset_add
@[simp] lemma to_multiset_to_finsupp (f : σ →₀ ℕ) :
f.to_multiset.to_finsupp = f :=
ext $ λ s, by rw [multiset.to_finsupp_apply, count_to_multiset]
lemma to_multiset_strict_mono : strict_mono (@to_multiset σ) :=
λ m n h,
begin
rw lt_iff_le_and_ne at h ⊢, cases h with h₁ h₂,
split,
{ rw multiset.le_iff_count, intro s, erw [count_to_multiset m s, count_to_multiset], exact h₁ s },
{ intro H, apply h₂, replace H := congr_arg multiset.to_finsupp H, simpa using H }
end
lemma sum_id_lt_of_lt (m n : σ →₀ ℕ) (h : m < n) :
m.sum (λ _, id) < n.sum (λ _, id) :=
begin
rw [← card_to_multiset, ← card_to_multiset],
apply multiset.card_lt_of_lt,
exact to_multiset_strict_mono h
end
variable (σ)
/-- The order on σ →₀ ℕ is well-founded.-/
lemma lt_wf : well_founded (@has_lt.lt (σ →₀ ℕ) _) :=
subrelation.wf (sum_id_lt_of_lt) $ inv_image.wf _ nat.lt_wf
instance decidable_le : decidable_rel (@has_le.le (σ →₀ ℕ) _) :=
λ m n, by rw le_iff; apply_instance
variable {σ}
def antidiagonal (f : σ →₀ ℕ) : ((σ →₀ ℕ) × (σ →₀ ℕ)) →₀ ℕ :=
(f.to_multiset.antidiagonal.map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finsupp
lemma mem_antidiagonal_support {f : σ →₀ ℕ} {p : (σ →₀ ℕ) × (σ →₀ ℕ)} :
p ∈ (antidiagonal f).support ↔ p.1 + p.2 = f :=
begin
erw [multiset.mem_to_finset, multiset.mem_map],
split,
{ rintros ⟨⟨a, b⟩, h, rfl⟩,
rw multiset.mem_antidiagonal at h,
simpa using congr_arg multiset.to_finsupp h },
{ intro h,
refine ⟨⟨p.1.to_multiset, p.2.to_multiset⟩, _, _⟩,
{ simpa using congr_arg to_multiset h },
{ rw [prod.map, to_multiset_to_finsupp, to_multiset_to_finsupp, prod.mk.eta] } }
end
@[simp] lemma antidiagonal_zero : antidiagonal (0 : σ →₀ ℕ) = single (0,0) 1 :=
by rw [← multiset.to_finsupp_singleton]; refl
lemma swap_mem_antidiagonal_support {n : σ →₀ ℕ} {f} (hf : f ∈ (antidiagonal n).support) :
f.swap ∈ (antidiagonal n).support :=
by simpa [mem_antidiagonal_support, add_comm] using hf
end finsupp