no sorry in qam_A_example

src/linear_algebra/blackbox.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Monica Omar
 -/
 import linear_algebra.inner_aut
+import linear_algebra.my_matrix.spectra
+import preq.equiv
 
 /-!
 
@@ -14,134 +16,119 @@ This file contains a blackbox theorem that says that two almost-Hermitian matric
 -/
 
 open_locale big_operators
-lemma equiv.perm.to_pequiv.to_matrix_mem_unitary_group {n : Type*} [decidable_eq n]
-  [fintype n] {𝕜 : Type*} [is_R_or_C 𝕜] [decidable_eq 𝕜] (σ : equiv.perm n) :
-  (equiv.to_pequiv σ).to_matrix ∈ matrix.unitary_group n 𝕜 :=
+
+lemma ite_eq_ite_iff {α : Type*} (a b c : α) :
+  (∀ {p : Prop} [decidable p], @ite α p _inst_1 a c = @ite α p _inst_1 b c)
+    ↔ a = b := by
+{ split; intros h,
+  { specialize @h true _,
+    simp_rw [if_true] at h,
+    exact h, },
+  { simp_rw [h, eq_self_iff_true, forall_2_true_iff], }, }
+
+lemma ite_eq_ite_iff_of_pi {n α : Type*} [decidable_eq n] (a b c :  n → α) :
+  (∀ (i j : n), ite (i = j) (a i) (c i) = ite (i = j) (b i) (c i))
+    ↔ a = b :=
 begin
-  simp_rw [matrix.mem_unitary_group_iff, ← matrix.ext_iff, matrix.mul_eq_mul,
-    matrix.mul_apply, pequiv.to_matrix_apply, boole_mul, equiv.to_pequiv_apply,
-    matrix.one_apply, option.mem_def, matrix.star_apply, pequiv.to_matrix_apply,
-    star_ite, is_R_or_C.star_def, map_one, map_zero, finset.sum_ite_eq,
-    finset.mem_univ, if_true],
-  intros i j,
-  simp_rw [equiv.to_pequiv_apply, option.mem_def, eq_comm, function.injective.eq_iff
-    (equiv.injective _)],
+  rw [← ite_eq_ite_iff _ _ c],
+  simp_rw [function.funext_iff, ite_apply],
+  split; rintros h _ _,
+  { intros i,
+    specialize h i i,
+    simp_rw [eq_self_iff_true, if_true] at h,
+    rw h, },
+  { exact h _, },
 end
 
-def multiset.of_list {α : Type*} : list α → multiset α :=
-  quot.mk _
-
--- instance {α : Type*} : has_coe (list α) (multiset α) :=
---   ⟨of_list⟩
-
 namespace matrix
 
 open_locale matrix
 
 variables {n 𝕜 : Type*} [is_R_or_C 𝕜] [fintype n] [decidable_eq n]
 
-noncomputable def is_hermitian.eigenvalues_multiset [decidable_eq 𝕜]
-  {A : matrix n n 𝕜} (hA : A.is_hermitian) :
-  multiset ℝ :=
-multiset.of_list (list.of_fn (hA.eigenvalues₀))
-
--- example [decidable_eq 𝕜]
---   {A B : matrix n n 𝕜} (hA : A.is_hermitian) (hB : B.is_hermitian) :
---   hA.eigenvalues_multiset = hB.eigenvalues_multiset :=
--- begin
---   ext,
---   congr,
--- end
-
--- example {n : ℕ} {A₁ : fin n → 𝕜} :
---   (multiset.of_list (list.of_fn A₁)) =
-
--- def eq_sets_with_multiplicities {n : ℕ} [decidable_eq 𝕜] (A₁ A₂ : fin n → 𝕜) :
---   -- (∀ (x : 𝕜), (∃ (i : fin n), A₁ i = x) ↔ ∃ (i : fin n), A₂ i = x)
---   -- ∧
---   -- -- (multiset.of_list (list.of_fn A₁))
---   ∀ i, multiset.count (finset.univ.val.map A₁) i = multiset.count (finset.univ.val.map A₂) i :=
--- begin
-
---   simp only [finset.univ],
--- end
-
-/-- TODO: change this to say equal spectra with same multiplicities. -/
+lemma is_almost_hermitian.spectra_ext [decidable_eq 𝕜]
+  {A B : n → 𝕜} (hA : (diagonal A).is_almost_hermitian)
+  (hB : (diagonal B).is_almost_hermitian) :
+  hA.spectra = hB.spectra
+  ↔ ∃ σ : equiv.perm n, ∀ i, A i = B (σ i) :=
+begin
+  sorry
+end
+
 lemma is_diagonal.spectrum_eq_iff_rotation [decidable_eq 𝕜]
