Weighted semiring instances

We provide a set of proven sound weighted semirings, including instances for Kleene-star and ω-continuity for these.

Most of the semirings are computable (i.e. have computable instances of Semiring), but some, specifically those that do operations on reals, have noncomputable instances for now.

def «command_Instantiate_computableSemiring_=>_» : Lean.ParserDescr

Equations

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

@[implicit_reducible]

instance ENat.WithBot.instReprWithBot_weightedNetKAT : Repr (WithBot ℕ∞)

Equations

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

theorem ENat.WithBot.cases_on {P : WithBot ℕ∞ → Prop} (x : WithBot ℕ∞) (bot : P ⊥) (top : P ⊤) (nat : ∀ (a : ℕ), P ↑a) : P x

@[simp]

theorem ENat.WithBot.top_add {x : WithBot ℕ∞} (hx : x ≠ ⊥) : ⊤ + x = ⊤

@[simp]

theorem ENat.WithBot.add_top {x : WithBot ℕ∞} (hx : x ≠ ⊥) : x + ⊤ = ⊤

@[simp]

theorem ENat.WithBot.add_eq_top_iff {x y : WithBot ℕ∞} : x + y = ⊤ ↔ x = ⊤ ∧ y ≠ ⊥ ∨ x ≠ ⊥ ∧ y = ⊤

theorem ENat.WithBot.add_top_eq {x : WithBot ℕ∞} : x + ⊤ = if x = ⊥ then ⊥ else ⊤

theorem ENat.WithBot.iSup_eq_bot {ι : Type u_1} {f : ι → WithBot ℕ∞} : ⨆ (i : ι), f i = ⊥ ↔ ∀ (i : ι), f i = ⊥

theorem ENat.WithBot.iSup_eq_' {ι : Type u_1} [Nonempty ι] {f : ι → WithBot ℕ∞} (h : ∃ (i : ι), f i ≠ ⊥) : ⨆ (i : ι), f i = ↑(⨆ (i : ι), WithBot.unbotD 0 (f i))

