Certificate construction for Hessenberg similarity

mkHessenbergSimilarity constructs a Hessenberg.Similarity certificate and corresponding Hessenberg reduction from a literal matrix over ℚ (or more generally a ring S with f : S → ℚ).

Main definitions

• mkHessenbergSimilarity: produce and elaborate the Hessenberg similarity certificate of a matrix literal.
• SimilarityResult: the Hessenberg.Similarity certificate together with the reduction data.

Implementation notes

The untrusted computation reduce (in Mathlib.Tactic.Hessenberg.Reduce) produces L a unit lower triangular matrix, σ a permutation corresponding to the row and column swaps, and H an upper Hessenberg matrix.

The mkHessenbergSimilarity function certifies Aσ * L = L * H (where Aσ is the reindexing of A.map f by σ) via the products Aσ * L = P and L * H = P, each proved by certifyProductEq on the lists of rows.

The conditions that L is lower triangular with nonzero diagonal and H is upper Hessenberg are decided by the kernel.

structure Mathlib.Tactic.Hessenberg.SimilarityResult {n : ℕ} (A : Q(Matrix (Fin «$n») (Fin «$n») ℚ)) : Type

The result of producing a Hessenberg similarity of A.

• cert : Q(Matrix.Hessenberg.Similarity «$A»)

  The elaborated Matrix.Hessenberg.Similarity certificate term.

• Harr : Q(Array ℚ)

  The literal of the row-major array of the Hessenberg matrix of the certificate.

• toArray_eq : Q(unknown_1.H.toArray = unknown_2)

  The proof that Harr is the array of the Hessenberg matrix of the certificate.

• red : Reduction

  The reduction data underlying the certificate.

def Mathlib.Tactic.Hessenberg.mkHessenbergSimilarity {u : Lean.Level} {S : Q(Type u)} (f : Q(«$S» → ℚ)) (n : ℕ) (A : Q(Matrix (Fin «$n») (Fin «$n») «$S»)) (entries : Array (Array Q(«$S»))) (evalEntry : Q(«$S») → Lean.MetaM ℚ) : Lean.MetaM (SimilarityResult q(«$A».map «$f»))

Produce the Matrix.Hessenberg.Similarity certificate and corresponding reduction of A.map f for the n × n matrix literal A over S and the map f : S → ℚ, from the parsed entries entries of A, where evalEntry evaluates the image under f of an entry.

Equations

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