-  (A₁ A₂ : n → 𝕜) :
-  spectrum 𝕜 (diagonal A₁ : matrix n n 𝕜).to_lin'
-    = spectrum 𝕜 (diagonal A₂ : matrix n n 𝕜).to_lin'
+  (A₁ A₂ : n → 𝕜) (hA₁ : (diagonal A₁).is_almost_hermitian) (hA₂ : (diagonal A₂).is_almost_hermitian) :
+  hA₁.spectra = hA₂.spectra
     ↔ ∃ (U : equiv.perm n), diagonal A₂ = inner_aut
       ⟨(equiv.to_pequiv U).to_matrix, equiv.perm.to_pequiv.to_matrix_mem_unitary_group U⟩⁻¹
       (diagonal A₁) :=
 begin
+  simp_rw [inner_aut_apply', unitary_group.inv_apply, ← matrix.ext_iff,
+    mul_apply, star_apply, ← unitary_group.star_coe_eq_coe_star,
+    unitary_group.inv_apply, star_star, unitary_group.coe_mk, pequiv.equiv_to_pequiv_to_matrix,
+    diagonal_apply, mul_ite, mul_zero, finset.sum_ite_eq', finset.mem_univ, if_true,
+    one_apply, mul_boole, star_ite, star_one, star_zero, boole_mul],
+  simp_rw [← ite_and, and_comm, ite_and, ← equiv.eq_symm_apply, finset.sum_ite_eq',
+    finset.mem_univ, if_true, (equiv.injective _).eq_iff],
+  rw [is_almost_hermitian.spectra_ext hA₁ hA₂],
+  simp_rw [ite_eq_ite_iff_of_pi, function.funext_iff],
   split,
