structure Countsupp (α M : Type) [Zero M] : Type

Countsupp α M, denoted α →c M, is the type of functions f : α → M such that f x = 0 for all but countably many x.

• toFun : α → M
• countable : (Function.support self.toFun).Countable

def «term_→c_» : Lean.TrailingParserDescr

Countsupp α M, denoted α →c M, is the type of functions f : α → M such that f x = 0 for all but countably many x.

Equations

• «term_→c_» = Lean.ParserDescr.trailingNode `«term_→c_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →c ") (Lean.ParserDescr.cat `term 25))

def Countsupp.support {α M : Type} [Zero M] (f : α →c M) : Set α

Equations

• f.support = Function.support f.toFun

@[implicit_reducible]

instance Countsupp.instFunLike {α M : Type} [Zero M] : FunLike (α →c M) α M

Equations

• Countsupp.instFunLike = { coe := Countsupp.toFun, coe_injective' := ⋯ }

theorem Countsupp.ext {α M : Type} [Zero M] {f g : α →c M} (h : ∀ (a : α), f a = g a) : f = g

theorem Countsupp.ext_iff {α M : Type} [Zero M] {f g : α →c M} : f = g ↔ ∀ (a : α), f a = g a

theorem Countsupp.ne_iff {α M : Type} [Zero M] {f g : α →c M} : f ≠ g ↔ ∃ (a : α), f a ≠ g a

theorem Countsupp.toFun_apply {α M : Type} [Zero M] (c : α →c M) (x : α) : c.toFun x = c x

@[simp]

theorem Countsupp.coe_mk {α M : Type} [Zero M] (f : α → M) (h : (Function.support f).Countable) : ⇑{ toFun := f, countable := h } = f

@[implicit_reducible]

instance Countsupp.instZero {α M : Type} [Zero M] : Zero (α →c M)

Equations

• Countsupp.instZero = { zero := { toFun := 0, countable := ⋯ } }

@[simp]

theorem Countsupp.coe_zero {α M : Type} [Zero M] : ⇑0 = 0

theorem Countsupp.zero_apply {α M : Type} [Zero M] {a : α} : 0 a = 0

@[simp]

theorem Countsupp.support_zero {α M : Type} [Zero M] : support 0 = ∅

theorem Countsupp.ite_apply {α M : Type} [Zero M] {p : Prop} [Decidable p] {f g : α →c M} {a : α} : (if p then f else g) a = if p then f a else g a

@[implicit_reducible]

instance Countsupp.instInhabited {α M : Type} [Zero M] : Inhabited (α →c M)

Equations

• Countsupp.instInhabited = { default := 0 }

@[simp]

theorem Countsupp.mem_support_iff {α M : Type} [Zero M] {f : α →c M} {a : α} : a ∈ f.support ↔ f a ≠ 0

@[simp]

theorem Countsupp.fun_support_eq {α M : Type} [Zero M] (f : α →c M) : Function.support ⇑f = f.support

theorem Countsupp.notMem_support_iff {α M : Type} [Zero M] {f : α →c M} {a : α} : a ∉ f.support ↔ f a = 0

theorem Countsupp.support_countable {α M : Type} [Zero M] {f : α →c M} : f.support.Countable

instance Countsupp.support_countable' {α M : Type} [Zero M] {f : α →c M} : Countable ↑f.support

@[simp]

theorem Countsupp.coe_eq_zero {α M : Type} [Zero M] {f : α →c M} : ⇑f = 0 ↔ f = 0

theorem Countsupp.ext_iff' {α M : Type} [Zero M] {f g : α →c M} : f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x

@[implicit_reducible]

instance Countsupp.instAdd {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : Add (X →c 𝒮)

Equations

• Countsupp.instAdd = { add := fun (a b : X →c 𝒮) => { toFun := fun (x : X) => a x + b x, countable := ⋯ } }

@[simp]

theorem Countsupp.add_apply {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (a b : X →c 𝒮) (x : X) : (a + b) x = a x + b x

@[implicit_reducible]

instance Countsupp.instMul {X 𝒮 : Type} [Semiring 𝒮] : Mul (X →c 𝒮)

Equations

• Countsupp.instMul = { mul := fun (a b : X →c 𝒮) => { toFun := fun (x : X) => a x * b x, countable := ⋯ } }

@[simp]

theorem Countsupp.mul_apply {X 𝒮 : Type} [Semiring 𝒮] (a b : X →c 𝒮) (x : X) : (a * b) x = a x * b x

@[implicit_reducible]

instance Countsupp.instHMul {X 𝒮 : Type} [Semiring 𝒮] : HMul 𝒮 (X →c 𝒮) (X →c 𝒮)

Equations

• Countsupp.instHMul = { hMul := fun (a : 𝒮) (b : X →c 𝒮) => { toFun := fun (x : X) => a * b x, countable := ⋯ } }

@[simp]

theorem Countsupp.hMul_apply_left {X 𝒮 : Type} [Semiring 𝒮] (a : 𝒮) (b : X →c 𝒮) (x : X) : (a * b) x = a * b x

@[implicit_reducible]

instance Countsupp.instHMul_1 {X 𝒮 : Type} [Semiring 𝒮] : HMul (X →c 𝒮) 𝒮 (X →c 𝒮)

Equations

• Countsupp.instHMul_1 = { hMul := fun (a : X →c 𝒮) (b : 𝒮) => { toFun := fun (x : X) => a x * b, countable := ⋯ } }

@[simp]

theorem Countsupp.hMul_apply_right {X 𝒮 : Type} [Semiring 𝒮] (a : X →c 𝒮) (b : 𝒮) (x : X) : (a * b) x = a x * b

@[implicit_reducible]

instance Countsupp.instNonUnitalSemiring {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : NonUnitalSemiring (X →c 𝒮)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Countsupp.instLE {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] : LE (X →c 𝒮)

Equations

• Countsupp.instLE = { le := fun (f g : X →c 𝒮) => ∀ (x : X), f x ≤ g x }

@[implicit_reducible]

instance Countsupp.instPartialOrder {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] : PartialOrder (X →c 𝒮)

Equations

• Countsupp.instPartialOrder = { toLE := Countsupp.instLE, lt := fun (a b : X →c 𝒮) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance Countsupp.instOmegaCompletePartialOrder {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : OmegaCompletePartialOrder (X →c 𝒮)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Countsupp.ωSup_apply {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type} [Fintype X] [DecidableEq 𝒮] (C : OmegaCompletePartialOrder.Chain (X →c 𝒮)) (x : X) : (OmegaCompletePartialOrder.ωSup C) x = OmegaCompletePartialOrder.ωSup (C.map { toFun := fun (x_1 : X →c 𝒮) => x_1 x, monotone' := ⋯ })

@[implicit_reducible]

instance Countsupp.instOrderBot {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : OrderBot (X →c 𝒮)

Equations

• Countsupp.instOrderBot = { bot := 0, bot_le := ⋯ }

instance Countsupp.instMulLeftMono {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [MulLeftMono 𝒮] : MulLeftMono (X →c 𝒮)

instance Countsupp.instMulRightMono {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [MulRightMono 𝒮] : MulRightMono (X →c 𝒮)

instance Countsupp.instIsPositiveOrderedAddMonoid {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] : IsPositiveOrderedAddMonoid (X →c 𝒮)

instance Countsupp.instOmegaContinuousNonUnitalSemiring {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type} : OmegaContinuousNonUnitalSemiring (X →c 𝒮)

noncomputable def Countsupp.bind {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {Y : Type} (f : X →c 𝒮) (g : X → Y →c 𝒮) : Y →c 𝒮

Equations

• f.bind g = { toFun := fun (y : Y) => ω∑ (x : ↑f.support), f ↑x * (g ↑x) y, countable := ⋯ }

@[simp]

theorem Countsupp.bind_apply {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {Y : Type} (f : X →c 𝒮) (g : X → Y →c 𝒮) (y : Y) : (f.bind g) y = ω∑ (i : ↑f.support), f ↑i * (g ↑i) y

theorem Countsupp.bind_mono_right {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {Y : Type} (f : X →c 𝒮) (g₁ g₂ : X → Y →c 𝒮) (h : g₁ ≤ g₂) : f.bind g₁ ≤ f.bind g₂

theorem Countsupp.bind_mono_left {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {Y : Type} {f₁ f₂ : X →c 𝒮} (g : X → Y →c 𝒮) (h : f₁ ≤ f₂) : f₁.bind g ≤ f₂.bind g

theorem Countsupp.bind_continuous_right {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {Y : Type} (f : X →c 𝒮) : OmegaCompletePartialOrder.ωScottContinuous f.bind

@[simp]

theorem Countsupp.sum_apply {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq X] {Y : Type} {f : X → Y →c 𝒮} {y : Y} (S : Finset X) : (∑ x ∈ S, f x) y = ∑ x ∈ S, (f x) y

@[simp]

theorem Countsupp.ωSum_apply {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Countable X] {Y : Type} {f : X → Y →c 𝒮} {y : Y} : (ω∑ (x : X), f x) y = ω∑ (x : X), (f x) y

theorem Countsupp.bind_continuous_left {X 𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {Y : Type} (g : X → Y →c 𝒮) : OmegaCompletePartialOrder.ωScottContinuous fun (f : X →c 𝒮) => f.bind g