@[implicit_reducible]

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

Equations

• Matrix.KStar.instKStarUnit_weightedNetKAT_1 = { kstar := fun (m : Matrix Unit Unit α) => KStar.kstar ↑(m () ()) }

instance Matrix.KStar.instLawfulKStarUnit_1 {α : Type u_2} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] : LawfulKStar (Matrix Unit Unit α)

@[implicit_reducible]

instance Matrix.KStar.instHMulNMatrix {α : Type u_1} [Mul α] {m n : ℕ} : HMul α (NMatrix m n α) (NMatrix m n α)

Equations

• Matrix.KStar.instHMulNMatrix = { hMul := fun (s : α) (M : NMatrix m n α) => M.map fun (x : α) => s * x }

@[implicit_reducible]

instance Matrix.KStar.instHMulNMatrix_1 {α : Type u_1} [Mul α] {m n : ℕ} : HMul (NMatrix m n α) α (NMatrix m n α)

Equations

• Matrix.KStar.instHMulNMatrix_1 = { hMul := fun (M : NMatrix m n α) (s : α) => M.map fun (x : α) => x * s }

@[implicit_reducible]

instance Matrix.KStar.instKStarNMatrixOfNatNat {α : Type u_1} [KStar α] : KStar (NMatrix 1 1 α)

Equations

• Matrix.KStar.instKStarNMatrixOfNatNat = { kstar := fun (a : NMatrix 1 1 α) => NMatrix.fill (KStar.kstar (a 0 0)) }

instance Matrix.KStar.instKStarIterNMatrixOfNatNat {α : Type u_2} [Semiring α] [KStar α] [KStarIter α] : KStarIter (NMatrix 1 1 α)

def Matrix.KStar.kstar_fin' {α : Type u_1} [AddCommMonoid α] [Mul α] [KStar α] {n : ℕ} (m : NMatrix n n α) : NMatrix n n α

Equations

• One or more equations did not get rendered due to their size.
• Matrix.KStar.kstar_fin' m_2 = NMatrix.ofFn fun (a b : Fin 0) => ⋯.elim

def Nat.isPowerOfTwo_iff {n : ℕ} : n.isPowerOfTwo ↔ ∃ (m : ℕ), n = 2 ^ m

Equations

• ⋯ = ⋯

def Nat.powTwoRec {motive : ℕ → Sort u_2} (base : motive 1) (induct : (i : ℕ) → motive (2 ^ i) → motive (2 ^ i + 2 ^ i)) (n : ℕ) : motive (2 ^ n)

Equations

• Nat.powTwoRec base induct n = Nat.recAux base (fun (n : ℕ) (ih : motive (2 ^ n)) => have this := ⋯; ⋯.mpr (induct n ih)) n

def Nat.powTwoRec' {motive : ℕ → Sort u_2} (base : motive 1) (induct : (i : ℕ) → motive (2 ^ i) → motive (2 ^ i + 2 ^ i)) (n : ℕ) (hn : n.isPowerOfTwo) : motive n

Equations

• Nat.powTwoRec' base induct n hn = ⋯.mp (Nat.powTwoRec base induct n.log2)

def Matrix.KStar.kstarFin₂ {α : Type u_1} [AddCommMonoid α] [Mul α] [KStar α] {n : ℕ} (h : n.isPowerOfTwo) : NMatrix n n α → NMatrix n n α

Equations

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

def Matrix.KStar.kstarFin {α : Type u_1} [AddCommMonoid α] [Mul α] [KStar α] {n : ℕ} (M : NMatrix n n α) : NMatrix n n α

A more efficient version of kstar_fin' that splits the matrix up into four approximately equal blocks.

Equations

• Matrix.KStar.kstarFin M = if hn : n.isPowerOfTwo then Matrix.KStar.kstarFin₂ hn M else sorry

theorem Matrix.KStar.kstar_fin'_eq_kstarFin : @kstar_fin' = @kstarFin

@[implicit_reducible]

instance Matrix.KStar.instKStarNMatrixOfAddCommMonoidOfMul {α : Type u_1} {n : ℕ} [AddCommMonoid α] [Mul α] [KStar α] : KStar (NMatrix n n α)

