Craig Alan Feinstein (Jul 25 2024 at 02:00): Craig Alan Feinstein (Jul 25 2024 at 02:00):@Chelsea Edmonds A question that came up now is in the odd v part of the BRC theorem. I'm trying to use an equation that you got from Stinson's book to prove a single algebraic equation:
context ordered_regular_pairwise_balance
begin
lemma brc_equation:
assumes "x mat v 1"
shows "l2_norm (mat_mult N x) = ฮ * (vector_sum x)^2 + (๐ - ฮ) * l2_norm x"
proof -
have "N * (NโงT) = ฮ โ
โฉm (Jโฉm ๐) + (๐ - ฮ) โ
โฉm (1โฉm ๐)" using
rpbd_incidence_matrix_cond by simp
then have "(N * (NโงT)) * x = (ฮ โ
โฉm (Jโฉm ๐) + (๐ - ฮ) โ
โฉm (1โฉm ๐)) * x"
by simp```
The "then have" part is giving me trouble. I probably am not using a good definition of the vector x. It's giving me " incompatible operand type" error. Any ideas as to how to fix this? I want x to be a rational vector, as the proof will use this fact to find an integer solution to an equation later on.
Craig Alan Feinstein said:
Chelsea Edmonds A question that came up now is in the odd v part of the BRC theorem. I'm trying to use an equation that you got from Stinson's book to prove a single algebraic equation:
context ordered_regular_pairwise_balance begin lemma brc_equation: assumes "x mat v 1" shows "l2_norm (mat_mult N x) = ฮ * (vector_sum x)^2 + (๐ - ฮ) * l2_norm x" proof - have "N * (NโงT) = ฮ โ โฉm (Jโฉm ๐) + (๐ - ฮ) โ โฉm (1โฉm ๐)" using rpbd_incidence_matrix_cond by simp then have "(N * (NโงT)) * x = (ฮ โ โฉm (Jโฉm ๐) + (๐ - ฮ) โ โฉm (1โฉm ๐)) * x" by simpThe "then have" part is giving me trouble. I probably am not using a good definition of the vector x. It's giving me " incompatible operand type" error. Any ideas as to how to fix this? I want x to be a rational vector, as the proof will use this fact to find an integer solution to an equation later on.
When you get this kind of error, the trick is to always to look at what the detail of the error is where it details the type its expecting vs what it got. When I copy this into Isabelle, on my end I'm getting a pretty complex function type for x. Which it must be inferring from your assumptions or theorem statement - so look back at how it is used in those and what types the functions/definitions you already used are expecting. Your assumption looks like it is likely the problem here - is it supposed to be x = <some 1-d matrix/vector>?
Also, are l2_norm, mat_mult and vector_sum all definitions you've defined? mat_mult in particular I'd expect to have a built in equivalent in the JNF matrix library already, which you should use if so to benefit from all the exisitng lemmas. If x is also supposed to be a vector - the mult_mat_vec definition may do what you want to do and that way you can declare x as a vector to start with.
Last thing, holding Cntr and hovering over variables in Isabelle is good way to check their type (and if they are defined). For example, ๐ is not defined in an ordered_regular_pairwise_balance context (as it places no restructions on uniform block size), so it comes up as a 'free variable'. Is this supposed to be in a bibd context instead? If so use the ordered_bibd context. You may need to add in the following declaration to establish inheritance (I suspect I missed this one in the original), so you get the Stinson theorem you referred to.
sublocale ordered_bibd โ ordered_regular_pairwise_balance ๐ฑs โฌs ฮ ๐
by unfold_locales
@Chelsea Edmonds that particular lemma that I was and still am working on uses the JNF library, as you had thought. l2_norm, mat_mult, and vector_sum are all in there. I had forgotten where I had gotten them when I wrote yesterday. When I used them for the next line, it worked. However, the next line didn't work. I'm not sure why. There's got to be a better way than this clunky language:
assumes "x rat mat v 1"
shows "l2_norm (mat_mult N x) = \<Lambda> * (vector_sum x)^2 + (\<r> - \<Lambda>) * l2_norm x"
proof -
have "N * (N\<^sup>T) = \<Lambda> \<cdot>\<^sub>m (J\<^sub>m \<v>) + (\<r> - \<Lambda>) \<cdot>\<^sub>m (1\<^sub>m \<v>)" using
rpbd_incidence_matrix_cond by simp
then have "mat_mult (N * (N\<^sup>T)) x =
mat_mult (\<Lambda> \<cdot>\<^sub>m (J\<^sub>m \<v>) + (\<r> - \<Lambda>) \<cdot>\<^sub>m (1\<^sub>m \<v>)) x" by simp
then have "mat_mult (transpose_mat x) (mat_mult (N * (N\<^sup>T)) x) =
mat_mult (transpose_mat x) (mat_mult (\<Lambda> \<cdot>\<^sub>m (J\<^sub>m \<v>) + (\<r> - \<Lambda>) \<cdot>\<^sub>m (1\<^sub>m \<v>)) x)"
by simp?
@Chelsea Edmonds I had realized before you wrote here that there was a problem with the fact that Stinson's theorem comes under a different locale than ordered_sym_bibd and knew I would need to fix this problem somehow; otherwise, I would have no way to prove the theorem using your work. I just tried your way that you gave me above using the sublocale, but Isabelle didn't accept it. I'll email you everything I have so far and you can tell me what you had in mind.
Also, the Bruck Ryser Theorem proof for even v doesn't hold for nonsymmetric BIBDs because the determinant of N is used in the proof and N must be square. However, I haven't found a reason why it has to be a symmetric BIBD for odd v. Maybe I missed the reason. In any case, I'm going to assume symmetric BIBD to make things easy for now.
Chelsea Edmonds (Jul 26 2024 at 09:52):Craig Alan Feinstein said:
Chelsea Edmonds that particular lemma that I was and still am working on uses the JNF library, as you had thought. l2_norm, mat_mult, and vector_sum are all in there. I had forgotten where I had gotten them when I wrote yesterday. When I used them for the next line, it worked. However, the next line didn't work. I'm not sure why. There's got to be a better way than this clunky language:
assumes "x rat mat v 1" shows "l2_norm (mat_mult N x) = \<Lambda> * (vector_sum x)^2 + (\<r> - \<Lambda>) * l2_norm x" proof - have "N * (N\<^sup>T) = \<Lambda> \<cdot>\<^sub>m (J\<^sub>m \<v>) + (\<r> - \<Lambda>) \<cdot>\<^sub>m (1\<^sub>m \<v>)" using rpbd_incidence_matrix_cond by simp then have "mat_mult (N * (N\<^sup>T)) x = mat_mult (\<Lambda> \<cdot>\<^sub>m (J\<^sub>m \<v>) + (\<r> - \<Lambda>) \<cdot>\<^sub>m (1\<^sub>m \<v>)) x" by simp then have "mat_mult (transpose_mat x) (mat_mult (N * (N\<^sup>T)) x) = mat_mult (transpose_mat x) (mat_mult (\<Lambda> \<cdot>\<^sub>m (J\<^sub>m \<v>) + (\<r> - \<Lambda>) \<cdot>\<^sub>m (1\<^sub>m \<v>)) x)" by simp? ```` For me, these definitions are all coming up as blue text, which means they aren't recognised. So I suspect you may have gotten them from somewhere else? The JNF library defines times_mat (which you can use the * notation for), mult_mat_vec, and smult_mat. I believe mult_mat was from the built in analysis matrix library. I can't find l2_norm defined anywhere, including using the FindFacts search tool (https://search.isabelle.in.tum.de/#). Similarly, vector_sum isn't defined. Did you mean sum_vec? Basically, watch out for any blue text in proofs - this typically means Isabelle is treating it as a free variable which may still parse something correctly but is often not want you want!
Chelsea Edmonds (Jul 26 2024 at 09:53):Craig Alan Feinstein said:
Chelsea Edmonds I had realized before you wrote here that there was a problem with the fact that Stinson's theorem comes under a different locale than ordered_sym_bibd and knew I would need to fix this problem somehow; otherwise, I would have no way to prove the theorem using your work. I just tried your way that you gave me above using the sublocale, but Isabelle didn't accept it. I'll email you everything I have so far and you can tell me what you had in mind.
Also, the Bruck Ryser Theorem proof for even v doesn't hold for nonsymmetric BIBDs because the determinant of N is used in the proof and N must be square. However, I haven't found a reason why it has to be a symmetric BIBD for odd v. Maybe I missed the reason. In any case, I'm going to assume symmetric BIBD to make things easy for now.
I'll take a quick look, it'll definitely be possible.
Last updated: Dec 21 2024 at 12:33 UTC