theorem ENat.WithBot.iSup_add {ι : Type u_1} [Nonempty ι] {f : ι → WithBot ℕ∞} {a : WithBot ℕ∞} : (⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a

theorem ENat.WithBot.add_iSup {ι : Type u_1} [Nonempty ι] {f : ι → WithBot ℕ∞} {a : WithBot ℕ∞} : a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

def Weighted.Tropical : Type

Equations

• Weighted.Tropical = ℕ∞

@[implicit_reducible]

instance Weighted.instDecidableEqTropical : DecidableEq Tropical

Equations

• Weighted.instDecidableEqTropical = Weighted.instDecidableEqTropical._aux_1

@[implicit_reducible]

instance Weighted.instTopTropical : Top Tropical

Equations

• Weighted.instTopTropical = { top := Weighted.instTopTropical._aux_1 }

def Weighted.Tropical.min (a b : ℕ∞) : ℕ∞

Equations

• Weighted.Tropical.min a b = if a ≤ b then a else b

@[simp]

theorem Weighted.Tropical.min_eq_sup (a b : ℕ∞) : min a b = Min.min a b

@[implicit_reducible]

def Weighted.Tropical.instWSemiringENat : WSemiring ℕ∞

Equations

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

@[implicit_reducible]

def Weighted.Tropical.instWLEENat : WLE ℕ∞

Equations

• Weighted.Tropical.instWLEENat = { wle := fun (x1 x2 : ℕ∞) => x1 ≥ x2 }

@[implicit_reducible]

def Weighted.Tropical.instWPartialOrderENat : WPartialOrder ℕ∞

Equations

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

@[implicit_reducible]

noncomputable def Weighted.Tropical.instWOmegaContinuousNonUnitalSemiringENat : WOmegaContinuousNonUnitalSemiring ℕ∞

Equations

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

@[implicit_reducible]

def Weighted.Tropical.instWKStarENat : WKStar ℕ∞

Equations

• Weighted.Tropical.instWKStarENat = { wkstar := fun (x : ℕ∞) => 𝟙 }

theorem Weighted.Tropical.instLawfulWKStarENat : LawfulWKStar ℕ∞

@[implicit_reducible]

instance Weighted.Tropical.instSemiring : Semiring Tropical

Equations

• Weighted.Tropical.instSemiring = WSemiring.toSemiring ℕ∞

@[implicit_reducible]

instance Weighted.Tropical.instKStar : KStar Tropical

Equations

• Weighted.Tropical.instKStar = WKStar.toKStar ℕ∞

@[implicit_reducible]

instance Weighted.Tropical.instDecidableLE : DecidableLE Tropical

Equations

• Weighted.Tropical.instDecidableLE = WPartialOrder.toDecidableLE ℕ∞

@[implicit_reducible]

noncomputable instance Weighted.Tropical.instOrderBot : OrderBot Tropical

Equations

• Weighted.Tropical.instOrderBot = WOmegaContinuousNonUnitalSemiring.toOrderBot ℕ∞

@[implicit_reducible]

instance Weighted.Tropical.instOfNatOfENat {n✝ : ℕ} [OfNat ℕ∞ n✝] : OfNat Tropical n✝

Equations

• Weighted.Tropical.instOfNatOfENat = { ofNat := OfNat.ofNat n✝ }

instance Weighted.Tropical.instMulRightMono : MulRightMono Tropical

instance Weighted.Tropical.instLawfulKStar : LawfulKStar Tropical

@[implicit_reducible]

noncomputable instance Weighted.Tropical.instOmegaCompletePartialOrder : OmegaCompletePartialOrder Tropical

Equations

• Weighted.Tropical.instOmegaCompletePartialOrder = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder ℕ∞

instance Weighted.Tropical.instMulLeftMono : MulLeftMono Tropical

instance Weighted.Tropical.instOmegaContinuousNonUnitalSemiring : OmegaContinuousNonUnitalSemiring Tropical

instance Weighted.Tropical.instIsPositiveOrderedAddMonoid : IsPositiveOrderedAddMonoid Tropical

@[implicit_reducible]

instance Weighted.Tropical.instReprOfENat [Repr ℕ∞] : Repr Tropical

Equations

• Weighted.Tropical.instReprOfENat = inst✝

@[implicit_reducible]

instance Weighted.Tropical.instPartialOrder : PartialOrder Tropical

Equations

• Weighted.Tropical.instPartialOrder = WPartialOrder.toPartialOrder ℕ∞

def Weighted.Arctic : Type

Equations

• Weighted.Arctic = WithBot ℕ∞

@[implicit_reducible]

instance Weighted.instDecidableEqArctic : DecidableEq Arctic

Equations

• Weighted.instDecidableEqArctic = Weighted.instDecidableEqArctic._aux_1

@[implicit_reducible]

instance Weighted.instTopArctic : Top Arctic

Equations

• Weighted.instTopArctic = { top := Weighted.instTopArctic._aux_1 }

def Weighted.Arctic.max : WithBot ℕ∞ → WithBot ℕ∞ → WithBot ℕ∞

Equations

• Weighted.Arctic.max x✝ (some none) = ⊤
• Weighted.Arctic.max (some none) x✝ = ⊤
• Weighted.Arctic.max (some (some a)) (some (some b)) = some (some (max a b))
• Weighted.Arctic.max none x✝ = x✝
• Weighted.Arctic.max x✝ none = x✝

@[simp]

theorem Weighted.Arctic.max_eq_sup (a b : WithBot ℕ∞) : max a b = Max.max a b

def Weighted.Arctic.add : WithBot ℕ∞ → WithBot ℕ∞ → WithBot ℕ∞

Equations

• Weighted.Arctic.add none x✝ = ⊥
• Weighted.Arctic.add x✝ none = ⊥
• Weighted.Arctic.add x✝ (some none) = ⊤
• Weighted.Arctic.add (some none) x✝ = ⊤
• Weighted.Arctic.add (some (some a)) (some (some b)) = some (some (a + b))

@[simp]

theorem Weighted.Arctic.add_eq_hadd (a b : WithBot ℕ∞) : add a b = a + b

@[implicit_reducible]

def Weighted.Arctic.instWSemiringWithBotENat : WSemiring (WithBot ℕ∞)

Equations

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

@[implicit_reducible]

def Weighted.Arctic.instWLEWithBotENat : WLE (WithBot ℕ∞)

Equations

• Weighted.Arctic.instWLEWithBotENat = { wle := fun (x1 x2 : WithBot ℕ∞) => x1 ≤ x2 }

@[implicit_reducible]

def Weighted.Arctic.instWPartialOrderWithBotENat : WPartialOrder (WithBot ℕ∞)

Equations

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

@[implicit_reducible]

noncomputable def Weighted.Arctic.instWOmegaContinuousNonUnitalSemiringWithBotENat : WOmegaContinuousNonUnitalSemiring (WithBot ℕ∞)

Equations

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

@[implicit_reducible]

def Weighted.Arctic.instWKStarWithBotENat : WKStar (WithBot ℕ∞)

Equations

• Weighted.Arctic.instWKStarWithBotENat = { wkstar := fun (a : WithBot ℕ∞) => if a ≤ 0 then 0 else ⊤ }

theorem Weighted.Arctic.instLawfulWKStarWithBotENat : LawfulWKStar (WithBot ℕ∞)

@[implicit_reducible]

instance Weighted.Arctic.instSemiring : Semiring Arctic

Equations

• Weighted.Arctic.instSemiring = WSemiring.toSemiring (WithBot ℕ∞)

instance Weighted.Arctic.instLawfulKStar : LawfulKStar Arctic

@[implicit_reducible]

instance Weighted.Arctic.instDecidableLE : DecidableLE Arctic

Equations

• Weighted.Arctic.instDecidableLE = WPartialOrder.toDecidableLE (WithBot ℕ∞)

@[implicit_reducible]

instance Weighted.Arctic.instReprOfWithBotENat [Repr (WithBot ℕ∞)] : Repr Arctic

Equations

• Weighted.Arctic.instReprOfWithBotENat = inst✝

instance Weighted.Arctic.instMulLeftMono : MulLeftMono Arctic

instance Weighted.Arctic.instIsPositiveOrderedAddMonoid : IsPositiveOrderedAddMonoid Arctic

instance Weighted.Arctic.instMulRightMono : MulRightMono Arctic

@[implicit_reducible]

noncomputable instance Weighted.Arctic.instOmegaCompletePartialOrder : OmegaCompletePartialOrder Arctic

Equations

• Weighted.Arctic.instOmegaCompletePartialOrder = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder (WithBot ℕ∞)

@[implicit_reducible]

noncomputable instance Weighted.Arctic.instOrderBot : OrderBot Arctic

Equations

• Weighted.Arctic.instOrderBot = WOmegaContinuousNonUnitalSemiring.toOrderBot (WithBot ℕ∞)

instance Weighted.Arctic.instOmegaContinuousNonUnitalSemiring : OmegaContinuousNonUnitalSemiring Arctic

@[implicit_reducible]

instance Weighted.Arctic.instKStar : KStar Arctic

Equations

• Weighted.Arctic.instKStar = WKStar.toKStar (WithBot ℕ∞)

@[implicit_reducible]

instance Weighted.Arctic.instOfNatOfWithBotENat {n✝ : ℕ} [OfNat (WithBot ℕ∞) n✝] : OfNat Arctic n✝

Equations

• Weighted.Arctic.instOfNatOfWithBotENat = { ofNat := OfNat.ofNat n✝ }

@[implicit_reducible]

instance Weighted.Arctic.instPartialOrder : PartialOrder Arctic

Equations

• Weighted.Arctic.instPartialOrder = WPartialOrder.toPartialOrder (WithBot ℕ∞)

def Weighted.Boolean : Type

Equations

• Weighted.Boolean = Bool

@[implicit_reducible]

instance Weighted.instDecidableEqBoolean : DecidableEq Boolean

Equations

• Weighted.instDecidableEqBoolean = Weighted.instDecidableEqBoolean._aux_1

@[implicit_reducible]

instance Weighted.instTopBoolean : Top Boolean

Equations

• Weighted.instTopBoolean = { top := Weighted.instTopBoolean._aux_1 }

@[implicit_reducible]

def Weighted.Boolean.instWSemiringBool : WSemiring Bool

Equations

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

@[implicit_reducible]

def Weighted.Boolean.instWLEBool : WLE Bool

Equations

• Weighted.Boolean.instWLEBool = { wle := fun (x1 x2 : Bool) => x1 ≤ x2 }

@[implicit_reducible]

def Weighted.Boolean.instWPartialOrderBool : WPartialOrder Bool

Equations

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

@[implicit_reducible]

noncomputable def Weighted.Boolean.instWOmegaContinuousNonUnitalSemiringBool : WOmegaContinuousNonUnitalSemiring Bool

Equations

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

@[implicit_reducible]

def Weighted.Boolean.instWKStarBool : WKStar Bool

Equations

• Weighted.Boolean.instWKStarBool = { wkstar := fun (x : Bool) => ⊤ }

theorem Weighted.Boolean.instLawfulWKStarBool : LawfulWKStar Bool

@[implicit_reducible]

instance Weighted.Boolean.instOfNatOfBool {n✝ : ℕ} [OfNat Bool n✝] : OfNat Boolean n✝

Equations

• Weighted.Boolean.instOfNatOfBool = { ofNat := OfNat.ofNat n✝ }

instance Weighted.Boolean.instMulLeftMono : MulLeftMono Boolean

instance Weighted.Boolean.instMulRightMono : MulRightMono Boolean

@[implicit_reducible]

instance Weighted.Boolean.instPartialOrder : PartialOrder Boolean

Equations

• Weighted.Boolean.instPartialOrder = WPartialOrder.toPartialOrder Bool

@[implicit_reducible]

noncomputable instance Weighted.Boolean.instOrderBot : OrderBot Boolean

Equations

• Weighted.Boolean.instOrderBot = WOmegaContinuousNonUnitalSemiring.toOrderBot Bool

@[implicit_reducible]

instance Weighted.Boolean.instReprOfBool [Repr Bool] : Repr Boolean

Equations

• Weighted.Boolean.instReprOfBool = inst✝

@[implicit_reducible]

instance Weighted.Boolean.instKStar : KStar Boolean

Equations

• Weighted.Boolean.instKStar = WKStar.toKStar Bool

instance Weighted.Boolean.instOmegaContinuousNonUnitalSemiring : OmegaContinuousNonUnitalSemiring Boolean

@[implicit_reducible]

instance Weighted.Boolean.instSemiring : Semiring Boolean

Equations

• Weighted.Boolean.instSemiring = WSemiring.toSemiring Bool

@[implicit_reducible]

noncomputable instance Weighted.Boolean.instOmegaCompletePartialOrder : OmegaCompletePartialOrder Boolean

Equations

• Weighted.Boolean.instOmegaCompletePartialOrder = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder Bool

@[implicit_reducible]

instance Weighted.Boolean.instDecidableLE : DecidableLE Boolean

Equations

• Weighted.Boolean.instDecidableLE = WPartialOrder.toDecidableLE Bool

instance Weighted.Boolean.instIsPositiveOrderedAddMonoid : IsPositiveOrderedAddMonoid Boolean

instance Weighted.Boolean.instLawfulKStar : LawfulKStar Boolean

def Weighted.Bottleneck : Type

Equations

• Weighted.Bottleneck = WithBot ℕ∞

@[implicit_reducible]

instance Weighted.instDecidableEqBottleneck : DecidableEq Bottleneck

Equations

• Weighted.instDecidableEqBottleneck = Weighted.instDecidableEqBottleneck._aux_1

@[implicit_reducible]

instance Weighted.instTopBottleneck : Top Bottleneck

Equations

• Weighted.instTopBottleneck = { top := Weighted.instTopBottleneck._aux_1 }

def Weighted.Bottleneck.max (a b : WithBot ℕ∞) : WithBot ℕ∞

Equations

• Weighted.Bottleneck.max a b = if a ≤ b then b else a

@[simp]

theorem Weighted.Bottleneck.max_eq_sup (a b : WithBot ℕ∞) : max a b = Max.max a b

def Weighted.Bottleneck.min (a b : WithBot ℕ∞) : WithBot ℕ∞

Equations

• Weighted.Bottleneck.min a b = if a ≤ b then a else b

@[simp]

theorem Weighted.Bottleneck.min_eq_sup (a b : WithBot ℕ∞) : min a b = Min.min a b

@[implicit_reducible]

def Weighted.Bottleneck.instWSemiringWithBotENat : WSemiring (WithBot ℕ∞)

Equations

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

@[implicit_reducible]

def Weighted.Bottleneck.instWLEWithBotENat : WLE (WithBot ℕ∞)

Equations

• Weighted.Bottleneck.instWLEWithBotENat = { wle := fun (x1 x2 : WithBot ℕ∞) => x1 ≤ x2 }

@[implicit_reducible]

def Weighted.Bottleneck.instWPartialOrderWithBotENat : WPartialOrder (WithBot ℕ∞)

Equations

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

@[implicit_reducible]

noncomputable def Weighted.Bottleneck.instWOmegaContinuousNonUnitalSemiringWithBotENat : WOmegaContinuousNonUnitalSemiring (WithBot ℕ∞)

Equations

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

@[implicit_reducible]

def Weighted.Bottleneck.instWKStarWithBotENat : WKStar (WithBot ℕ∞)

Equations

• Weighted.Bottleneck.instWKStarWithBotENat = { wkstar := fun (x : WithBot ℕ∞) => ⊤ }

theorem Weighted.Bottleneck.instLawfulWKStarWithBotENat : LawfulWKStar (WithBot ℕ∞)

instance Weighted.Bottleneck.instMulLeftMono : MulLeftMono Bottleneck

instance Weighted.Bottleneck.instMulRightMono : MulRightMono Bottleneck

@[implicit_reducible]

instance Weighted.Bottleneck.instOfNatOfWithBotENat {n✝ : ℕ} [OfNat (WithBot ℕ∞) n✝] : OfNat Bottleneck n✝

Equations

• Weighted.Bottleneck.instOfNatOfWithBotENat = { ofNat := OfNat.ofNat n✝ }

@[implicit_reducible]

noncomputable instance Weighted.Bottleneck.instOmegaCompletePartialOrder : OmegaCompletePartialOrder Bottleneck

Equations

• Weighted.Bottleneck.instOmegaCompletePartialOrder = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder (WithBot ℕ∞)

@[implicit_reducible]

noncomputable instance Weighted.Bottleneck.instOrderBot : OrderBot Bottleneck

Equations

• Weighted.Bottleneck.instOrderBot = WOmegaContinuousNonUnitalSemiring.toOrderBot (WithBot ℕ∞)

@[implicit_reducible]

instance Weighted.Bottleneck.instPartialOrder : PartialOrder Bottleneck

Equations

• Weighted.Bottleneck.instPartialOrder = WPartialOrder.toPartialOrder (WithBot ℕ∞)

@[implicit_reducible]

instance Weighted.Bottleneck.instKStar : KStar Bottleneck

Equations

• Weighted.Bottleneck.instKStar = WKStar.toKStar (WithBot ℕ∞)

@[implicit_reducible]

instance Weighted.Bottleneck.instDecidableLE : DecidableLE Bottleneck

Equations

• Weighted.Bottleneck.instDecidableLE = WPartialOrder.toDecidableLE (WithBot ℕ∞)

instance Weighted.Bottleneck.instLawfulKStar : LawfulKStar Bottleneck

@[implicit_reducible]

instance Weighted.Bottleneck.instReprOfWithBotENat [Repr (WithBot ℕ∞)] : Repr Bottleneck

Equations

• Weighted.Bottleneck.instReprOfWithBotENat = inst✝

instance Weighted.Bottleneck.instOmegaContinuousNonUnitalSemiring : OmegaContinuousNonUnitalSemiring Bottleneck

@[implicit_reducible]

instance Weighted.Bottleneck.instSemiring : Semiring Bottleneck

Equations

• Weighted.Bottleneck.instSemiring = WSemiring.toSemiring (WithBot ℕ∞)

instance Weighted.Bottleneck.instIsPositiveOrderedAddMonoid : IsPositiveOrderedAddMonoid Bottleneck

def Weighted.ENNReal' : Type

Equations

• Weighted.ENNReal' = ENNReal

@[implicit_reducible]

instance Weighted.instTopENNReal' : Top ENNReal'

Equations

• Weighted.instTopENNReal' = { top := Weighted.instTopENNReal'._aux_1 }

