class LawfulKStar (α : Type u_1) [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] : Prop

• kstar_eq_sum (m : α) : KStar.kstar m = ω∑ (n : ℕ), m ^ n

class KStarIter (α : Type u_1) [One α] [Mul α] [Add α] [KStar α] : Prop

• kstar_iter (m : α) : 1 + m * KStar.kstar m = KStar.kstar m

@[implicit_reducible]

instance KStar.instUnitStar {α : Type u_1} [KStar α] : KStar (Matrix Unit Unit α)

Equations

• KStar.instUnitStar = { kstar := fun (m : Matrix Unit Unit α) (α_1 β : Unit) => KStar.kstar (m α_1 β) }

theorem KStar.ωSup_pow {α : Type u_2} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [MulLeftMono α] [MulRightMono α] [IsPositiveOrderedAddMonoid α] [OmegaContinuousNonUnitalSemiring α] (f : ℕ → α) (hf : Monotone f) (i : ℕ) : OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => f n ^ i, monotone' := ⋯ } = OmegaCompletePartialOrder.ωSup { toFun := fun (n : ℕ) => f n, monotone' := hf } ^ i

theorem KStar.kstar_iter {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a : α} : 1 + a * KStar.kstar a = KStar.kstar a

(A.10)

instance KStar.instKStarIter {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] : KStarIter α

theorem KStar.kstar_iter' {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a : α} : 1 + KStar.kstar a * a = KStar.kstar a

(A.11)

theorem KStar.idk_left {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] {a c : α} (h : 1 + a * c ≤ c) : KStar.kstar a ≤ c

theorem KStar.idk_right {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulRightMono α] {a c : α} (h : 1 + c * a ≤ c) : KStar.kstar a ≤ c

theorem KStar.A12 {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a b c : α} (h : b + a * c ≤ c) : KStar.kstar a * b ≤ c

(A.12)

theorem KStar.A13 {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a b c : α} (h : b + c * a ≤ c) : b * KStar.kstar a ≤ c

(A.13)

theorem KStar.mul_kstar_le_kstar {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a : α} : a * KStar.kstar a ≤ KStar.kstar a

theorem KStar.kstar_le_kstar {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] {a b : α} (h : a ≤ b) : KStar.kstar a ≤ KStar.kstar b

theorem KStar.mul_kstar {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a b : α} : KStar.kstar (a * b) = 1 + a * KStar.kstar (b * a) * b

theorem KStar.least_q {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {a b : α} : IsLeast {x : α | b + a * x = x} (KStar.kstar a * b)