WeightedNetKAT.OmegaContinuousNonUnitalSemiring

source

@[simp]

theorem Chain.mk_apply {β : Type u_1} [Preorder β] (f : ℕ → β) (hf : Monotone f) (a : ℕ) :

{ toFun := f, monotone' := hf } a = f a

source

@[simp]

theorem OmegaCompletePartialOrder.ωSup_const {α : Type u_1} [OmegaCompletePartialOrder α] (x : α) :

ωSup { toFun := fun (x_1 : ℕ) => x, monotone' := ⋯ } = x

source

theorem OmegaCompletePartialOrder.ωSup_ωSup_eq_ωSup {α : Type u_1} [OmegaCompletePartialOrder α] (f : ℕ →o ℕ →o α) :

ωSup { toFun := fun (i : ℕ) => ωSup { toFun := fun (j : ℕ) => (f i) j, monotone' := ⋯ }, monotone' := ⋯ } = ωSup { toFun := fun (i : ℕ) => (f i) i, monotone' := ⋯ }

source

theorem OmegaCompletePartialOrder.ωSup_ωSup_eq_ωSup' {α : Type u_1} [OmegaCompletePartialOrder α] (f : ℕ → ℕ → α) (hf : Monotone f) (hf' : ∀ (i : ℕ), Monotone (f i)) :

ωSup { toFun := fun (i : ℕ) => ωSup { toFun := fun (j : ℕ) => f i j, monotone' := ⋯ }, monotone' := ⋯ } = ωSup { toFun := fun (i : ℕ) => f i i, monotone' := ⋯ }

source

class IsPositiveOrderedAddMonoid (𝒮 : Type u_1) [AddCommMonoid 𝒮] [PartialOrder 𝒮] [OrderBot 𝒮] extends IsOrderedAddMonoid 𝒮 :

Prop

add_le_add_left (a b : 𝒮) : a ≤ b → ∀ (c : 𝒮), a + c ≤ b + c
add_le_add_right (a b : 𝒮) : a ≤ b → ∀ (c : 𝒮), c + a ≤ c + b
bot_eq_zero : ⊥ = 0

Instances

source

@[simp]

theorem nonpos_iff_eq_zero' {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] {a : α} :

a ≤ 0 ↔ a = 0

source

@[simp]

theorem zero_le'' {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] (a : α) :

0 ≤ a

source

theorem Finset.sum_range_le_sup_of_le {𝒮 : Type u_1} [Semiring 𝒮] [PartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {m n : ℕ} {f g : ℕ → 𝒮} (h : f ≤ g) :

∑ i ∈ range n, f i ≤ ∑ i ∈ range (max m n), g i

source

instance instSubsingletonAddUnitsOfIsPositiveOrderedAddMonoid (𝒮 : Type u_1) [AddCommMonoid 𝒮] [PartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] :

Subsingleton (AddUnits 𝒮)

source

class OmegaContinuousNonUnitalSemiring (𝒮 : Type u_1) [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] :

Prop

ωScottContinuous_add_right (x : 𝒮) : OmegaCompletePartialOrder.ωScottContinuous fun (x_1 : 𝒮) => x_1 + x
ωScottContinuous_add_left (x : 𝒮) : OmegaCompletePartialOrder.ωScottContinuous fun (x_1 : 𝒮) => x + x_1
ωScottContinuous_mul_right (x : 𝒮) : OmegaCompletePartialOrder.ωScottContinuous fun (x_1 : 𝒮) => x_1 * x
ωScottContinuous_mul_left (x : 𝒮) : OmegaCompletePartialOrder.ωScottContinuous fun (x_1 : 𝒮) => x * x_1

Instances

source

theorem ωSup_add {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f : OmegaCompletePartialOrder.Chain 𝒮} (a : 𝒮) :

OmegaCompletePartialOrder.ωSup f + a = OmegaCompletePartialOrder.ωSup { toFun := fun (i : ℕ) => f i + a, monotone' := ⋯ }

source

theorem add_ωSup {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f : OmegaCompletePartialOrder.Chain 𝒮} (a : 𝒮) :

a + OmegaCompletePartialOrder.ωSup f = OmegaCompletePartialOrder.ωSup { toFun := fun (i : ℕ) => a + f i, monotone' := ⋯ }

source

theorem ωSup_mul {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f : OmegaCompletePartialOrder.Chain 𝒮} (a : 𝒮) :

OmegaCompletePartialOrder.ωSup f * a = OmegaCompletePartialOrder.ωSup { toFun := fun (i : ℕ) => f i * a, monotone' := ⋯ }

source

theorem mul_ωSup {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f : OmegaCompletePartialOrder.Chain 𝒮} (a : 𝒮) :

a * OmegaCompletePartialOrder.ωSup f = OmegaCompletePartialOrder.ωSup { toFun := fun (i : ℕ) => a * f i, monotone' := ⋯ }

source

theorem ωSup_add_ωSup {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f g : OmegaCompletePartialOrder.Chain 𝒮} :

OmegaCompletePartialOrder.ωSup f + OmegaCompletePartialOrder.ωSup g = OmegaCompletePartialOrder.ωSup { toFun := fun (i : ℕ) => f i + g i, monotone' := ⋯ }

source

theorem ωSup_mul_ωSup {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f g : OmegaCompletePartialOrder.Chain 𝒮} :

OmegaCompletePartialOrder.ωSup f * OmegaCompletePartialOrder.ωSup g = OmegaCompletePartialOrder.ωSup { toFun := fun (i : ℕ) => f i * g i, monotone' := ⋯ }

source

instance instIsPositiveOrderedAddMonoidForall {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} :

IsPositiveOrderedAddMonoid (X → 𝒮)

source

@[simp]

theorem ωSup_eq_zero_iff {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] (C : OmegaCompletePartialOrder.Chain 𝒮) :

OmegaCompletePartialOrder.ωSup C = 0 ↔ ∀ (i : ℕ), C i = 0

source

noncomputable def ωSum {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] (f : X → 𝒮) :

𝒮

Sum over countable X

Equations

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

Instances For

source

def «termω∑_,_» :

Lean.ParserDescr

Sum over countable X

Equations

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

Instances For

source

@[simp]

theorem ωSum_zero {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] :

ω∑ (x : X), 0 = 0

source

@[simp]

theorem ωSum_eq_zero_iff {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] {f : X → 𝒮} :

ω∑ (i : X), f i = 0 ↔ ∀ (x : X), f x = 0

source

theorem ωSum_mono {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] {f g : X → 𝒮} (h : f ≤ g) :

ω∑ (n : X), f n ≤ ω∑ (n : X), g n

source

theorem ωSum_le_of_finset {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] {f : X → 𝒮} {a : 𝒮} (h : ∀ (S : Finset X), ∑ x ∈ S, f x ≤ a) :

ω∑ (x : X), f x ≤ a

source

theorem le_ωSum_of_finset {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] {f : X → 𝒮} (S : Finset X) :

∑ x ∈ S, f x ≤ ω∑ (x : X), f x

source

theorem ωSum_finset {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {I : Type u_3} [DecidableEq I] [Countable I] (S : Finset I) (f : I → 𝒮) :

ω∑ (x : ↥S), f ↑x = ∑ x ∈ S, f x

source

theorem ωSum_fintype {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {I : Type u_3} [DecidableEq I] [Countable I] [Fintype I] (f : I → 𝒮) :

ω∑ (x : I), f x = ∑ x : I, f x

source

@[simp]

theorem asdsad {𝒮 : Type u_1} [OmegaCompletePartialOrder 𝒮] {X : Type u_2} {c : OmegaCompletePartialOrder.Chain (X → 𝒮)} {x : X} :

OmegaCompletePartialOrder.ωSup c x = OmegaCompletePartialOrder.ωSup (c.map { toFun := fun (x_1 : X → 𝒮) => x_1 x, monotone' := ⋯ })

source

@[simp]

theorem ωSum_apply {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {X : Type u_2} [Countable X] {Y : Type u_3} {f : X → Y → 𝒮} {y : Y} :

(ω∑ (x : X), f x) y = ω∑ (x : X), f x y

source

theorem ωSum_nat_eq_ωSup {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {f : ℕ → 𝒮} :

ω∑ (x : ℕ), f x = OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => ∑ x ∈ Finset.range n, f x, monotone' := ⋯ }

source

theorem ωSum_nat_eq_ωSup_succ {𝒮 : Type u_1} [AddCommMonoid 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {f : ℕ → 𝒮} :

ω∑ (x : ℕ), f x = OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => ∑ x ∈ Finset.range (n + 1), f x, monotone' := ⋯ }

source

theorem Finset.sum_ωScottContinuous {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [DecidableEq X] (S : Finset X) :

OmegaCompletePartialOrder.ωScottContinuous fun (f : X → 𝒮) => ∑ i ∈ S, f i

source

theorem ωSum_ωSup {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] (C : OmegaCompletePartialOrder.Chain (X → 𝒮)) :

ω∑ (n : X), OmegaCompletePartialOrder.ωSup C n = OmegaCompletePartialOrder.ωSup { toFun := fun (x : ℕ) => ω∑ (n : X), C x n, monotone' := ⋯ }

source

theorem ωSum_ωSup' {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] (C : X → OmegaCompletePartialOrder.Chain 𝒮) :

ω∑ (n : X), OmegaCompletePartialOrder.ωSup (C n) = OmegaCompletePartialOrder.ωSup { toFun := fun (x : ℕ) => ω∑ (n : X), (C n) x, monotone' := ⋯ }

source

theorem sum_ωSup {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [DecidableEq X] (S : Finset X) (C : OmegaCompletePartialOrder.Chain (X → 𝒮)) :

∑ n ∈ S, OmegaCompletePartialOrder.ωSup C n = OmegaCompletePartialOrder.ωSup { toFun := fun (x : ℕ) => ∑ n ∈ S, C x n, monotone' := ⋯ }

source

theorem sum_ωSup' {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [DecidableEq X] (S : Finset X) (C : X → OmegaCompletePartialOrder.Chain 𝒮) :

∑ n ∈ S, OmegaCompletePartialOrder.ωSup (C n) = OmegaCompletePartialOrder.ωSup { toFun := fun (x : ℕ) => ∑ n ∈ S, (C n) x, monotone' := ⋯ }

source

theorem ωSum_nat_eq_succ {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {f : ℕ → 𝒮} :

ω∑ (x : ℕ), f x = f 0 + ω∑ (x : ℕ), f (x + 1)

source

theorem ωSum_add {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] {f g : X → 𝒮} :

ω∑ (x : X), (f x + g x) = ω∑ (x : X), f x + ω∑ (x : X), g x

source

theorem ωSum_mul_left {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] {f : X → 𝒮} {a : 𝒮} :

ω∑ (x : X), a * f x = a * ω∑ (x : X), f x

source

theorem ωSum_mul_right {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] {f : X → 𝒮} {a : 𝒮} :

ω∑ (x : X), f x * a = (ω∑ (x : X), f x) * a

source

theorem ωSum_sum_comm {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] {Y : Type u_3} (S : Finset Y) {f : X → Y → 𝒮} :

ω∑ (x : X), ∑ y ∈ S, f x y = ∑ y ∈ S, ω∑ (x : X), f x y

source

theorem ωSum_comm_le {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] {Y : Type u_3} [Countable Y] {f : X → Y → 𝒮} :

ω∑ (x : X) (y : Y), f x y ≤ ω∑ (y : Y) (x : X), f x y

source

theorem ωSum_comm {𝒮 : Type u_1} [NonUnitalSemiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {X : Type u_2} [Countable X] {Y : Type u_3} [DecidableEq Y] [Countable Y] {f : X → Y → 𝒮} :

ω∑ (x : X) (y : Y), f x y = ω∑ (y : Y) (x : X), f x y

source

theorem Function.Injective.ωSum_eq {α : Type u_3} {ι : Type u_4} {γ : Type u_5} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [Countable ι] [Countable γ] {g : γ → ι} (hg : Injective g) {f : ι → α} (hf : support f ⊆ Set.range g) :

ω∑ (c : γ), f (g c) = ω∑ (b : ι), f b

source

theorem ωSum_subtype_eq_of_supp_subset {α : Type u_3} {ι : Type u_4} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [Countable ι] {f : ι → α} {s : Set ι} (hs : Function.support f ⊆ s) :

ω∑ (x : ↑s), f ↑x = ω∑ (x : ι), f x

source

theorem ωSum_substype_supp {α : Type u_3} {ι : Type u_4} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [Countable ι] (f : ι → α) :

ω∑ (x : ↑(Function.support f)), f ↑x = ω∑ (x : ι), f x

source

theorem ωSum_eq_ωSum_of_ne_one_bij {α : Type u_3} {ι : Type u_4} {γ : Type u_5} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [Countable ι] [Countable γ] {f : ι → α} {g : γ → α} (i : ↑(Function.support g) → ι) (hi : Function.Injective i) (hf : Function.support f ⊆ Set.range i) (hfg : ∀ (x : ↑(Function.support g)), f (i x) = g ↑x) :

ω∑ (x : ι), f x = ω∑ (y : γ), g y

source

theorem ωSum_eq_single {α : Type u_3} {ι : Type u_4} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [Countable ι] {f : ι → α} (x : ι) (hf : ∀ (x' : ι), x' ≠ x → f x' = 0) :

ω∑ (x : ι), f x = f x

source

theorem ωSum_prod {α : Type u_3} {β : Type u_4} {γ : Type u_5} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] [Countable β] [Countable γ] {f : β × γ → α} :

ω∑ (p : β × γ), f p = ω∑ (b : β) (c : γ), f (b, c)

source

theorem ωSum_prod' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [NonUnitalSemiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] [Countable β] [Countable γ] {f : β → γ → α} :

ω∑ (p : β × γ), f p.1 p.2 = ω∑ (b : β) (c : γ), f b c