@[implicit_reducible]

noncomputable def Weighted.ENNReal.instWSemiringENNReal : WSemiring ENNReal

Equations

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

@[implicit_reducible]

def Weighted.ENNReal.instWLEENNReal : WLE ENNReal

Equations

• Weighted.ENNReal.instWLEENNReal = { wle := fun (x1 x2 : ENNReal) => x1 ≤ x2 }

@[implicit_reducible]

noncomputable def Weighted.ENNReal.instWPartialOrderENNReal : WPartialOrder ENNReal

Equations

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

@[implicit_reducible]

noncomputable def Weighted.ENNReal.instWOmegaContinuousNonUnitalSemiringENNReal : WOmegaContinuousNonUnitalSemiring ENNReal

Equations

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

@[implicit_reducible]

noncomputable def Weighted.ENNReal.instWKStarENNReal : WKStar ENNReal

Equations

• Weighted.ENNReal.instWKStarENNReal = { wkstar := fun (r : ENNReal) => (1 - r)⁻¹ }

theorem Weighted.ENNReal.instLawfulWKStarENNReal : LawfulWKStar ENNReal

@[implicit_reducible]

instance Weighted.ENNReal.instOfNatENNReal'OfENNReal {n✝ : ℕ} [OfNat ENNReal n✝] : OfNat ENNReal' n✝

