Pointwise order on finitely supported functions

This file lifts order structures on α to ι →₀ α.

Main declarations

• Finsupp.orderEmbeddingToFun: The order embedding from finitely supported functions to functions.

@[simp]

theorem Finsupp.support_mapDomain_of_nonneg {α : Type u_3} {β : Type u_4} {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [DecidableEq β] {x : α →₀ M} (hx : 0 ≤ x) (f : α → β) : (mapDomain f x).support = Finset.image f x.support

Order structures

theorem Finsupp.sum_le_sum {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ h₂ : ι → α → β} (h : ∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) : f.sum h₁ ≤ f.sum h₂

theorem Finsupp.sum_nonneg {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} (h : ∀ i ∈ f.support, 0 ≤ h₁ i (f i)) : 0 ≤ f.sum h₁

theorem Finsupp.sum_nonneg' {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} (h : ∀ (i : ι), 0 ≤ h₁ i (f i)) : 0 ≤ f.sum h₁

theorem Finsupp.sum_nonpos {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β} (h : ∀ i ∈ f.support, h₁ i (f i) ≤ 0) : f.sum h₁ ≤ 0

theorem Finsupp.sum_pos {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedCancelAddMonoid β] [AddLeftStrictMono β] {f : ι →₀ α} {g : ι → α → β} (h : ∀ i ∈ f.support, 0 < g i (f i)) (hf : f ≠ 0) : 0 < f.sum g

theorem Finsupp.sum_pos' {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [AddCommMonoid β] [Preorder β] [IsOrderedCancelAddMonoid β] [AddLeftStrictMono β] {f : ι →₀ α} {g : ι → α → β} (h : ∀ i ∈ f.support, 0 ≤ g i (f i)) (hf : ∃ i ∈ f.support, 0 < g i (f i)) : 0 < f.sum g

@[simp]

theorem Finsupp.single_le_single {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a b : α} : single i a ≤ single i b ↔ a ≤ b

theorem Finsupp.single_mono {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} : Monotone (single i)

@[simp]

theorem Finsupp.single_nonneg {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} : 0 ≤ single i a ↔ 0 ≤ a

@[simp]

theorem Finsupp.single_nonpos {ι : Type u_1} {α : Type u_3} [Zero α] [Preorder α] {i : ι} {a : α} : single i a ≤ 0 ↔ a ≤ 0

theorem Finsupp.sum_le_sum_index {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β} (hf : f₁ ≤ f₂) (hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)) (hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) : f₁.sum h ≤ f₂.sum h

theorem Finsupp.embDomain_le_embDomain_iff_le {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Zero α] [LE α] [Std.Refl fun (x1 x2 : α) => x1 ≤ x2] (f : ι ↪ κ) (g₁ g₂ : ι →₀ α) : embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂

theorem Finsupp.embDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Zero α] [Preorder α] (f : ι ↪ κ) : Monotone (embDomain f)

theorem Finsupp.embDomain_lt_embDomain_iff_lt {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [Zero α] [Preorder α] (f : ι ↪ κ) (g₁ g₂ : ι →₀ α) : embDomain f g₁ < embDomain f g₂ ↔ g₁ < g₂

theorem Finsupp.mapDomain_le_mapDomain_iff_le {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [LE α] [Std.Refl fun (x1 x2 : α) => x1 ≤ x2] {f : ι → κ} (h : Function.Injective f) (g₁ g₂ : ι →₀ α) : mapDomain f g₁ ≤ mapDomain f g₂ ↔ g₁ ≤ g₂

theorem Finsupp.mapDomain_lt_mapDomain_iff_lt {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [Preorder α] {f : ι → κ} (h : Function.Injective f) (g₁ g₂ : ι →₀ α) : mapDomain f g₁ < mapDomain f g₂ ↔ g₁ < g₂

Algebraic order structures

instance Finsupp.isOrderedAddMonoid {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (ι →₀ α)

theorem Finsupp.mapDomain_mono {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] {f : ι → κ} : Monotone (mapDomain f)

theorem Finsupp.mapDomain_nonneg {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] {f : ι → κ} {g : ι →₀ α} (hg : 0 ≤ g) : 0 ≤ mapDomain f g

theorem Finsupp.mapDomain_nonpos {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] {f : ι → κ} {g : ι →₀ α} (hg : g ≤ 0) : mapDomain f g ≤ 0

theorem Finsupp.single_le_sum {α : Type u_6} {M : Type u_7} {N : Type u_8} [Zero M] [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] (f : α →₀ M) {g : α → M → N} (h : 0 ≤ fun (x1 : α) (x2 : M) => g x1 x2) (a : α) : (single a (f a)).sum g ≤ f.sum g

theorem Finsupp.single_eval_le_sum {α : Type u_6} {M : Type u_7} {N : Type u_8} [Zero M] [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] (f : α →₀ M) {g : M → N} (hg : g 0 = 0) (h : 0 ≤ fun (x : M) => g x) (a : α) : g (f a) ≤ f.sum fun (x : α) (m : M) => g m

instance Finsupp.isOrderedCancelAddMonoid {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] : IsOrderedCancelAddMonoid (ι →₀ α)

instance Finsupp.addLeftReflectLE {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Preorder α] [AddLeftReflectLE α] : AddLeftReflectLE (ι →₀ α)

instance Finsupp.instPosSMulMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [PosSMulMono α β] : PosSMulMono α (ι →₀ β)

instance Finsupp.instSMulPosMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosMono α β] : SMulPosMono α (ι →₀ β)

instance Finsupp.instPosSMulReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [PosSMulReflectLE α β] : PosSMulReflectLE α (ι →₀ β)

instance Finsupp.instSMulPosReflectLE {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] [SMulPosReflectLE α β] : SMulPosReflectLE α (ι →₀ β)

instance Finsupp.instPosSMulStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [PosSMulStrictMono α β] : PosSMulStrictMono α (ι →₀ β)

instance Finsupp.instSMulPosStrictMono {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosStrictMono α β] : SMulPosStrictMono α (ι →₀ β)

instance Finsupp.instSMulPosReflectLT {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] [SMulPosReflectLT α β] : SMulPosReflectLT α (ι →₀ β)

@[instance_reducible]

instance Finsupp.orderBot {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsBotZeroClass α] : OrderBot (ι →₀ α)

Equations

• Finsupp.orderBot = { bot := 0, bot_le := ⋯ }

instance Finsupp.instIsBotZeroClass {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsBotZeroClass α] : IsBotZeroClass (ι →₀ α)

@[deprecated bot_eq_zero (since := "2026-05-07")]

theorem Finsupp.bot_eq_zero {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [IsBotZeroClass α] : ⊥ = 0

@[simp]

theorem Finsupp.add_eq_zero_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] (f g : ι →₀ α) : f + g = 0 ↔ f = 0 ∧ g = 0

theorem Finsupp.le_iff' {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] (f g : ι →₀ α) {s : Finset ι} (hf : f.support ⊆ s) : f ≤ g ↔ ∀ i ∈ s, f i ≤ g i

theorem Finsupp.le_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] (f g : ι →₀ α) : f ≤ g ↔ ∀ i ∈ f.support, f i ≤ g i

theorem Finsupp.support_monotone {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] : Monotone support

theorem Finsupp.support_mono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] {f g : ι →₀ α} [CanonicallyOrderedAdd α] (hfg : f ≤ g) : f.support ⊆ g.support

@[instance_reducible]

instance Finsupp.decidableLE {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [DecidableLE α] : DecidableLE (ι →₀ α)

Equations

• f.decidableLE g = decidable_of_iff (∀ i ∈ f.support, f i ≤ g i) ⋯

@[instance_reducible]

instance Finsupp.decidableLT {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [DecidableLE α] : DecidableLT (ι →₀ α)

Equations

• Finsupp.decidableLT = decidableLTOfDecidableLE

@[simp]

theorem Finsupp.single_le_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] {i : ι} {x : α} {f : ι →₀ α} : single i x ≤ f ↔ x ≤ f i

@[instance_reducible]

noncomputable instance Finsupp.tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] : Sub (ι →₀ α)

This is called tsub for truncated subtraction, to distinguish it with subtraction in an additive group.

Equations

• Finsupp.tsub = { sub := Finsupp.zipWith (fun (m n : α) => m - n) ⋯ }

instance Finsupp.orderedSub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] : OrderedSub (ι →₀ α)