-  { simp_rw [inner_aut_apply', unitary_group.inv_apply, ← matrix.ext_iff,
-      mul_apply, star_apply, ← unitary_group.star_coe_eq_coe_star,
-      unitary_group.inv_apply, star_star, unitary_group.coe_mk, pequiv.equiv_to_pequiv_to_matrix,
-      diagonal_apply, mul_ite, mul_zero, finset.sum_ite_eq', finset.mem_univ, if_true,
-      one_apply, mul_boole, star_ite, star_one, star_zero, boole_mul],
-    simp_rw [← ite_and, and_comm, ite_and, ← equiv.eq_symm_apply, finset.sum_ite_eq',
-      finset.mem_univ, if_true, (equiv.injective _).eq_iff, diagonal.spectrum, set.ext_iff,
-      set.mem_set_of_eq],
-    intros h,
-    simp_rw [ite_eq_iff', @eq_comm _ _ (ite _ _ _), ite_eq_iff', eq_self_iff_true,
-      imp_true_iff, and_true, forall_and_distrib],
-    let H : ∀ i j, ((i = j → ¬i = j → 0 = A₂ i) ↔ true),
-    { intros i j,
-      split,
-      { simp_rw [imp_true_iff], },
-      { intros H h1 h2,
-        contradiction, }, },
-    simp only [H, and_true],
-    have H' : ∀ (U : equiv.perm n) i j, (¬i = j → i = j → A₁ ((equiv.symm U) i) = 0) ↔ true,
-    { intros U i j,
-      split,
-      { simp_rw [imp_true_iff], },
-      { intros H h1 h2,
-        contradiction, }, },
-    simp only [H', and_true],
-    clear H H',
-    have : ∀ (U : equiv.perm n), (∀ (i j : n), (i = j → i = j → A₁ ((equiv.symm U) i) = A₂ i)) ↔
-       (∀ i, A₁ (equiv.symm U i) = A₂ i),
-    { intros U,
-      split,
-      { intros h i,--intros U i j,
-        exact h i i rfl rfl, },
-      { intros h i j h1 h2,
-        exact h _, }, },
-    simp only [this],
-    clear this,
-    sorry, },
+  { rintros ⟨σ, hσ⟩,
+    use σ,
+    intros i,
+    rw [hσ, equiv.apply_symm_apply], },
   { rintros ⟨U, hU⟩,
-    simp_rw [hU, inner_aut.spectrum_eq], },
+    use U,
+    intros i,
+    rw [hU, equiv.symm_apply_apply], },
+end
+
+lemma is_almost_hermitian.spectra_of_inner_aut [decidable_eq 𝕜]
+  {A : matrix n n 𝕜} (hA : A.is_almost_hermitian) (U : unitary_group n 𝕜) :
+  (hA.of_inner_aut U).spectra = hA.spectra :=
+begin
+  sorry
+end
+lemma is_almost_hermitian.inner_aut_spectra [decidable_eq 𝕜]
+  {A : matrix n n 𝕜}
+  (U : unitary_group n 𝕜)
+  (hA : (inner_aut U A).is_almost_hermitian) :
+  hA.spectra = ((is_almost_hermitian_iff_of_inner_aut _).mpr hA).spectra :=
+begin
+  rw ← is_almost_hermitian.spectra_of_inner_aut _ U⁻¹,
+  simp_rw [inner_aut_inv_apply_inner_aut_self],
 end
 
-lemma is_almost_hermitian.spectrum_eq_iff [decidable_eq 𝕜] [linear_order n] {A₁ A₂ : matrix n n 𝕜}
+
+lemma is_almost_hermitian.spectrum_eq_iff [decidable_eq 𝕜] {A₁ A₂ : matrix n n 𝕜}
   (hA₁ : A₁.is_almost_hermitian) (hA₂ : A₂.is_almost_hermitian) :
-  spectrum 𝕜 A₁.to_lin' = spectrum 𝕜 A₂.to_lin'
-    ↔ ∃ (U : unitary_group n 𝕜), A₂ = inner_aut U⁻¹ A₁ :=
+  hA₁.spectra = hA₂.spectra ↔ ∃ (U : unitary_group n 𝕜), A₂ = inner_aut U⁻¹ A₁ :=
 begin
-  rcases hA₁.schur_decomp with ⟨D₁, U₁, h₁⟩,
-  rcases hA₂.schur_decomp with ⟨D₂, U₂, h₂⟩,
-  rcases hA₁ with ⟨α₁, N₁, hA₁⟩,
-  rcases hA₂ with ⟨α₂, N₂, hA₂⟩,
-  rw [← h₁, ← h₂],
-  rw [inner_aut_eq_iff] at h₁ h₂,
   split,
