Email Gateway (Aug 22 2022 at 16:38): Email Gateway (Aug 22 2022 at 16:38):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Hi,
This may be trivial but I have a difficulty proving the following lemma:
lemma
fixes A :: "real^3^3"
and x::"real^3"
assumes "A>0"
shows " (A *v x) - (mat 1 *v x) = (A - mat 1) *v x "
where A is a positive definite diagonal matrix. Is there a lemma predefined
related to this?
Cheers
Omar
Email Gateway (Aug 22 2022 at 16:39):From: Fabian Immler <immler@in.tum.de>
Dear Omar,
Unfortunately, there are no lemmas on distributivity of *v in the distribution.
Some are currently in the AFP-entry Perron_Frobenius:
https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
You can prove them (in HOL-Analysis) as follows:
lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: ring_1 ^ 'n)"
unfolding matrix_vector_mult_def
by vector (simp add: sum_subtractf left_diff_distrib)
lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
unfolding matrix_vector_mult_def
by vector (simp add: sum.distrib distrib_right)
lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
unfolding matrix_vector_mult_def
by vector (simp add: sum.distrib distrib_left)
lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v (v - w) = M *v v - M *v w"
unfolding matrix_vector_mult_def
by vector (simp add: sum_subtractf right_diff_distrib)
Those should probably be included in the next Isabelle release.
Hope this helps,
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 16:39):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Dear Fabian,
That's obvious now. I thought I couldn't find them. Many thanks for sending
these through. I also realized that I previously proved one of them as
below:
lemma mat_vec_add_dis: "A *v g + B *v g = (A + B) *v g"
apply (vector matrix_vector_mult_def)
apply (smt Cartesian_Euclidean_Space.sum_cong_aux distrib_right
sum.distrib)
done
Thanks
Omar
Email Gateway (Aug 22 2022 at 16:39):From: Lawrence Paulson <lp15@cam.ac.uk>
I have recently been adding some results involving matrices to the repository and they will be available in the next release.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:39):From: Omar Jasim <oajasim1@sheffield.ac.uk>
I believe also this lemma doesn't exist:
lemma
fixes y :: "real^3"
and X :: "real^3^3"
shows "norm(X *v y) ≤ norm (X) * norm (y)"
Omar Jasim
PhD Student
Automatic Control and Systems Engineering - ACSE
University of Sheffield
UK
Last updated: Apr 23 2024 at 16:19 UTC