instance Finsupp.instCanonicallyOrderedAddOfAddLeftMono {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftMono α] : CanonicallyOrderedAdd (ι →₀ α)

@[simp]

theorem Finsupp.coe_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (f g : ι →₀ α) : ⇑(f - g) = ⇑f - ⇑g

theorem Finsupp.tsub_apply {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (f g : ι →₀ α) (a : ι) : (f - g) a = f a - g a

@[simp]

theorem Finsupp.single_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {i : ι} {a b : α} : single i (a - b) = single i a - single i b

theorem Finsupp.support_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {f1 f2 : ι →₀ α} : (f1 - f2).support ⊆ f1.support

theorem Finsupp.subset_support_tsub {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [DecidableEq ι] {f1 f2 : ι →₀ α} : f1.support \ f2.support ⊆ (f1 - f2).support

theorem Finsupp.mapDomain_tsub {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {f : ι → κ} (h : Function.Injective f) (f1 f2 : ι →₀ α) : mapDomain f (f1 - f2) = mapDomain f f1 - mapDomain f f2

theorem Finsupp.embDomain_tsub {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (f : ι ↪ κ) (f1 f2 : ι →₀ α) : embDomain f (f1 - f2) = embDomain f f1 - embDomain f f2

theorem Finsupp.support_add_eq_union {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] {f1 f2 : ι →₀ α} [DecidableEq ι] : (f1 + f2).support = f1.support ∪ f2.support

The support of a sum is the union of the supports, when the coefficients satisfy CanonicallyOrderedAdd.

In the case where the supports are disjoint, there is also Finsupp.support_add_eq, which holds in any AddZeroClass.

@[simp]

theorem Finsupp.support_inf {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [IsBotZeroClass α] [DecidableEq ι] (f g : ι →₀ α) : (f ⊓ g).support = f.support ∩ g.support

@[simp]

theorem Finsupp.support_sup {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [IsBotZeroClass α] [DecidableEq ι] (f g : ι →₀ α) : (f ⊔ g).support = f.support ∪ g.support

theorem Finsupp.disjoint_iff {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [IsBotZeroClass α] {f g : ι →₀ α} : Disjoint f g ↔ Disjoint f.support g.support

Some lemmas about ℕ

theorem Finsupp.sub_single_one_add {ι : Type u_1} {a : ι} {u u' : ι →₀ ℕ} (h : u a ≠ 0) : u - single a 1 + u' = u + u' - single a 1

theorem Finsupp.add_sub_single_one {ι : Type u_1} {a : ι} {u u' : ι →₀ ℕ} (h : u' a ≠ 0) : u + (u' - single a 1) = u + u' - single a 1

theorem Finsupp.sub_add_single_one_cancel {ι : Type u_1} {u : ι →₀ ℕ} {i : ι} (h : u i ≠ 0) : u - single i 1 + single i 1 = u

theorem Finsupp.isLowerSet_range_embDomain {α : Type u_3} {β : Type u_4} (f : α ↪ β) : IsLowerSet (Set.range (embDomain f))