Only two sorries remain for Banach-Tarski

Stream: general

[Arthur Tilley]

Hi everyone,

The first sorry is mentioned in a previous post (see this mwe).

The second is much simpler to state. The following should be a mwe.

import Mathlib

abbrev SO3 := Matrix.specialOrthogonalGroup (Fin 3) ℝ

abbrev MAT:= Matrix (Fin 3) (Fin 3) ℝ

noncomputable def as_complex (M : MAT) : Matrix (Fin 3) (Fin 3) ℂ := (algebraMap ℝ ℂ).mapMatrix M

noncomputable def cpoly (g : SO3) := Matrix.charpoly (as_complex g.val)

lemma idlem (g : SO3) :  (cpoly g).roots.count 1 = 3 → g = 1 := by
  sorry

I have tried two approaches here

I think the usual approach would be to use the fact that unitary matrices are diagonalizable, and in this case the diagonal matrix will be the identity matrix. But I can’t seem to find any theorems about diagonalizability in Mathlib, and I'm curious whether I'm missing something.

Another approach is to show that the geometric multiplicity of 1 is equal to the algebraic multiplicity. I found one theorem that gets us this but it requires that g (or the endomorphism corresponding to g) is Semisimple. But this seems to require showing that the minimal polynomial is X-1, and if I knew that I’d be done already.