-  { intros h,
-    simp_rw inner_aut.spectrum_eq at h,
-    obtain ⟨σ, hσ⟩ : ∃ σ : equiv.perm n, diagonal D₂
-      = inner_aut ⟨(equiv.to_pequiv σ).to_matrix, _⟩⁻¹ (diagonal D₁) :=
-    (is_diagonal.spectrum_eq_iff_rotation D₁ D₂).mp h,
-    let P : unitary_group n 𝕜 := ⟨(equiv.to_pequiv σ).to_matrix,
-      equiv.perm.to_pequiv.to_matrix_mem_unitary_group σ⟩,
-    existsi U₁ * P * U₂⁻¹,
-    simp_rw [← linear_map.comp_apply, inner_aut_comp_inner_aut, h₁,
-      _root_.mul_inv_rev, inv_inv, mul_assoc, inv_mul_self, mul_one, hσ, ← h₁,
-      ← linear_map.comp_apply, inner_aut_comp_inner_aut], },
-  { rintros ⟨U, hU⟩,
-    simp_rw [hU, ← linear_map.comp_apply, inner_aut_comp_inner_aut, inner_aut.spectrum_eq], },
+  { rcases hA₁.schur_decomp with ⟨D₁, U₁, h₁⟩,
+    rcases hA₂.schur_decomp with ⟨D₂, U₂, h₂⟩,
+    have hA₁' : is_almost_hermitian (inner_aut U₁ (diagonal D₁)) :=
+    by rw [h₁]; exact hA₁,
+    have hA₂' : is_almost_hermitian (inner_aut U₂ (diagonal D₂)) :=
+    by rw [h₂]; exact hA₂,
+    have h₁' : hA₁.spectra = hA₁'.spectra :=
+    by { simp_rw [h₁], },
+    have h₂' : hA₂.spectra = hA₂'.spectra :=
+    by { simp_rw [h₂], },
+    rw [h₁', h₂'],
+    simp_rw [is_almost_hermitian.inner_aut_spectra, is_diagonal.spectrum_eq_iff_rotation],
+    rcases hA₁ with ⟨α₁, N₁, hA₁⟩,
+    rcases hA₂ with ⟨α₂, N₂, hA₂⟩,
+    simp_rw [← h₁, ← h₂],
+    rw [inner_aut_eq_iff] at h₁ h₂,
+    rintros ⟨U, hU⟩,
+    simp_rw [hU, inner_aut_apply_inner_aut_inv, inner_aut_eq_iff,
+      inner_aut_apply_inner_aut, _root_.mul_inv_rev, inv_inv],
+    use U₁ * (⟨(equiv.to_pequiv U).to_matrix,
+      equiv.perm.to_pequiv.to_matrix_mem_unitary_group _⟩ : unitary_group n 𝕜) * U₂⁻¹,
+    simp_rw [_root_.mul_inv_rev, inv_inv, mul_assoc, inv_mul_self, mul_one,
+      inv_mul_cancel_left, mul_inv_self, inner_aut_one, linear_map.one_apply], },
+  { rintros ⟨U, rfl⟩,
+    simp_rw [is_almost_hermitian.inner_aut_spectra], },
 end
 
 /-- two matrices are _almost similar_ if there exists some
@@ -153,18 +140,10 @@ def is_almost_similar_to [fintype n] [decidable_eq n] [is_R_or_C 𝕜] (x y : ma
   `matrix.is_almost_similar_to` and `matrix.has_almost_equal_spectra_to` -/
 lemma is_almost_hermitian.has_almost_equal_spectra_to_iff_is_almost_similar_to
   [linear_order n] {x y : matrix n n ℂ} (hx : x.is_almost_hermitian) (hy : y.is_almost_hermitian) :
-  x.has_almost_equal_spectra_to y ↔ x.is_almost_similar_to y :=
+  hx.has_almost_equal_spectra_to hy ↔ x.is_almost_similar_to y :=
 begin
-  have : (∃ (β : ℂˣ), spectrum ℂ (to_lin' x) = spectrum ℂ (to_lin' ((β : ℂ) • y)))
-    ↔ (∃ β : ℂ, β ≠ 0 ∧ spectrum ℂ (to_lin' x) = spectrum ℂ (to_lin' (β • y))) :=
-  ⟨λ ⟨β, hβ⟩, ⟨(β : ℂ), ⟨units.ne_zero _, hβ⟩⟩, λ ⟨β, ⟨hβ, h⟩⟩, ⟨units.mk0 β hβ, h⟩⟩,
-  simp_rw [matrix.has_almost_equal_spectra_to, this, is_almost_hermitian.spectrum_eq_iff hx
-    (almost_hermitian_iff_smul.mp hy _), matrix.is_almost_similar_to],
-  split,
-  { rintros ⟨β, ⟨hβ, ⟨U, hU⟩⟩⟩,
-    exact ⟨units.mk0 β hβ, U, hU⟩, },
-  { rintros ⟨β, U, hU⟩,
-    exact ⟨β, ⟨units.ne_zero _, ⟨U, hU⟩⟩⟩, },
+  simp_rw [is_almost_hermitian.has_almost_equal_spectra_to,
+    is_almost_hermitian.spectrum_eq_iff, matrix.is_almost_similar_to],
 end
 
 

src/linear_algebra/kronecker_to_tensor.lean

@@ -3,10 +3,6 @@ Copyright (c) 2023 Monica Omar. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Monica Omar
 -/
-import linear_algebra.contraction
-import ring_theory.matrix_algebra
-import data.matrix.kronecker
-import data.matrix.dmatrix
 import linear_algebra.my_matrix.basic
 import linear_algebra.tensor_finite
 
@@ -141,7 +137,7 @@ begin
     algebra.tensor_product.tmul_mul_tmul, matrix.mul_eq_mul],
 end
 
