2 ms·

Just read your original opening statement. I think what everyone is telling you is that you were being unnecessarily hyperbolic towards an author that writes fo

Just read your original opening statement. I think what everyone is telling you is that you were being unnecessarily hyperbolic towards an author that writes for a mathematical argument. If it offends you so much as you've indicated that you just "moved on," then so be it.

auggierose 7y ago
I still stand by my opening statement. Now, after the discussion here I understand what the theorem statement is saying. That's a lot of work I had to do to understand the theorem statement, and it would have been unnecessary, had the theorem been stated "syntactically" correctly. Now why wasn't the theorem stated syntactically correct? If we had to state it in a mechanised theorem prover like Isabelle then we would extract the definition of the eigenvalues from the statement into a separate definition, like: For a hermitian n x n matrix H, let lambda_1(A), ..., lambda_n(A) be the eigenvalues of H. But of course, here we assume an order of the eigenvalues, and we don't really want that, because it is immaterial to what follows. So we rather have to write it like that: Definition: For a matrix H, let L(H) be the set of its eigenvalues. Theorem: If H is a n x n Hermitian matrix, then |L(H)| = n. But, of course, this is not true, as |L(H)| < n is a possibility. So you would have to account for that somehow as well in your definition / notation. So it is probably better to go back instead again, and explain the notation as follows: Notation: For a Hermitian n x n matrix H, let lambda_1(H), ..., lambda_n(H) be its eigenvalues (in an arbitrary order). Theorem: What Tao said. The notation could still not be written in Isabelle like that, but at least it has proper scoping now.
auggierose 7y ago
And I am pretty sure that every single downvote I get for this discussion here is from somebody who doesn't properly understand the theorem statement.
- tomrod 7y ago
  Point of feedback: this assumption does not hold.
  - auggierose 7y ago
    Some people also just downvote because they don't like something, although it is right.
    - tomrod 7y ago
      True, but this isn't what you asserted.
      - auggierose 7y ago
        Nope, it wasn't, thus my amendment.
        tomrod 7y ago
        Without objection. Cheers.

auggierose 7y ago

I still stand by my opening statement. Now, after the discussion here I understand what the theorem statement is saying. That's a lot of work I had to do to understand the theorem statement, and it would have been unnecessary, had the theorem been stated "syntactically" correctly. Now why wasn't the theorem stated syntactically correct? If we had to state it in a mechanised theorem prover like Isabelle then we would extract the definition of the eigenvalues from the statement into a separate definition, like: For a hermitian n x n matrix H, let lambda_1(A), ..., lambda_n(A) be the eigenvalues of H. But of course, here we assume an order of the eigenvalues, and we don't really want that, because it is immaterial to what follows. So we rather have to write it like that: Definition: For a matrix H, let L(H) be the set of its eigenvalues. Theorem: If H is a n x n Hermitian matrix, then |L(H)| = n. But, of course, this is not true, as |L(H)| < n is a possibility. So you would have to account for that somehow as well in your definition / notation. So it is probably better to go back instead again, and explain the notation as follows: Notation: For a Hermitian n x n matrix H, let lambda_1(H), ..., lambda_n(H) be its eigenvalues (in an arbitrary order). Theorem: What Tao said. The notation could still not be written in Isabelle like that, but at least it has proper scoping now.

auggierose 7y ago

And I am pretty sure that every single downvote I get for this discussion here is from somebody who doesn't properly understand the theorem statement.

tomrod 7y ago
Point of feedback: this assumption does not hold.
- auggierose 7y ago
  Some people also just downvote because they don't like something, although it is right.
  - tomrod 7y ago
    True, but this isn't what you asserted.
    - auggierose 7y ago
      Nope, it wasn't, thus my amendment.
      - tomrod 7y ago
        Without objection. Cheers.