(https://github.com/aetilley/banach-tarski)

Happy New Year,
Arthur

[Aaron Hill]

One possible approach:

• The roots of the charpoly are eigenvalues (https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Eigenspace/Charpoly.html#Module.End.hasEigenvalue_iff_isRoot_charpoly)
• The generalized eigenspaces span the entire space (https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.html#Module.End.iSup_maxGenEigenspace_eq_top)
• There's only a single generalized eigenvalue, so all of the other generalized eigenspaces are bot
• the linear map must therefore be diagonal (I have some messy code for this: https://github.com/Aaron1011/mathlib4/blob/1a06f50ee097ae52bafb8cf4d0c683b0a64b8078/Mathlib/Analysis/Matrix/Unitary.lean#L4)

[Aaron Hill]

it might also be useful to have that maxGenEigenSpace = eigenspace for a IsStarNormal linear map (which should include Matrix.specialOrthogonalGroup). I have an aristotle-generated proof of this here: https://github.com/Aaron1011/mathlib4/blob/1a06f50ee097ae52bafb8cf4d0c683b0a64b8078/Mathlib/Analysis/Matrix/StarNormalEigen.lean#L140

[Li Xuanji]

I threw this into Aristotle out of curiosity and it closed the goal. The key idea seems to be to use the explicit formula for the determinant of a 3x3 matrix to get an explicit formula for the characteristic polynomial.

import Mathlib

set_option maxHeartbeats 0
set_option linter.style.longLine false

abbrev SO3 := Matrix.specialOrthogonalGroup (Fin 3) ℝ

abbrev MAT:= Matrix (Fin 3) (Fin 3) ℝ

noncomputable def as_complex (M : MAT) : Matrix (Fin 3) (Fin 3) ℂ := (algebraMap ℝ ℂ).mapMatrix M

noncomputable def cpoly (g : SO3) := Matrix.charpoly (as_complex g.val)

lemma idlem (g : SO3) :  (cpoly g).roots.count 1 = 3 → g = 1 := by
  -- Since the only real roots of $P_g$ are $\pm 1$, and $P_g$ has three roots, they must all be $1$. Hence, $g$ is the identity matrix.
  have h_roots : (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} → g = 1 := by
    have h_roots : (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} → Matrix.charpoly (as_complex g.val) = (Polynomial.X - Polynomial.C 1) ^ 3 := by
      intro h_roots
      have h_poly : (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} := by
        exact h_roots;
      rw [ ← Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq ( show Polynomial.Monic ( Matrix.charpoly ( as_complex g.val ) ) from ?_ ) ];
      · norm_num [ h_poly ];
        ring;
      · aesop;
      · exact Matrix.charpoly_monic _;
    intro h; specialize h_roots h; simp_all +decide [ Matrix.charpoly, Matrix.det_fin_three ] ;
    -- By comparing coefficients, we can see that $g$ must be the identity matrix.
    have h_coeff : ∀ i j, (g.val i j : ℂ) = if i = j then 1 else 0 := by
      -- By comparing coefficients of $X^2$ on both sides of the equation, we can derive that the sum of the diagonal elements of $g$ must be 3.
      have h_diag_sum : (g.val 0 0 : ℂ) + (g.val 1 1 : ℂ) + (g.val 2 2 : ℂ) = 3 := by
        have h₁ := congr_arg ( Polynomial.eval 0 ) h_roots; have h₂ := congr_arg ( Polynomial.eval 1 ) h_roots; have h₃ := congr_arg ( Polynomial.eval ( -1 ) ) h_roots; norm_num [ Complex.ext_iff ] at *; linarith!;
      -- Since $g$ is orthogonal, we have $g^T g = I$.
      have h_orthogonal : (g.val.transpose * g.val : Matrix (Fin 3) (Fin 3) ℝ) = 1 := by
        have := g.2.1; simp_all +decide [ Matrix.mul_eq_one_comm ] ;
        exact this.2;
      -- Since $g$ is orthogonal, we have $g^T g = I$. Therefore, the sum of the squares of the entries in each row is 1.
      have h_row_squares : ∀ i, (g.val i 0 : ℝ)^2 + (g.val i 1 : ℝ)^2 + (g.val i 2 : ℝ)^2 = 1 := by
        intro i; have := congr_fun ( congr_fun h_orthogonal i ) i; simp_all +decide [ Matrix.mul_apply, Fin.sum_univ_three ] ;
        have := congr_fun ( congr_fun ( show ( g.val * g.val.transpose : Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) = 1 from by simpa [ Matrix.mul_eq_one_comm ] using h_orthogonal ) i ) i; simp_all +decide [ Matrix.mul_apply, Fin.sum_univ_three ] ; ring_nf at *; aesop;
      -- Since the sum of the squares of the entries in each row is 1 and the sum of the diagonal elements is 3, each diagonal element must be 1.
      have h_diag_one : ∀ i, (g.val i i : ℝ) = 1 := by
        norm_cast at *; simp_all +decide [ Fin.forall_fin_succ ] ;
        refine' ⟨ _, _, _ ⟩ <;> nlinarith only [ h_diag_sum, h_row_squares, sq_nonneg ( ( g.val 0 0 : ℝ ) - 1 ), sq_nonneg ( ( g.val 1 1 : ℝ ) - 1 ), sq_nonneg ( ( g.val 2 2 : ℝ ) - 1 ) ];
      simp_all +decide [ Fin.forall_fin_succ ];
      exact ⟨ ⟨ by nlinarith only [ h_row_squares.1 ], by nlinarith only [ h_row_squares.1 ] ⟩, ⟨ by nlinarith only [ h_row_squares.2.1 ], by nlinarith only [ h_row_squares.2.1 ] ⟩, by nlinarith only [ h_row_squares.2.2 ], by nlinarith only [ h_row_squares.2.2 ] ⟩;
    ext i j; specialize h_coeff i j; aesop;
  -- Since the polynomial is of degree 3, if 1 is a root with multiplicity 3, then the polynomial must be $(x-1)^3$.
  have h_poly_form : (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} ↔ Multiset.count 1 (Matrix.charpoly (as_complex g.val)).roots = 3 := by
    have h_poly_form : (Matrix.charpoly (as_complex g.val)).degree = 3 := by
      simp +decide [ Matrix.charpoly_degree_eq_dim ];
    -- Since the polynomial is of degree 3, if 1 is a root with multiplicity 3, then the polynomial must be $(x-1)^3$. Hence, the roots must be exactly {1, 1, 1}.
    have h_poly_form : (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} ↔ Multiset.count 1 (Matrix.charpoly (as_complex g.val)).roots = 3 := by
      have h_poly_form : (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} → Multiset.count 1 (Matrix.charpoly (as_complex g.val)).roots = 3 := by
        aesop
      have h_poly_form' : Multiset.count 1 (Matrix.charpoly (as_complex g.val)).roots = 3 → (Matrix.charpoly (as_complex g.val)).roots = {1, 1, 1} := by
        intro h_count
        have h_poly_form' : Multiset.card (Matrix.charpoly (as_complex g.val)).roots = 3 := by
          have h_poly_form' : Multiset.card (Matrix.charpoly (as_complex g.val)).roots ≤ 3 := by
            exact le_trans ( Polynomial.card_roots' _ ) ( Polynomial.natDegree_le_of_degree_le <| le_of_eq ‹_› );
          exact le_antisymm h_poly_form' ( by linarith [ Multiset.count_le_card 1 ( Matrix.charpoly ( as_complex g.val ) |> Polynomial.roots ) ] );
        have h_poly_form' : ∀ x ∈ (Matrix.charpoly (as_complex g.val)).roots, x = 1 := by
          intro x hx; contrapose! h_count; simp_all +decide ;
          have h_poly_form' : Polynomial.rootMultiplicity 1 (Matrix.charpoly (as_complex g.val)) + Polynomial.rootMultiplicity x (Matrix.charpoly (as_complex g.val)) ≤ 3 := by
            have h_poly_form' : Polynomial.rootMultiplicity 1 (Matrix.charpoly (as_complex g.val)) + Polynomial.rootMultiplicity x (Matrix.charpoly (as_complex g.val)) ≤ Multiset.card (Matrix.charpoly (as_complex g.val)).roots := by
              have h_poly_form' : Polynomial.rootMultiplicity 1 (Matrix.charpoly (as_complex g.val)) + Polynomial.rootMultiplicity x (Matrix.charpoly (as_complex g.val)) ≤ Multiset.card (Multiset.filter (fun y => y = 1) (Matrix.charpoly (as_complex g.val)).roots) + Multiset.card (Multiset.filter (fun y => y = x) (Matrix.charpoly (as_complex g.val)).roots) := by
                rw [ Multiset.filter_eq', Multiset.filter_eq' ] ; aesop;
              refine le_trans h_poly_form' ?_;
              rw [ ← Multiset.card_add ] ; exact Multiset.card_le_card <| Multiset.le_iff_count.mpr fun y => by by_cases hy : y = 1 <;> by_cases hy' : y = x <;> aesop;
            linarith;
          linarith [ show Polynomial.rootMultiplicity x ( Matrix.charpoly ( as_complex g.val ) ) > 0 from Nat.pos_of_ne_zero ( by aesop ) ];
        exact Multiset.eq_replicate.mpr ⟨ by assumption, h_poly_form' ⟩
      exact ⟨h_poly_form, h_poly_form'⟩;
    exact h_poly_form;
  exact fun h => h_roots <| h_poly_form.mpr h

[Arthur Tilley]

Aaron Hill said:

it might also be useful to have that maxGenEigenSpace = eigenspace for a IsStarNormal linear map (which should include Matrix.specialOrthogonalGroup). I have an aristotle-generated proof of this here: https://github.com/Aaron1011/mathlib4/blob/1a06f50ee097ae52bafb8cf4d0c683b0a64b8078/Mathlib/Analysis/Matrix/StarNormalEigen.lean#L140

Your lemma star_normal_maxGenEigenspace_eq_eigenspace appears to be exactly what I need, but it it timing out after 3 million heartbeats. Is this expected?

(I just grabbed it and the lemma above that it depends on an pasted them into a file. Not sure if this is ok. I didn't see you setting the maxHeartbeats so maybe I'm doing something wrong.)

EDIT: Ok, I decided to use the Aristotle proof for now (for another reason that I leave as a comment in the most recent commit). Although I hope to revisit this one day.

This means there is Only One Sorry remaining for the project and that is the issue of flattening bases / matrices that I outline here

(I'll suppress the urge to tag general with a new post, but I'll update the linked thread.)

[Violeta Hernández]

Aristotle can often generate very verbose and slow proofs. But it shouldn't be too hard to clean them up and golf them.

[Arthur Tilley]

Thanks @Violeta Hernández

The Aristotle code that @Li Xuanji provided is running fairly quickly. The lemma that was timing out is, I think, not Aristotle code, but I could have misunderstood Aaron. (I'll also note that I've noticed that a timeout in one place can be due to an error in another, so I might have made a mistake elsewhere.)

Anyway, I'm happy to say that the project is now sorry-free.

[Li Xuanji]

In case you want a less computational proof of idlem, I generalized it to n to force Aristotle to avoid using the matrix entries.

https://gist.github.com/ldct/19c9058719ab7076c9b590e994ca40ee

(Zulip seems to have some trouble with the size of the file, so I threw it up on Github)