-def tensor_to_kronecker :
+@[simps] def tensor_to_kronecker :
   (matrix m m R ⊗[R] matrix n n R) ≃ₐ[R] (matrix (m × n) (m × n) R) :=
 { to_fun := tensor_product.to_kronecker,
   inv_fun := matrix.kronecker_to_tensor_product,
@@ -162,12 +158,12 @@ lemma kronecker_to_tensor_to_linear_map_eq :
       : matrix (n × m) (n × m) R →ₗ[R] matrix n n R ⊗[R] matrix m m R) :=
 rfl
 
-end
-
-lemma tensor_to_kronecker_to_linear_map_eq {R m n : Type*} [comm_semiring R]
-  [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :
-  (tensor_to_kronecker
-    : (matrix m m R ⊗[R] matrix n n R) ≃ₐ[R] matrix (m × n) (m × n) R).to_linear_map
+lemma tensor_to_kronecker_to_linear_map_eq :
+  (((@tensor_to_kronecker R m n _ _ _ _ _
+    : (matrix m m R ⊗[R] matrix n n R) ≃ₐ[R] _).to_linear_map)
+    : (matrix m m R ⊗[R] matrix n n R) →ₗ[R] matrix (m × n) (m × n) R)
   = (tensor_product.to_kronecker
     : (matrix m m R ⊗[R] matrix n n R) →ₗ[R] matrix (m × n) (m × n) R) :=
 rfl
+
+end

src/linear_algebra/my_matrix/basic.lean

@@ -295,7 +295,7 @@ open_locale matrix
 variables {R n m : Type*} [semiring R] [star_add_monoid R]
   [decidable_eq n] [decidable_eq m]
 
-@[simp] lemma matrix.std_basis_matrix_conj_transpose (i : n) (j : m) (a : R) :
+lemma matrix.std_basis_matrix_conj_transpose (i : n) (j : m) (a : R) :
   (matrix.std_basis_matrix i j a)ᴴ = matrix.std_basis_matrix j i (star a) :=
 begin
   simp_rw [matrix.std_basis_matrix, ite_and],
@@ -315,19 +315,19 @@ begin
     exact h H, },
 end
 
-@[simp] lemma matrix.std_basis_matrix.star_apply (i k : n) (j l : m) (a : R) :
+lemma matrix.std_basis_matrix.star_apply (i k : n) (j l : m) (a : R) :
   star (matrix.std_basis_matrix i j a k l) = matrix.std_basis_matrix j i (star a) l k :=
 begin
   rw [← matrix.std_basis_matrix_conj_transpose, ← matrix.conj_transpose_apply],
 end
 
-@[simp] lemma matrix.std_basis_matrix.star_apply' (i : n) (j : m) (x : n × m) (a : R) :
+lemma matrix.std_basis_matrix.star_apply' (i : n) (j : m) (x : n × m) (a : R) :
   star (matrix.std_basis_matrix i j a x.fst x.snd)
     = matrix.std_basis_matrix j i (star a) x.snd x.fst :=
 by rw matrix.std_basis_matrix.star_apply
 
 /-- $e_{ij}^*=e_{ji}$ -/