Equations

• Weighted.ENNReal.instOfNatENNReal'OfENNReal = { ofNat := OfNat.ofNat n✝ }

@[implicit_reducible]

noncomputable instance Weighted.ENNReal.instSemiringENNReal' : Semiring ENNReal'

Equations

• Weighted.ENNReal.instSemiringENNReal' = WSemiring.toSemiring ENNReal

instance Weighted.ENNReal.instIsPositiveOrderedAddMonoidENNReal' : IsPositiveOrderedAddMonoid ENNReal'

instance Weighted.ENNReal.instMulRightMonoENNReal' : MulRightMono ENNReal'

@[implicit_reducible]

noncomputable instance Weighted.ENNReal.instDecidableLEENNReal' : DecidableLE ENNReal'

Equations

• Weighted.ENNReal.instDecidableLEENNReal' = WPartialOrder.toDecidableLE ENNReal

instance Weighted.ENNReal.instLawfulKStarENNReal' : LawfulKStar ENNReal'

@[implicit_reducible]

instance Weighted.ENNReal.instReprENNReal'OfENNReal [Repr ENNReal] : Repr ENNReal'

Equations

• Weighted.ENNReal.instReprENNReal'OfENNReal = inst✝

@[implicit_reducible]

noncomputable instance Weighted.ENNReal.instOmegaCompletePartialOrderENNReal' : OmegaCompletePartialOrder ENNReal'

