def Viterbi : Type

Viterbi semiring (max-times) over probabilities in [0,1].

Equations

• Viterbi = { p : NNReal // p ≤ 1 }

instance Viterbi.instCoeNNReal : Coe Viterbi NNReal

Equations

• Viterbi.instCoeNNReal = { coe := Subtype.val }

theorem Viterbi.ext {a b : Viterbi} (h : ↑a = ↑b) : a = b

theorem Viterbi.ext_iff {a b : Viterbi} : a = b ↔ ↑a = ↑b

@[simp]

theorem Viterbi.coe_mk (p : NNReal) (hp : p ≤ 1) : ↑⟨p, hp⟩ = p

instance Viterbi.instZero : Zero Viterbi

Equations

• Viterbi.instZero = { zero := ⟨0, Viterbi.instZero._proof_1⟩ }

instance Viterbi.instOne : One Viterbi

Equations

• Viterbi.instOne = { one := ⟨1, Viterbi.instOne._proof_1⟩ }

instance Viterbi.instAdd : Add Viterbi

Equations

• Viterbi.instAdd = { add := fun (a b : Viterbi) => ⟨max ↑a ↑b, ⋯⟩ }

instance Viterbi.instMul : Mul Viterbi

Equations

• Viterbi.instMul = { mul := fun (a b : Viterbi) => ⟨↑a * ↑b, ⋯⟩ }

@[simp]

theorem Viterbi.zero_def : ↑0 = 0

@[simp]

theorem Viterbi.one_def : ↑1 = 1

@[simp]

theorem Viterbi.add_def (a b : Viterbi) : ↑(a + b) = max ↑a ↑b

@[simp]

theorem Viterbi.mul_def (a b : Viterbi) : ↑(a * b) = ↑a * ↑b

instance Viterbi.instCommSemiring : CommSemiring Viterbi

Equations

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

theorem Viterbi.viterbi_order_le (a b : Viterbi) : ↑a ≤ ↑b ↔ a + b = b

instance Viterbi.instPartialOrder : PartialOrder Viterbi

Equations

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

@[simp]

theorem Viterbi.le_def (a b : Viterbi) : a ≤ b ↔ ↑a ≤ ↑b

noncomputable instance Viterbi.instSemiringWithMonus : SemiringWithMonus Viterbi

Equations

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

theorem Viterbi.absorptive : _root_.absorptive Viterbi

theorem Viterbi.idempotent : _root_.idempotent Viterbi

theorem Viterbi.mul_sub_left_distributive : _root_.mul_sub_left_distributive Viterbi