-@[simp] lemma matrix.std_basis_matrix.star_one {R : Type*} [semiring R]
+lemma matrix.std_basis_matrix.star_one {R : Type*} [semiring R]
   [star_ring R] (i : n) (j : m) :
   (matrix.std_basis_matrix i j (1 : R))ᴴ = matrix.std_basis_matrix j i (1 : R) :=
 begin
@@ -336,11 +336,11 @@ begin
 end
 
 open_locale big_operators
-@[simp] lemma matrix.trace_iff {R n : Type*} [add_comm_monoid R] [fintype n] (x : matrix n n R) :
+lemma matrix.trace_iff {R n : Type*} [add_comm_monoid R] [fintype n] (x : matrix n n R) :
   x.trace = ∑ k : n, (x k k) :=
 rfl
 
-@[simp] lemma matrix.std_basis_matrix.mul_apply_basis {R p q : Type*} [semiring R]
+lemma matrix.std_basis_matrix.mul_apply_basis {R p q : Type*} [semiring R]
   [decidable_eq p] [decidable_eq q] (i x : n) (j y : m) (k z : p) (l w : q) :
   matrix.std_basis_matrix k l (matrix.std_basis_matrix i j (1 : R) x y) z w
     = (matrix.std_basis_matrix i j (1 : R) x y) * (matrix.std_basis_matrix k l (1 : R) z w) :=
@@ -349,7 +349,7 @@ begin
     and_rotate, and_assoc, and_comm],
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_apply_basis' {R p q : Type*} [semiring R]
+lemma matrix.std_basis_matrix.mul_apply_basis' {R p q : Type*} [semiring R]
   [decidable_eq p] [decidable_eq q] (i x : n) (j y : m) (k z : p) (l w : q) :
   matrix.std_basis_matrix k l (matrix.std_basis_matrix i j (1 : R) x y) z w
     = ite (i = x ∧ j = y ∧ k = z ∧ l = w) 1 0 :=
@@ -358,7 +358,7 @@ begin
            zero_mul, one_mul],
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_apply {R : Type*} [fintype n] [semiring R]
+lemma matrix.std_basis_matrix.mul_apply {R : Type*} [fintype n] [semiring R]
   (i j k l m p : n) :
   ∑ (x x_1 : n × n) (x_2 x_3 : n),
     matrix.std_basis_matrix l k (matrix.std_basis_matrix p m (1 : R) x_1.snd x_1.fst) x.snd x.fst
@@ -391,7 +391,7 @@ begin
   refl,
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_std_basis_matrix
+lemma matrix.std_basis_matrix.mul_std_basis_matrix
   {R p : Type*} [semiring R] [decidable_eq p] [fintype m]
   (i x : n) (j k : m) (l y : p) (a b : R) :
   ((matrix.std_basis_matrix i j a) ⬝ (matrix.std_basis_matrix k l b)) x y =
@@ -402,7 +402,7 @@ begin
     finset.sum_const_zero, eq_comm],
 end
 
-@[simp] lemma matrix.std_basis_matrix.mul_std_basis_matrix' {R p : Type*}
+lemma matrix.std_basis_matrix.mul_std_basis_matrix' {R p : Type*}
   [fintype n] [decidable_eq p] [semiring R]
   (i : m) (j k : n) (l : p) :
   matrix.std_basis_matrix i j (1 : R) ⬝ matrix.std_basis_matrix k l (1 : R)

src/linear_algebra/my_matrix/is_almost_hermitian.lean

@@ -213,10 +213,4 @@ begin
   exact ⟨rfl, hx⟩,
 end
 
-/-- we say a matrix $x$ _has almost equal spectra to_ another matrix $y$ if
-  there exists some scalar $0\neq\beta \in \mathbb{C}$ such that $x$ and $\beta y$ have equal spectra -/
-def has_almost_equal_spectra_to [fintype n] [decidable_eq n] [field 𝕜]
-  (x y : matrix n n 𝕜) : Prop :=
-∃ β : 𝕜ˣ, spectrum 𝕜 x.to_lin' = spectrum 𝕜 ((β : 𝕜) • y).to_lin'
-
 end matrix