Equations

• Weighted.ENNReal.instOmegaCompletePartialOrderENNReal' = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder ENNReal

@[implicit_reducible]

noncomputable instance Weighted.ENNReal.instKStarENNReal' : KStar ENNReal'

Equations

• Weighted.ENNReal.instKStarENNReal' = WKStar.toKStar ENNReal

instance Weighted.ENNReal.instOmegaContinuousNonUnitalSemiringENNReal' : OmegaContinuousNonUnitalSemiring ENNReal'

@[implicit_reducible]

noncomputable instance Weighted.ENNReal.instOrderBotENNReal' : OrderBot ENNReal'

Equations

• Weighted.ENNReal.instOrderBotENNReal' = WOmegaContinuousNonUnitalSemiring.toOrderBot ENNReal

@[implicit_reducible]

noncomputable instance Weighted.ENNReal.instPartialOrderENNReal' : PartialOrder ENNReal'

Equations

• Weighted.ENNReal.instPartialOrderENNReal' = WPartialOrder.toPartialOrder ENNReal

instance Weighted.ENNReal.instMulLeftMonoENNReal' : MulLeftMono ENNReal'

@[reducible, inline]

abbrev Weighted.Viterbi.PReal : Submonoid ENNReal

Equations

• Weighted.Viterbi.PReal = { carrier := {r : ENNReal | r ≤ 1}, mul_mem' := @Weighted.Viterbi.PReal._proof_2, one_mem' := Weighted.Viterbi.PReal._proof_3 }

