Re: [isabelle] Vector transpose
- To: Omar Jasim <oajasim1 at sheffield.ac.uk>
- Subject: Re: [isabelle] Vector transpose
- From: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
- Date: Tue, 27 Feb 2018 10:56:42 +0000
- Accept-language: de-DE, de-AT, en-US
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com>
- References: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com>
- Thread-index: AQHTr7jbFnBBfJTrD0CU5Wq0JZLZ6KO4AxcA
- Thread-topic: [isabelle] Vector transpose
if you’re not working with “real^’a” but with “real mat” from AFP/Jordan_Normal_Form/Matrix,
then you find “transpose_mat”. However, there “norm” is not defined.
However, using AFP/Perron_Frobenius/HMA_Connect you might easily be able to define transpose for “real^’a”
and then reuse the results for transpose_mat via the transfer-package.
For instance, eigen_vectors for “real^’a^’a” are defined like this, and results are just transferred.
> I was looking for a transpose of a vector (real^'a) but I couldn't find it.
> Probably there is no such definition. The problem I faced is:
> fixes E :: "(real, 6) vec"
> and Q :: "((real, 6) vec, 6) vec"
> and B:: "((real, 3) vec, 6) vec"
> shows "norm((E v* Q) v* B) = norm(transpose (B) *v (Q*v E))"
> So please, is there a transpose of a vector defined in Isabelle/HOL?
This archive was generated by a fusion of
Pipermail (Mailman edition) and