Equations

• Matrix.KStar.instKStarNMatrixOfAddCommMonoidOfMul = { kstar := Matrix.KStar.kstar_fin' }

@[implicit_reducible]

instance Matrix.KStar.instKStarEMatrixOfAddCommMonoidOfMul {α : Type u_1} {n : Type u_2} [Listed n] [AddCommMonoid α] [Mul α] [KStar α] : KStar (EMatrix n n α)

Equations

• Matrix.KStar.instKStarEMatrixOfAddCommMonoidOfMul = { kstar := Matrix.KStar.instKStarEMatrixOfAddCommMonoidOfMul._aux_1 }

def Matrix.KStar.kstar_fin {α : Type u_1} [AddCommMonoid α] [Mul α] [KStar α] {n : ℕ} (m : Matrix (Fin n) (Fin n) α) : Matrix (Fin n) (Fin n) α

Equations

• Matrix.KStar.kstar_fin m = NMatrix.asMatrix (Matrix.KStar.kstar_fin' (NMatrix.ofMatrix m))

theorem Matrix.KStar.kstar_fin'_iter {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] {n : ℕ} (M : NMatrix n n α) : 1 + M * KStar.kstar M = KStar.kstar M

theorem Matrix.KStar.kstarFin_iter_pow_two {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] {n : ℕ} (M : NMatrix (2 ^ n) (2 ^ n) α) : 1 + M * kstarFin M = kstarFin M

theorem Matrix.KStar.kstarFin_iter {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] {n : ℕ} (M : NMatrix n n α) : 1 + M * kstarFin M = kstarFin M

instance Matrix.KStar.instKStarIterNMatrixOfLawfulKStar {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [LawfulKStar α] {n : ℕ} : KStarIter (NMatrix n n α)

instance Matrix.KStar.instMulLeftMonoNMatrixOfIsPositiveOrderedAddMonoid {α : Type u_1} [OmegaCompletePartialOrder α] [OrderBot α] [Mul α] [AddCommMonoid α] [IsPositiveOrderedAddMonoid α] [MulLeftMono α] {n : ℕ} : MulLeftMono (NMatrix n n α)

instance Matrix.KStar.instMulRightMonoNMatrixOfIsPositiveOrderedAddMonoid {α : Type u_1} [OmegaCompletePartialOrder α] [OrderBot α] [Mul α] [AddCommMonoid α] [IsPositiveOrderedAddMonoid α] [MulRightMono α] {n : ℕ} : MulRightMono (NMatrix n n α)

theorem Matrix.KStar.ωSup_apply {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [MulLeftMono α] [MulRightMono α] [IsPositiveOrderedAddMonoid α] [OmegaContinuousNonUnitalSemiring α] {n : ℕ} (x j : Fin n) (c : OmegaCompletePartialOrder.Chain (NMatrix n n α)) : (OmegaCompletePartialOrder.ωSup c) x j = OmegaCompletePartialOrder.ωSup (c.map { toFun := fun (n_1 : NMatrix n n α) => n_1 x j, monotone' := ⋯ })

instance Matrix.KStar.instOmegaContinuousNonUnitalSemiringNMatrix {α : Type u_1} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [MulLeftMono α] [MulRightMono α] [IsPositiveOrderedAddMonoid α] [OmegaContinuousNonUnitalSemiring α] {n : ℕ} : OmegaContinuousNonUnitalSemiring (NMatrix n n α)

axiom Matrix.KStar.axiomNMatrixStarLeωSum {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {n : ℕ} (m : NMatrix n n α) : KStar.kstar m ≤ ω∑ (n_1 : ℕ), m ^ n_1

instance Matrix.KStar.instLawfulKStarNMatrixOfKStarIterOfOmegaContinuousNonUnitalSemiring {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {n : ℕ} : LawfulKStar (NMatrix n n α)

instance Matrix.KStar.instLawfulKStarEMatrix {α : Type u_1} [Semiring α] [KStar α] [KStarIter α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] {n : Type u_2} [Listed n] : LawfulKStar (EMatrix n n α)