def Weighted.Viterbi : Type

Equations

• Weighted.Viterbi = ↥Weighted.Viterbi.PReal

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instMulZeroClassSubtypeENNRealMemSubmonoidPReal : MulZeroClass ↥PReal

Equations

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

@[simp]

theorem Weighted.Viterbi.PReal.zero_le {p : ↥PReal} : 0 ≤ p

@[simp]

theorem Weighted.Viterbi.PReal.zero_le_coe {p : ↥PReal} : 0 ≤ ↑p

@[simp]

theorem Weighted.Viterbi.PReal.one_le {p : ↥PReal} : p ≤ 1

@[simp]

theorem Weighted.Viterbi.PReal.one_le_coe {p : ↥PReal} : ↑p ≤ 1

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instCompleteLatticeSubtypeENNRealMemSubmonoidPReal : CompleteLattice ↥PReal

Equations

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

@[implicit_reducible]

noncomputable def Weighted.Viterbi.instWSemiringSubtypeENNRealMemSubmonoidPReal : WSemiring ↥PReal

Equations

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

@[implicit_reducible]

def Weighted.Viterbi.instWLESubtypeENNRealMemSubmonoidPReal : WLE ↥PReal

Equations

• Weighted.Viterbi.instWLESubtypeENNRealMemSubmonoidPReal = { wle := fun (x1 x2 : ↥Weighted.Viterbi.PReal) => x1 ≤ x2 }

@[implicit_reducible]

noncomputable def Weighted.Viterbi.instWPartialOrderSubtypeENNRealMemSubmonoidPReal : WPartialOrder ↥PReal

Equations

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

@[simp]

theorem Weighted.Viterbi.PReal.iSup_val {f : ℕ → ↥PReal} : ↑(⨆ (i : ℕ), f i) = ⨆ (i : ℕ), ↑(f i)

@[implicit_reducible]

noncomputable def Weighted.Viterbi.instWOmegaContinuousNonUnitalSemiringSubtypeENNRealMemSubmonoidPReal : WOmegaContinuousNonUnitalSemiring ↥PReal

Equations

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

@[implicit_reducible]

noncomputable def Weighted.Viterbi.instWKStarSubtypeENNRealMemSubmonoidPReal : WKStar ↥PReal

Equations

• Weighted.Viterbi.instWKStarSubtypeENNRealMemSubmonoidPReal = { wkstar := fun (x : ↥Weighted.Viterbi.PReal) => 1 }

theorem Weighted.Viterbi.instLawfulWKStarSubtypeENNRealMemSubmonoidPReal : LawfulWKStar ↥PReal

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instSemiring : Semiring Viterbi

Equations

• Weighted.Viterbi.instSemiring = WSemiring.toSemiring ↥Weighted.Viterbi.PReal

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instKStar : KStar Viterbi

Equations

• Weighted.Viterbi.instKStar = WKStar.toKStar ↥Weighted.Viterbi.PReal

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instOrderBot : OrderBot Viterbi

Equations

• Weighted.Viterbi.instOrderBot = WOmegaContinuousNonUnitalSemiring.toOrderBot ↥Weighted.Viterbi.PReal

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instOmegaCompletePartialOrder : OmegaCompletePartialOrder Viterbi

Equations

• Weighted.Viterbi.instOmegaCompletePartialOrder = WOmegaCompletePartialOrder.toOmegaCompletePartialOrder ↥Weighted.Viterbi.PReal

instance Weighted.Viterbi.instMulLeftMono : MulLeftMono Viterbi

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instDecidableLE : DecidableLE Viterbi

Equations

• Weighted.Viterbi.instDecidableLE = WPartialOrder.toDecidableLE ↥Weighted.Viterbi.PReal

instance Weighted.Viterbi.instOmegaContinuousNonUnitalSemiring : OmegaContinuousNonUnitalSemiring Viterbi

instance Weighted.Viterbi.instLawfulKStar : LawfulKStar Viterbi

instance Weighted.Viterbi.instIsPositiveOrderedAddMonoid : IsPositiveOrderedAddMonoid Viterbi

instance Weighted.Viterbi.instMulRightMono : MulRightMono Viterbi

@[implicit_reducible]

noncomputable instance Weighted.Viterbi.instPartialOrder : PartialOrder Viterbi

Equations

• Weighted.Viterbi.instPartialOrder = WPartialOrder.toPartialOrder ↥Weighted.Viterbi.PReal

@[implicit_reducible]

instance Weighted.Viterbi.instOfNatOfSubtypeENNRealMemSubmonoidPReal {n✝ : ℕ} [OfNat (↥PReal) n✝] : OfNat Viterbi n✝

Equations

• Weighted.Viterbi.instOfNatOfSubtypeENNRealMemSubmonoidPReal = { ofNat := OfNat.ofNat n✝ }

@[implicit_reducible]

instance Weighted.Viterbi.instReprOfSubtypeENNRealMemSubmonoidPReal [Repr ↥PReal] : Repr Viterbi

Equations

• Weighted.Viterbi.instReprOfSubtypeENNRealMemSubmonoidPReal = inst✝