Theory Cauchy_Eigenvalue_Interlacing

theory Cauchy_Eigenvalue_Interlacing
  imports Misc_Matrix_Results

begin

section "Courant-Fischer Minimax Theorem"

text
  "We took inspiration from the proof given in this set of lecture notes by Dr. David Bindel:
  https://www.cs.cornell.edu/courses/cs6210/2019fa/lec/2019-11-04.pdf. In particular, the approach
  presented there explicitly obtains the eigenvector basis via diagonal decomposition, which is
  conducive to the theorems we have available."

definition sup_defined :: "'a::preorder set ⇒ bool" where
  "sup_defined S ⟷ S ≠ {} ∧ bdd_above S"

definition inf_defined :: "'a::preorder set ⇒ bool" where
  "inf_defined S ⟷ S ≠ {} ∧ bdd_below S"

locale cf_setup = cmplx_herm_mat n for n
begin

text
  "Although the @{term cf_setup} locale adds no more assumptions beyond those from the
  @{term cmplx_herm_mat} locale, we separate the Courant Fischer proof into a separate locale so that
  the terms involved in the proof (such as @{term Λ} and @{term U}) don't pollute the namespace."

definition dimensional :: "complex vec set ⇒ nat ⇒ bool" where
  "dimensional 𝒱 k ⟷ subspace class_ring 𝒱 V ∧ vectorspace.dim class_ring (vs 𝒱) = k"

lemma dimensional_n: "dimensional 𝒱 k ⟹ 𝒱 ⊆ carrier_vec n"
  unfolding dimensional_def subspace_def submodule_def by auto

lemma dimensional_n_vec: "⋀v. v ∈ 𝒱 ⟹ dimensional 𝒱 k ⟹ v ∈ carrier_vec n"
  using dimensional_n by fast

text "Note here that we refer to the Inf and Sup rather than the Min and Max."

definition rayleigh_min where
  "rayleigh_min 𝒱 = Inf {ρ A v | v. v ≠ 0⇩v n ∧ v ∈ 𝒱}"

definition rayleigh_max where
  "rayleigh_max 𝒱 = Sup {ρ A v | v. v ≠ 0⇩v n ∧ v ∈ 𝒱}"

definition maximin :: "nat ⇒ real" where
  "maximin k = Sup {rayleigh_min 𝒱 | 𝒱. dimensional 𝒱 k}"

definition minimax :: "nat ⇒ real" where
  "minimax k = Inf {rayleigh_max 𝒱 | 𝒱. dimensional 𝒱 (n - k + 1)}"

definition maximin_defined where
  "maximin_defined k ⟷ sup_defined {rayleigh_min 𝒱 | 𝒱. dimensional 𝒱 k}"
                               
definition minimax_defined where
  "minimax_defined k ⟷ inf_defined {rayleigh_max 𝒱 | 𝒱. dimensional 𝒱 (n - k + 1)}"

abbreviation es :: "complex list" where "es ≡ eigenvalues"

definition Λ_U :: "complex mat × complex mat" where
  "Λ_U ≡ SOME (Λ, U). real_diag_decomp A Λ U ∧ es = diag_mat Λ"

definition Λ :: "complex mat" where
  "Λ ≡ fst Λ_U"

definition U :: "complex mat" where
  "U ≡ snd Λ_U"

lemma A_decomp: "real_diag_decomp A Λ U" and es: "es = diag_mat Λ"
proof-
  obtain Λ' U' where decomp: "real_diag_decomp A Λ' U'" "diag_mat Λ' = es"
    by (meson A_dim A_herm eigenvalues hermitian_real_diag_decomp_eigvals)
  thus "real_diag_decomp A Λ U" "es = diag_mat Λ"
    unfolding Λ_def U_def Λ_U_def
    by (metis (mono_tags, lifting) someI_ex case_prod_unfold old.prod.case)+
qed

lemma U_carrier: "U ∈ carrier_mat n n" and Λ_carrier: "Λ ∈ carrier_mat n n"
  using A_decomp A_dim
  unfolding real_diag_decomp_def unitary_diag_def unitarily_equiv_def similar_mat_wit_def
  by auto+

lemma UH_carrier: "U⇧H ∈ carrier_mat n n" by (simp add: U_carrier)

lemma UH_unitary: "unitary U⇧H"
  by (metis A_decomp U_carrier adjoint_is_conjugate_transpose real_diag_decompD(1) unitary_adjoint unitary_diagD(3))

lemma len_U_cols: "length (cols U) = n" using U_carrier by simp

lemma dim: "local.dim = n"
  by (simp add: dim_is_n)

lemma fin_dim: "fin_dim" by simp

lemma U_cols_orthogonal_span:
  assumes I: "I ⊆ {0..<n}"
  assumes v: "v ∈ span {col U i | i. i ∈ I}"
  assumes j: "j ∈ {0..<n} - I"
  shows "(U⇧H *⇩v v)$j = 0"
proof-
  let ?ℬ = "{col U i | i. i ∈ I}"
  have v_carrier: "v ∈ carrier_vec n"
  proof-
    have "col U i ∈ carrier_vec n" if "i < n" for i
      using U_carrier col_carrier_vec that by blast
    thus ?thesis
      using v I by (smt (verit, best) atLeastLessThan_iff mem_Collect_eq span_closed subset_iff)
  qed
  have ℬ_carrier: "?ℬ ⊆ carrier_vec n" using U_carrier col_dim by blast
  obtain cs B where cs: "finite B" "B ⊆ ?ℬ" "v = lincomb cs B"
    using v[unfolded span_def] by blast

  have "(U⇧H *⇩v v)$j = (conjugate (col U j)) ∙ v" using j len_U_cols by auto
  also have "… = (∑b ∈ B. cs b * ((conjugate (col U j)) ∙ b))"
    apply (rule sprod_vec_sum[of v n "conjugate (col U j)" B cs])
        apply (rule v_carrier) 
    using UH_carrier
       apply fastforce   
    using ℬ_carrier cs(2)
      apply order
     apply (simp add: cs(1))
    by (simp add: cs(3) lincomb_def)
  also have "… = 0"
  proof-
    have "b ∈ B ⟹ b ∙c ((col U j)) = 0" for b
      using I j cs(2) len_U_cols A_decomp diag_decomp_ortho
      using corthogonal_matD[OF diag_decomp_ortho[OF A_decomp]]
      by (smt (verit, best) Diff_iff atLeastLessThan_iff cols_length mem_Collect_eq subsetD)
    hence "b ∈ B ⟹ (conjugate (col U j)) ∙ b = 0" for b
      using U_carrier ℬ_carrier cs(2)
      by (metis (lifting) carrier_matD(1) col_dim conjugate_vec_sprod_comm subsetD)
    thus ?thesis by force
  qed
  finally show "((U⇧H *⇩v v)$j) = 0" by force
qed

lemma U_cols_basis:
  assumes I: "I ⊆ {0..<n}"
  defines [simp]: "ℬ ≡ {col U i | i. i ∈ I}"
  shows "ℬ ⊆ carrier_vec n"
        "lin_indpt ℬ"
        "card ℬ = card I"
        "vectorspace.dim class_ring (vs (span ℬ)) = card I"
proof-
  show carrier: "ℬ ⊆ carrier_vec n" using U_carrier ℬ_def col_dim by blast

  have "lin_indpt (set (cols U))" using A_dim diag_decomp_cols_lin_indpt[OF A_decomp] by blast
  moreover have "ℬ ⊆ set (cols U)"
    unfolding ℬ_def
    using I U_carrier len_U_cols
    by (smt (verit, best) cols_def cols_length image_iff list.set_map mem_Collect_eq set_upt subset_iff)
  ultimately show li: "lin_indpt ℬ" using supset_ld_is_ld by blast

  have "i ∈ I ⟹ j ∈ I ⟹ i ≠ j ⟹ col U i ≠ col U j" for i j
    using I A_decomp U_carrier
    by (metis det_identical_cols diag_decomp_invertible invertible_det lessThan_atLeast0 lessThan_iff subset_eq)
  hence "inj_on (col U) I" using I inj_on_subset unfolding inj_on_def by blast
  moreover have "ℬ = (col U)`I" unfolding ℬ_def by blast
  ultimately show "card ℬ = card I" using card_image[of "col U" I] by argo
  thus "vectorspace.dim class_ring (vs (span ℬ)) = card I"
    apply (subst dim_of_lin_indpt_span[OF li carrier])
    using I by (simp add: finite_subset)
qed

end

context cmplx_herm_mat
begin

interpretation A?: cf_setup A n by unfold_locales

text "In the local context, we interpret the @{const cf_setup} locale, giving us access to the
abbreviation @{const es} as well as other constants like @{const U} and @{const Λ} which form
the decomposition of @{term A}. Once the local context is closed, this interpretation is no
longer accessible, so these names do not pollute the @{const cmplx_herm_mat} namespace."

lemma len_eigenvalues: "length es = n"
  by (metis Λ_carrier es carrier_matD(1) diag_mat_def length_map length_upt verit_minus_simplify(2))

lemma unit_vec_rayleigh_formula:
  assumes unit_v: "vec_norm v = 1"
  assumes v_dim: "v ∈ carrier_vec n"
  shows "ρ A v = (∑j ∈ {..<n}. es!j * (cmod ((U⇧H *⇩v v)$j))^2)"
proof-
  have U_Λ: "unitary U ∧ unitary U⇧H" "A = U * Λ * U⇧H" "U⇧H ∈ carrier_mat n n"
      apply (metis U_carrier A_decomp adjoint_is_conjugate_transpose real_diag_decomp_def unitarily_equiv_def unitary_adjoint unitary_diag_def)
     apply (metis A_decomp adjoint_is_conjugate_transpose real_diag_decomp_def similar_mat_wit_def unitarily_equiv_def unitary_diag_def)
    by (simp add: U_carrier)
  have "diagonal_mat Λ" using A_decomp unfolding real_diag_decomp_def by fastforce
  hence Λ_diag_mult: "⋀x i. x ∈ carrier_vec n ⟹ i ∈ {..<n} ⟹ (Λ *⇩v x)$i = (Λ$$(i,i) * x$i)"
    using Λ_carrier diagonal_mat_mult_vec by blast
  have Λ_diag_eigenvals: "⋀i. i ∈ {..<n} ⟹ Λ$$(i,i) = es!i"
    using A_decomp Λ_carrier by (simp add: diag_mat_def es)

  define x where "x ≡ U⇧H *⇩v v"
  hence x_dim: "x ∈ carrier_vec n" using U_Λ(3) mult_mat_vec_carrier v_dim by blast
  hence x_conj_dim: "conjugate x ∈ carrier_vec n" by simp
  have x_norm: "vec_norm x = 1" using U_Λ unit_v unitary_vec_norm v_dim x_def by presburger

  have *: "⋀i. i ∈ {..<n} ⟹ (conjugate x)$i = conjugate (x$i)"
    unfolding conjugate_vec_def using x_dim by auto

  have "v ∙c v = 1" using unit_v csqrt_eq_1 unfolding vec_norm_def by blast
  hence "QF A v / Complex_Matrix.inner_prod v v = QF A v" by simp
  hence "ρ A v = complex_of_real (Re (QF A v))"
    unfolding rayleigh_quotient_def rayleigh_quotient_complex_def by simp
  also have "… = QF A v"
    using hermitian_quadratic_form_real[OF v_dim] by simp
  also have "… = inner_prod v ((U * Λ * U⇧H) *⇩v v)"
    unfolding quadratic_form_def using U_Λ by argo
  also have "… = inner_prod v (U *⇩v ((Λ * U⇧H) *⇩v v))"
    by (smt (verit, best) Λ_carrier U_carrier More_Matrix.carrier_vec_conjugate assoc_mat_mult_vec' carrier_dim_vec mat_vec_mult_assoc transpose_carrier_mat v_dim)
  also have "… = inner_prod (U⇧H *⇩v v) ((Λ * U⇧H) *⇩v v)"
    by (metis Λ_carrier U_carrier More_Matrix.carrier_vec_conjugate adjoint_def_alter adjoint_is_conjugate_transpose mult_carrier_mat mult_mat_vec_carrier transpose_carrier_mat v_dim)
  also have "… = (Λ *⇩v x) ∙c x"
    by (metis Λ_carrier U_carrier More_Matrix.carrier_vec_conjugate carrier_vecD mat_vec_mult_assoc transpose_carrier_mat v_dim x_def)
  also have "… = (∑j ∈ {..<n}. (es!j * x$j) * conjugate (x$j))"
    using Λ_diag_mult x_dim Λ_diag_eigenvals atLeast0LessThan x_dim by (simp add: inner_prod_def scalar_prod_def)
  also have "… = (∑j ∈ {..<n}. es!j * (cmod (x$j))^2)"
    by (smt (verit) cring_simprules(11) mult_conj_cmod_square of_real_mult of_real_sum sum.cong)
  finally show "ρ A v = (∑j ∈ {..<n}. es!j * (cmod (x$j))^2)" 
    using of_real_eq_iff by blast
qed

lemma rayleigh_bdd_below': "∀v ∈ carrier_vec n. v ≠ 0⇩v n ⟶ ρ A v ≥ Min (Re ` set es)"
proof-
  define m where "m ≡ Min (Re ` set es)"
  have "ρ A v ≥ m" if *: "v ∈ carrier_vec n" "v ≠ 0⇩v n" for v
  proof-
    define v' where "v' ≡ vec_normalize v"
    have v': "vec_norm v' = 1 ∧ v' ∈ carrier_vec n"
      using normalized_vec_norm[of v n] unfolding vec_norm_def v'_def
      using * csqrt_1 normalized_vec_dim by presburger
    have "ρ A v = ρ A v'"
      using A_dim *(1) v' v'_def
      by (metis normalize_zero rayleigh_quotient_scale_complex vec_eq_norm_smult_normalized vec_norm_zero)
    also have "… = (∑i ∈ {..<n}. es!i * (cmod ((U⇧H *⇩v v')$i))^2)"
      using unit_vec_rayleigh_formula * v' by blast
    also have "… ≥ m"
    proof-
      have "vec_norm (U⇧H *⇩v v') = 1"
        by (metis v' U_carrier A_decomp Complex_Matrix.unitary_def adjoint_dim_row adjoint_is_conjugate_transpose carrier_matD(2) real_diag_decomp_def unitary_adjoint unitary_diagD(3) unitary_vec_norm)
      moreover have "vec_norm (U⇧H *⇩v v') = csqrt (∑i ∈ {..<n}. (cmod ((U⇧H *⇩v v')$i))^2)"
        by (metis complex_vec_norm_sum U_carrier carrier_dim_vec carrier_matD(2) dim_mult_mat_vec dim_row_conjugate index_transpose_mat(2))
      ultimately have norm: "(∑i ∈ {..<n}. (cmod ((U⇧H *⇩v v')$i))^2) = 1"
        by (metis Re_complex_of_real one_complex.sel(1) one_power2 power2_csqrt)

      have "finite (Re ` set es)" by simp
      hence "∀x ∈ Re ` set es. m ≤ x" using Min_le m_def by blast
      moreover have "∀i ∈ {..<n}. ∃x ∈ Re ` set es. x = es!i"
        using es eigenvalues_real len_eigenvalues by (simp add: subsetD)
      ultimately have "⋀i. i ∈ {..<n} ⟹ m ≤ es!i"
        by (metis Im_complex_of_real Re_complex_of_real less_eq_complex_def)
      hence ineq: "⋀i. i ∈ {..<n} ⟹  m * (cmod ((U⇧H *⇩v v')$i))^2 ≤ es!i * (cmod ((U⇧H *⇩v v')$i))^2"
        by (metis conjugate_square_positive mult_conj_cmod_square mult_right_mono of_real_hom.hom_mult)
        
      have "m ≤ m * (∑i ∈ {..<n}. (cmod ((U⇧H *⇩v v')$i))^2)" using norm by auto
      also have "… = (∑i ∈ {..<n}. m * (cmod ((U⇧H *⇩v v')$i))^2)"
        by (simp add: mult_hom.hom_sum)
      also have "… ≤ (∑i ∈ {..<n}. es!i * (cmod ((U⇧H *⇩v v')$i))^2)"
        by (smt (verit, best) of_real_sum sum_mono ineq)
      finally show ?thesis
        by (metis Im_complex_of_real Re_complex_of_real less_eq_complex_def)
    qed
    finally show "ρ A v ≥ m" by (simp add: less_eq_complex_def)
  qed
  thus ?thesis unfolding m_def by blast
qed

lemma rayleigh_bdd_below:
  assumes "dimensional 𝒱 k"
  shows "∃m. ∀v ∈ 𝒱. v ≠ 0⇩v n ⟶ ρ A v ≥ m"
  by (meson assms dimensional_n rayleigh_bdd_below' subsetD)

lemma rayleigh_min_exists:
  assumes "dimensional 𝒱 k"
  shows "∀x ∈ {ρ A v | v. v ≠ 0⇩v n ∧ v ∈ 𝒱}. rayleigh_min 𝒱 ≤ x"
  using rayleigh_bdd_below[OF assms]
  unfolding rayleigh_min_def
  by (smt (verit) bdd_below.I cInf_lower mem_Collect_eq)

lemma courant_fischer_unit_rayleigh_helper1:
  assumes "dimensional 𝒱 (k + 1)"
  shows "∃v. vec_norm v = 1 ∧ v ∈ 𝒱 ∧ v ≠ 0⇩v n ∧ ρ A v ≤ es!k"
proof-
  define ℬ' where "ℬ' = {col U i | i. i ∈ {k..<n}}"
  have 𝒱: "subspace class_ring 𝒱 V"
    using assms dimensional_def by blast
  have k: "k < n"
    using assms unfolding dimensional_def
    using subspace_dim[of 𝒱] subspace_fin_dim[of 𝒱] fin_dim dim
    by linarith
  have ℬ'_dim: "vectorspace.dim class_ring (vs (span ℬ')) = n - k" and carrier_ℬ': "ℬ' ⊆ carrier_vec n"
    using U_cols_basis[of "{k..<n}", folded ℬ'_def] by auto

  obtain v where v: "v ∈ 𝒱 ∩ span ℬ'" and nz: "v ≠ 0⇩v n"
    using dim_sum_nontriv_int[OF 𝒱 span_is_subspace[OF carrier_ℬ'] _ fin_dim, unfolded ℬ'_dim]
    using assms[unfolded dimensional_def] dim k
    by auto
  define v' where "v' ≡ vec_normalize v"
  have v': "vec_norm v' = 1" "v' ∈ 𝒱 ∩ span ℬ'" "v' ∈ carrier_vec n"
  proof-
    have "subspace class_ring (span ℬ') V" using carrier_ℬ' span_is_subspace by presburger
    thus "v' ∈ 𝒱 ∩ span ℬ'"
      using v carrier_ℬ' assms 𝒱
      unfolding v'_def vec_normalize_def dimensional_def
      using assms dimensional_n module_incl_imp_submodule submoduleE(4) submodule_is_module
      by auto
    show "vec_norm v' = 1" "v' ∈ carrier_vec n"
      using v nz assms unfolding v'_def
       apply (metis IntE basic_trans_rules(31) csqrt_1 dimensional_n normalized_vec_norm vec_norm_def)
      using v nz assms unfolding v'_def
      by (meson IntE basic_trans_rules(31) dimensional_n normalized_vec_dim)
  qed

  have *: "i < k ⟹ cmod ((U⇧H *⇩v v')$i) = 0" for i
    using U_cols_orthogonal_span[of "{k..<n}" v' i] k v'(2)[unfolded ℬ'_def] by force
  have "ρ A v' = (∑i=0..<n. es!i * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2))"
    by (rule unit_vec_rayleigh_formula[OF v'(1,3), folded atLeast0LessThan])
  also have "… = (∑i=0..<k. es!i * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2))
      + (∑i=k..<n. es!i * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2))"
    using k by (metis (lifting) le_eq_less_or_eq sum.atLeastLessThan_concat zero_le)
  also have "… = (∑i=k..<n. es!i * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2))"
    using * by fastforce
  also have "… ≤ (∑i=k..<n. es!k * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2))"
  proof-
    have "∀i < n. k ≤ i ⟶ es!i ≤ es!k"
      using eigenvalues_sorted by (simp add: le_eq_less_or_eq len_eigenvalues sorted_wrt_iff_nth_less)
    hence "∀i ∈ {k..<n}. es!i * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2)
        ≤ es ! k * complex_of_real ((cmod ((U⇧H *⇩v v')$i))⇧2)"
      apply (clarify, simp add: atLeastLessThan_def lessThan_def atLeast_def)
      by (metis conjugate_square_positive mult_conj_cmod_square mult_right_mono of_real_power)
    thus ?thesis by (meson sum_mono)
  qed
  also have "… = es!k * (∑i=k..<n. ((cmod ((U⇧H *⇩v v')$i))⇧2))"
    by (simp add: mult_hom.hom_sum)
  also have "… = es!k * (vec_norm (U⇧H *⇩v v'))⇧2"
  proof-
    have 1: "U⇧H *⇩v v' ∈ carrier_vec n" using UH_carrier v'(3) by force
    have "(vec_norm (U⇧H *⇩v v'))⇧2 = (∑i<n. ((cmod ((U⇧H *⇩v v')$i))⇧2))"
      unfolding complex_vec_norm_sum[OF 1] by force
    also have "… = (∑i=0..<k. ((cmod ((U⇧H *⇩v v')$i))⇧2)) + (∑i=k..<n. ((cmod ((U⇧H *⇩v v')$i))⇧2))"
      using k by (metis k atLeast0LessThan le_eq_less_or_eq sum.atLeastLessThan_concat zero_order(1))
    also have "… = (∑i=k..<n. ((cmod ((U⇧H *⇩v v')$i))⇧2))" using * by simp
    finally show ?thesis by simp
  qed
  also have "… = es!k"
    using unitary_vec_norm[OF v'(3) UH_carrier UH_unitary, unfolded v'(1)] by simp
  finally show ?thesis using v' by (metis IntE field.one_not_zero vec_norm_zero)
qed

lemma courant_fischer_unit_rayleigh_helper2:
  assumes k: "k < n"
  defines "es_R ≡ map Re es"
  shows "∃𝒱. dimensional 𝒱 (k + 1) ∧ (∀v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ⟶ es_R ! k ≤ ρ A v)"
proof-
  let ?geq = "λv. ρ A v ≥ es_R!k"
  let ?P = "λ𝒱 v. v ≠ 0⇩v n ∧ v ∈ 𝒱 ∧ vec_norm v = 1"
  let ?Q = "λ𝒱. dimensional 𝒱 (k + 1)"

  have es_R: "map complex_of_real es_R = es"
  proof-
    { fix i assume *: "i < length es"
      hence "es!i ∈ Reals" using eigenvalues_real by auto
      hence "complex_of_real (es_R!i) = es!i" by (simp add: * es_R_def)
    }
    thus ?thesis by (simp add: es_R_def map_nth_eq_conv)
  qed

  let ?ℬ = "{col U i | i. i ∈ {..<k + 1}}"
  define 𝒱 where "𝒱 ≡ span ?ℬ"
  have ℬ_card: "card ?ℬ = k + 1" and ℬ_dim: "?ℬ ⊆ carrier_vec n" and 1: "?Q 𝒱"
    unfolding dimensional_def 𝒱_def
    using assms U_carrier U_cols_basis[of "{..<k + 1}"] 
    by (simp_all add: span_is_subspace lessThan_atLeast0)
  moreover have 2: "∀v. ?P 𝒱 v ⟶ ?geq v"
  proof clarify
    fix v :: "complex vec"
    assume *: "v ≠ 0⇩v n" and **: "v ∈ 𝒱" and ***: "vec_norm v = 1"

    have v_dim: "v ∈ carrier_vec n" using ** ℬ_dim 𝒱_def span_closed by blast

    (* cols k+1 to n of U are orthogonal to v *)
    define x where "x ≡ U⇧H *⇩v v"
    have x_dim: "x ∈ carrier_vec n"
      by (metis U_carrier More_Matrix.carrier_vec_conjugate mult_mat_vec_carrier transpose_carrier_mat v_dim x_def)
    have x_norm: "vec_norm x = 1"
      using ***
      using A_decomp[unfolded real_diag_decomp_def unitary_diag_def unitarily_equiv_def]
      using x_def x_dim v_dim
      by (metis Complex_Matrix.unitary_def adjoint_is_conjugate_transpose carrier_vecD dim_mult_mat_vec unitary_adjoint unitary_vec_norm)

    have ineq: "⋀j. j ∈ {..<n} ⟹ es!k * (cmod (x$j))^2 ≤ es!j * (cmod (x$j))^2"
    proof- (* case on j ≤ k *)
      fix j
      assume *: "j ∈ {..<n}"
      show "es!k * (cmod (x$j))^2 ≤ es!j * (cmod (x$j))^2"
      proof(cases "j ≤ k")
        case True
        hence "es!k ≤ es!j"
          using k by (metis len_eigenvalues antisym_conv1 eigenvalues_sorted nless_le sorted_wrt_nth_less)
        thus ?thesis by (simp add: less_eq_complex_def mult_right_mono)
      next
        case False
        hence "j > k" by simp
        hence "cmod (x$j) = 0"
          using * **[unfolded 𝒱_def] assms U_cols_orthogonal_span[of "{..<k + 1}" v j, folded x_def]
          by (metis Diff_iff Suc_eq_plus1 atLeastLessThan_iff lessThan_atLeast0 lessThan_subset_iff
              less_iff_succ_less_eq norm_zero not_less_eq)
        thus ?thesis by fastforce
      qed
    qed

    have unit: "(∑j ∈ {..<n}. (cmod (x$j))^2) = 1"
      by (metis atLeast0LessThan carrier_vecD cpx_vec_length_square of_real_eq_1_iff power_one vec_norm_sq_cpx_vec_length_sq x_dim x_norm)
    have "es_R!k = es!k" using k eigenvalues_real es_R len_eigenvalues by (metis length_map nth_map)
    also have "… = es!k * (∑j ∈ {..<n}. (cmod (x$j))^2)" by (simp add: unit)
    also have "… = (∑j ∈ {..<n}. es!k * (cmod (x$j))^2)" by (simp add: mult_hom.hom_sum)
    also have "… ≤ (∑j ∈ {..<n}. es!j * (cmod (x$j))^2)" by (meson ineq sum_mono)
    also have "… = ρ A v" using unit_vec_rayleigh_formula A_decomp *** v_dim x_def by fastforce
    finally show "?geq v" by (simp add: less_eq_complex_def)
  qed
  ultimately have *: "dimensional 𝒱 (k + 1) ∧ (∀v. ?P 𝒱 v ⟶ es_R ! k ≤ ρ A v)" by blast
  moreover have "∀v. v ≠ 0⇩v n ⟶ v ∈ 𝒱 ⟶ ρ A v = ρ A (vec_normalize v) ∧ ?P 𝒱 (vec_normalize v)"
  proof (clarify, rule conjI)
    fix v assume v: "v ≠ 0⇩v n" "v ∈ 𝒱"
    show "?P 𝒱 (vec_normalize v)"
      using 1 * v vec_normalize_norm[of v n] submodule_is_module[of 𝒱]
      using vec_normalize_def[of v] dimensional_def[of 𝒱 "k + 1"] subspace_def[of class_ring 𝒱 V]
      by (metis dimensional_n dimensional_n_vec module_incl_imp_submodule rmult_0 submoduleE(4)
          vec_eq_norm_smult_normalized)
    show "ρ A v = ρ A (vec_normalize v)"
      unfolding vec_normalize_def 
      using rayleigh_quotient_scale_complex[OF A_dim, of v "1 / vec_norm v"] v * dimensional_n_vec vec_norm_zero
      by auto
  qed
  ultimately show ?thesis by metis
qed

subsection "Max-Min Statement"

proposition courant_fischer_maximin:
  assumes k: "k < n"
  shows "es!k = maximin (k + 1)"
        "maximin_defined (k + 1)"
proof-
  define es_R where "es_R ≡ map Re es"
  have es_R: "map complex_of_real es_R = es"
  proof-
    { fix i assume *: "i < length es"
      hence "es!i ∈ Reals" using eigenvalues_real by auto
      hence "complex_of_real (es_R!i) = es!i" by (simp add: * es_R_def)
    }
    thus ?thesis by (simp add: es_R_def map_nth_eq_conv)
  qed
  hence es_R_i: "⋀i. i ∈ {..<n} ⟹ es_R!i = Re (es!i)"
    using A_dim eigenvalues eigvals_poly_length es_R_def by simp
  hence es_R_k: "es_R!k = Re (es!k)" by (simp add: k)

  let ?leq = "λv. ρ A v ≤ es_R!k"
  let ?geq = "λv. ρ A v ≥ es_R!k"
  let ?P = "λ𝒱 v. v ≠ 0⇩v n ∧ v ∈ 𝒱"
  let ?Q = "λ𝒱. dimensional 𝒱 (k + 1)"
  let ?S⇩ρ = "λ𝒱. {ρ A v |v. ?P 𝒱 v}"

  have 1: "⋀𝒱. ?Q 𝒱 ⟹ (∃v. ?P 𝒱 v ∧ ?leq v)"
    using es_R_k by (metis Re_complex_of_real courant_fischer_unit_rayleigh_helper1 less_eq_complex_def)

  have 2: "∃𝒱. ?Q 𝒱 ∧ (∀v. ?P 𝒱 v ⟶ ?geq v)"
    using courant_fischer_unit_rayleigh_helper2[OF k] unfolding es_R_def by blast

  from 2 obtain 𝒱' where 𝒱': "?Q 𝒱' ∧ (∀v. ?P 𝒱' v ⟶ ?geq v)" by blast
  from this 1 obtain v' where v': "?P 𝒱' v' ∧ ?leq v'" by presburger
  moreover have all_v_geq: "∀v. ?P 𝒱' v ⟶ ?geq v" using 𝒱' by blast
  ultimately have "ρ A v' = es_R!k" by fastforce
  hence "es_R!k ∈ ?S⇩ρ 𝒱'" using v' by force
  moreover have "∀x ∈ ?S⇩ρ 𝒱'. x ≥ es_R!k" using all_v_geq by blast
  ultimately have "es_R!k = Inf (?S⇩ρ 𝒱')" by (smt (verit) rayleigh_bdd_below cInf_eq_minimum)
  moreover have "⋀𝒱. ?Q 𝒱 ⟹ Inf (?S⇩ρ 𝒱) ≤ es_R!k"
  proof-
    fix 𝒱
    assume *: "?Q 𝒱"
    then obtain v where v: "?P 𝒱 v ∧ ?leq v" using 1 by presburger
    then have "ρ A v ∈ ?S⇩ρ 𝒱" by blast
    then have "Inf (?S⇩ρ 𝒱) ≤ ρ A v"
      using rayleigh_min_exists[OF *] k rayleigh_min_def cf_setup_axioms by auto
    thus "Inf (?S⇩ρ 𝒱) ≤ es_R!k" using v by linarith
  qed
  ultimately have *: "es_R!k ∈ {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱} ∧ (∀x ∈ {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱}. x ≤ es_R!k)"
    using 𝒱' by blast
  hence "Sup {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱} = es_R!k" by (meson cSup_eq_maximum)
  moreover have "Sup {Inf (?S⇩ρ 𝒱) | 𝒱. ?Q 𝒱} = maximin (k + 1)"
    unfolding maximin_def rayleigh_min_def dimensional_def by blast
  ultimately show "es!k = maximin (k + 1)"
    using k es_R by (metis len_eigenvalues length_map nth_map)
  show "maximin_defined (k + 1)"
    using * unfolding maximin_defined_def sup_defined_def rayleigh_min_def bdd_above_def by blast
qed

subsection "Min-Max Statement"

interpretation neg: cf_setup "-A" n
  by (unfold_locales, simp add: A_dim, simp add: negative_hermitian)

lemma neg_es: "neg.es = rev (map (λx. -x) es)"
proof-
  let ?l = "(map (λx. -x) es)"
  { fix i j assume "i < j" "j < length ?l"
    moreover then have "es!i ≥ es!j"
      using eigenvalues_sorted sorted_wrt_iff_nth_less[of "(≥)" es] by force
    ultimately have "?l!i ≤ ?l!j" by simp
  }
  hence "sorted_wrt (≤) ?l" by (metis sorted_wrt_iff_nth_less)
  thus ?thesis
    using sorted_wrt_rev
    by (metis A_herm hermitian_is_square neg.eigenvalues_unique neg_mat_eigvals rev_rev_ident
        eigenvalues(1))
qed

lemma maximin_minimax:
  assumes k: "k < n"
  shows "neg.maximin (n - k) = - minimax (k + 1)"
        "neg.maximin_defined (n - k) ⟹ minimax_defined (k + 1)"
proof-
  define P where "P ≡ λ(v::complex vec) 𝒱. v ≠ 0⇩v n ∧ v ∈ 𝒱"
  define Q where "Q ≡ λ𝒱. neg.dimensional 𝒱 (n - k)"

  have "Inf {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = - Sup (uminus`{Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱})"
    using Inf_real_def .
  moreover have *: "uminus`{Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = {- Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}"
    by blast
  moreover have **: "{- Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = {Inf {ρ (-A) v |v. P v 𝒱} |𝒱. Q 𝒱}"
  proof-
    have "⋀𝒱. Q 𝒱 ⟹ - Sup {ρ A v |v. P v 𝒱} = Inf {ρ (-A) v |v. P v 𝒱}"
    proof-
      fix 𝒱 assume *: "Q 𝒱"
      have "Inf {ρ (-A) v |v. P v 𝒱} = - Sup (uminus`{ρ (-A) v |v. P v 𝒱})"
        using Inf_real_def by fast
      moreover have "uminus`{ρ (-A) v |v. P v 𝒱} = {- ρ (-A) v |v. P v 𝒱}" by blast
      moreover have "{- ρ (-A) v |v. P v 𝒱} = {ρ A v |v. P v 𝒱}"
      proof-
        have "⋀v. P v 𝒱 ⟹ - ρ (- A) v = ρ A v"
          using * A_dim
          unfolding P_def Q_def
          by (metis dimensional_n_vec rayleigh_quotient_negative)
        thus ?thesis by metis
      qed
      ultimately show "- Sup {ρ A v |v. P v 𝒱} = Inf {ρ (-A) v |v. P v 𝒱}" by presburger
    qed
    thus ?thesis by force
  qed
  ultimately have "- Inf {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} = Sup {Inf {ρ (-A) v |v. P v 𝒱} |𝒱. Q 𝒱}"
    by auto
  moreover have "n - (k + 1) + 1 = n - k" using k by fastforce
  ultimately show "cf_setup.maximin (-A) n (n - k) = - cf_setup.minimax A n (k + 1)"
    by (simp add: minimax_def neg.maximin_def neg.rayleigh_min_def rayleigh_max_def P_def Q_def)

  show "cf_setup.minimax_defined A n (k + 1)" if "cf_setup.maximin_defined (-A) n (n - k)"
  proof-
    have "{Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱} ≠ {}"
      using that
      unfolding neg.maximin_defined_def sup_defined_def neg.rayleigh_min_def P_def Q_def
      by fast
    moreover have "bdd_below {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}"
    proof-
      have "bdd_above {Inf {ρ (-A) v |v. P v 𝒱} |𝒱. Q 𝒱}"
        using that
        unfolding neg.maximin_defined_def sup_defined_def neg.rayleigh_min_def P_def Q_def
        by argo
      hence "bdd_above {- Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}" using ** by argo
      hence "bdd_below {Sup {ρ A v |v. P v 𝒱} |𝒱. Q 𝒱}" by (smt (verit, best) * bdd_above_uminus)
      thus ?thesis by blast
    qed
    moreover have "n - k = n - (k + 1) + 1" using k by simp
    ultimately show ?thesis
      unfolding minimax_defined_def inf_defined_def rayleigh_max_def P_def Q_def by algebra
  qed
qed

lemma courant_fischer_minimax:
  assumes k: "k < n"
  shows "es!k = minimax (k + 1)" "minimax_defined (k + 1)"
proof-
  define es' where "es' = rev (map (λx. -x) es)"
  have *: "es'!(n - k - 1) = neg.maximin (n - k)
      ∧ neg.maximin_defined (n - k)"
    using k neg.courant_fischer_maximin[of "n - k - 1"]
    using neg.eigenvalues_unique neg_es es'_def
    by (metis One_nat_def Suc_diff_Suc Suc_less_eq diff_less_Suc minus_nat.simps(1) semiring_norm(174)
        zero_less_diff)
  moreover have "es!k = - es'!(n - k - 1)"
  proof-
    have "n - k - 1 < length es" using k A_dim eigenvalues eigvals_poly_length by force
    moreover have "length es = n" using A_dim eigenvalues by auto
    ultimately have "es!k = (rev es)!(n - k - 1)"
      using rev_nth[of "n - k - 1" es] by (simp add: Suc_diff_Suc k le_simps(1))
    also have "… = rev (map (λx. -x) (map (λx. -x) es))!(n - k - 1)"
      by simp
    also have "… = - es'!(n - k - 1)"
      by (metis ‹n - k - 1 < length es› es'_def length_map length_rev nth_map rev_map)
    finally show ?thesis .
  qed
  ultimately show "es!k = cf_setup.minimax A n (k + 1)" "cf_setup.minimax_defined A n (k + 1)"
    using assms maximin_minimax by force+
qed

subsection "Theorem Statement"

theorem courant_fischer:
  assumes "k < n"
  shows "es!k = minimax (k + 1)"
        "es!k = maximin (k + 1)"
        "minimax_defined (k + 1)"
        "maximin_defined (k + 1)"
  using courant_fischer_minimax courant_fischer_maximin maximin_minimax assms by algebra+

section "Cauchy Eigenvalue Interlacing Theorem"

text
  "We follow the proof given in this set of lecture notes by Dr. David Bindel:
  https://www.cs.cornell.edu/courses/cs6210/2019fa/lec/2019-11-04.pdf"

subsection "Theorem Statement and Proof"

lemma cauchy_eigval_interlacing_aux:
  fixes W B :: "complex mat"
  fixes α β :: "complex list"
  fixes j m :: nat

  defines "B ≡ W⇧H * A * W"
  defines "α ≡ eigenvalues"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes j: "j < n" "j < m"
  assumes m: "0 < m" "m ≤ n"

  assumes W_dim: "W ∈ carrier_mat n m"
  assumes W_isom: "isometry_mat W n m"

  shows "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
proof-
  interpret B: cf_setup B m
    using A_dim A_herm W_dim B_def compression_is_hermitian(1)
    by (metis carrier_matD(2) carrier_mat_triv cmplx_herm_mat.intro
         cf_setup.intro dim_row_conjugate index_mult_mat(2,3) index_transpose_mat(2))

  show α_real: "set α ⊆ ℝ"
    using hermitian_real_diag_decomp_eigvals[OF A_dim A_herm] α_def eigenvalues(1) by metis
  show β_real: "set β ⊆ ℝ"
    using hermitian_real_diag_decomp_eigvals[of B n β] B.eigenvalues(1) β_def
    by (metis B.A_dim B.A_herm hermitian_real_diag_decomp_eigvals)
  show α_length: "length α = n" using α_def eigenvalues(1) A_dim α_def by auto
  have "B ∈ carrier_mat m m" by (simp add: B.A_dim)
  show β_length: "length β = m" using B.A_dim B.eigenvalues(1) β_def by fastforce

  let ?S⇩1 = "{B.rayleigh_min 𝒱 | 𝒱. B.dimensional 𝒱 (j + 1)}"
  let ?S⇩2 = "{A.rayleigh_min ((*⇩v) W ` 𝒱) |𝒱. B.dimensional 𝒱 (j + 1)}"
  let ?S⇩3 = "{A.rayleigh_min 𝒱 | 𝒱. A.dimensional 𝒱 (Suc j)}"

  interpret isom: isometry_mat W n m by (rule W_isom)
  have *: "⋀𝒱. B.dimensional 𝒱 (Suc j) ⟹ A.dimensional ((*⇩v) W ` 𝒱) (Suc j)"
  proof-
    fix 𝒱 assume *: "B.dimensional 𝒱 (Suc j)"
    note Bdim =
      conjunct1[OF *[unfolded B.dimensional_def]]
      conjunct2[OF *[unfolded B.dimensional_def]]
    show "A.dimensional ((*⇩v) W ` 𝒱) (Suc j)"
      unfolding A.dimensional_def isom.inj_subspace_image[OF isom.is_inj Bdim(1) B.fin_dim] Bdim(2)
      using isom.subspace_image[OF Bdim(1)]
      by blast
  qed
  hence S⇩2_sub_S⇩3: "?S⇩2 ⊆ ?S⇩3" by auto
  have bdd_above_S⇩3: "bdd_above ?S⇩3"
    using j(1) courant_fischer α_def
    by (metis (lifting) ext A.maximin_defined_def Suc_eq_plus1 sup_defined_def)
  hence bdd_above_S⇩2: "bdd_above ?S⇩2"
    using S⇩2_sub_S⇩3 by (meson basic_trans_rules(31) bdd_above_def)
  have S⇩2_ne: "?S⇩2 ≠ {}"
    using j(2)
    by (metis (mono_tags, lifting) B.courant_fischer_unit_rayleigh_helper2 empty_Collect_eq)

  have "Re (β!j) = B.maximin (j + 1)"
    using B.courant_fischer(2)[OF j(2)] β_def by simp
  also have "… ≤ Sup {A.rayleigh_min ((λv. W *⇩v v)`𝒱) | 𝒱. B.dimensional 𝒱 (j + 1)}"
  proof-
    note 1 = bdd_above_S⇩2
    have 2: "∀y ∈ ?S⇩1. ∃x ∈ ?S⇩2. y ≤ x"
    proof clarify
      fix 𝒱 assume dim: "B.dimensional 𝒱 (j + 1)"
      define 𝒱' where "𝒱' ≡ (*⇩v) W ` 𝒱"
      have dim_𝒱': "A.dimensional 𝒱' (j + 1)" using *[OF dim[simplified], folded 𝒱'_def] by fastforce

      define x :: real where "x ≡ A.rayleigh_min 𝒱'"
      have "x ∈ ?S⇩2" unfolding x_def 𝒱'_def using dim by blast
      moreover have "B.rayleigh_min 𝒱 ≤ x"
      proof-
        have le: "⋀x. x ∈ {v. v ≠ 0⇩v n ∧ v ∈ 𝒱'} ⟹ B.rayleigh_min 𝒱 ≤ ρ A x"
        proof-
          fix x assume x: "x ∈ {v. v ≠ 0⇩v n ∧ v ∈ 𝒱'}"
          then obtain v where xv: "x = W *⇩v v" and v: "v ∈ 𝒱" and v_nz: "v ≠ 0⇩v m"
            unfolding 𝒱'_def using that isom.T0_is_0 by fastforce

          have 1: "inner_prod (W *⇩v v) (A *⇩v (W *⇩v v)) = inner_prod v ((W⇧H * A * W *⇩v v))"
          proof-
            have "inner_prod (W *⇩v v) (A *⇩v (W *⇩v v)) = inner_prod v (W⇧H *⇩v (A *⇩v (W *⇩v v)))"
              using W_dim v dim
              by (meson A_dim B.cmplx_herm_mat_axioms cscalar_prod_conjugate_transpose
                  B.dimensional_n_vec mult_mat_vec_carrier)
            also have "… = inner_prod v ((W⇧H * A * W) *⇩v v)"
              using W_dim A_dim v dim
              by (smt (verit, ccfv_SIG) B.dimensional_n_vec More_Matrix.carrier_vec_conjugate assoc_mult_mat_vec mult_carrier_mat
                  mult_mat_vec_carrier transpose_carrier_mat)
            finally show ?thesis .
          qed
          have 2: "inner_prod (W *⇩v v) (W *⇩v v) = inner_prod v v"
            using isom.preserves_norm v dim by (metis B.dimensional_n_vec inner_prod_vec_norm_pow2)
          have bdd: "bdd_below {ρ B v |v. v ≠ 0⇩v m ∧ v ∈ 𝒱}"
            using B.rayleigh_bdd_below' dim[unfolded B.dimensional_def subspace_def submodule_def]
            unfolding bdd_below_def
            by auto
          have "ρ A x = ρ A (W *⇩v v)" unfolding xv ..
          also have "… = ρ B v"
            unfolding rayleigh_quotient_def rayleigh_quotient_complex_def B_def quadratic_form_def 1 2 ..
          finally show "B.rayleigh_min 𝒱 ≤ ρ A x"
            unfolding B.rayleigh_min_def
            using v v_nz bdd
            by (metis (mono_tags, lifting) cInf_lower mem_Collect_eq)
        qed
        have ne: "{v. v ≠ 0⇩v n ∧ v ∈ 𝒱'} ≠ {}"
          using dim_𝒱'[unfolded A.dimensional_def] nontriv_subspace_exists by fastforce
        have set_rw: "{ρ A v |v. v ≠ 0⇩v n ∧ v ∈ 𝒱'} = ρ A ` {v. v ≠ 0⇩v n ∧ v ∈ 𝒱'}" by blast
        show ?thesis
          unfolding x_def A.rayleigh_min_def set_rw
          by (rule cINF_greatest[OF ne, of "B.rayleigh_min 𝒱" "λv. ρ A v"], rule le)
      qed
      ultimately show "∃x ∈ ?S⇩2. B.rayleigh_min 𝒱 ≤ x" by blast
    qed
    have 3: "?S⇩1 ≠ {}" using S⇩2_ne by blast
    show ?thesis
      apply (simp add: B.maximin_def)
      using 1 2 3 by (metis (lifting) ext Suc_eq_plus1 cSup_mono) 
  qed
  also have "… ≤ Sup {A.rayleigh_min 𝒱 | 𝒱. A.dimensional 𝒱 (j + 1)}"
    by (metis (no_types, lifting) ext S⇩2_ne S⇩2_sub_S⇩3 Suc_eq_plus1 bdd_above_S⇩3 cSup_subset_mono)
  also have "… = Re (α!j)"
    using bdd_above_S⇩3 α_def courant_fischer(2)[OF j(1), unfolded A.maximin_def] by force
  finally have "Re (β!j) ≤ Re (α!j)" .
  moreover have "α!j ∈ ℝ" using α_real α_length j(1) by fastforce
  moreover have "β!j ∈ ℝ" using β_real β_length j(2) by fastforce
  ultimately show "β!j ≤ α!j" by (simp add: complex_is_Real_iff less_eq_complex_def)
qed

theorem cauchy_eigval_interlacing:
  fixes W B :: "complex mat"
  fixes α β :: "complex list"
  fixes j m :: nat

  defines "B ≡ W⇧H * A * W"
  defines "α ≡ eigenvalues"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes j: "j < n" "j < m"
  assumes m: "0 < m" "m ≤ n"
  assumes W_dim: "W ∈ carrier_mat n m"
  assumes W_isom: "isometry_mat W n m"

  shows "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
proof-
  interpret B: cf_setup B m
    apply unfold_locales
    using A_dim A_herm W_dim B_def compression_is_hermitian
    by auto
  show "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" and lengths: "length α = n" "length β = m"
    by (rule cauchy_eigval_interlacing_aux[OF j m W_dim W_isom, folded B_def α_def β_def])+

  define A' where "A' ≡ - A"
  interpret A': cf_setup A' n
    using A_dim A_herm negative_hermitian by (unfold_locales, auto simp add: A'_def)
  define B' where "B' ≡ W⇧H * A' * W"
  have neg_B: "B' = - B" unfolding B'_def A'_def B_def using W_dim A_dim by force
  then interpret B': cf_setup B' m
    by (simp add: B.A_dim B.negative_hermitian cmplx_herm_mat.intro cf_setup.intro)
  define α' where "α' = A'.es"
  define β' where "β' ≡ B'.es"

  let ?j' = "m - j - 1"
  have j': "?j' < n" "?j' < m" using m by simp_all
  have "α!(n - m + j) = - α' ! (m - j - 1)"
    using lengths(1) m j j' neg_es[folded A'_def] by (simp add: α'_def α_def rev_nth)
  moreover have "β!j = - β' ! (m - j - 1)"
    using lengths(2) m j j' neg_es
    by (simp add: β'_def β_def B.neg_es Suc_diff_Suc neg_B rev_nth)
  ultimately show "α!(n - m + j) ≤ β!j"
    using cmplx_herm_mat.cauchy_eigval_interlacing_aux(1)
      [ OF A'.cmplx_herm_mat_axioms j' m W_dim W_isom, folded B'_def]
    unfolding β'_def α'_def A'_def B'_def
    by force
qed

subsection "Principal Submatrix Corollaries (Using @{const pick} Function)"

corollary submatrix_eigval_interlacing:
  fixes I :: "nat set"

  defines "B ≡ submatrix A I I"
  defines "m ≡ card I"
  defines "α ≡ eigenvalues"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes j: "j < m"
  assumes I: "I ⊆ {..<n}" "I ≠ {}" 

  shows "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
proof-
  obtain Q where Q: "B = Q⇧H * A * Q" "isometry_mat Q n m"
    using A_dim I B_def m_def submatrix_as_compression_obt by blast
  have Q_carrier: "Q ∈ carrier_mat n m"
    using Q(2)[unfolded isometry_mat_def mat_as_linear_map_def] ..

  interpret B: cf_setup B m
    apply unfold_locales
    using A_dim A_herm B_def Q compression_is_hermitian(2)
     apply (metis Q_carrier)
    by (simp add: I(1) B_def principal_submatrix_hermitian)

  have 1: "j < n"
    using j m_def I(1)
    by (metis atLeast0LessThan dual_order.strict_trans le_eq_less_or_eq subset_eq_atLeast0_lessThan_card)
  have 2: "0 < m" using j by linarith
  have 3: "m ≤ n"
    using I(1) m_def atLeast0LessThan subset_eq_atLeast0_lessThan_card by presburger

  show "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
    using cauchy_eigval_interlacing[OF 1 j 2 3 Q_carrier Q(2)]
    unfolding Q(1)[symmetric]
    by (simp_all add: α_def β_def)
qed

subsection "Principal Submatrix Corollary (as Injective Function on Indices)"

corollary submatrix_eigval_interlacing':
  fixes B :: "complex mat"
  fixes m :: "nat"
  fixes f :: "nat ⇒ nat"

  defines "B ≡ submatrix_of_inj A f f m m"
  defines "α ≡ eigenvalues"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes f: "f : {..<m} → {..<n}"
  assumes inj: "inj_on f {..<m}"
  assumes j: "j < m"

  shows "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
proof-
  obtain Q where Q: "B = Q⇧H * A * Q" "isometry_mat Q n m"
    using f inj α_def B_def submatrix_of_inj_as_compression_obt by (metis A_dim)
  have Q_carrier: "Q ∈ carrier_mat n m"
    using Q(2)[unfolded isometry_mat_def mat_as_linear_map_def] ..

  interpret B: cf_setup B m
    apply unfold_locales
    using A_dim A_herm B_def Q compression_is_hermitian Q_carrier
    by meson+

  note 3 = card_inj[OF f inj, simplified]
  hence 1: "j < n" using j by auto
  have 2: "0 < m" using j by linarith
  show "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
    using α_def β_def Q(1) cauchy_eigval_interlacing[OF 1 j 2 3 Q_carrier Q(2)] by fastforce+
qed

end

section "Theorem Statements (Outside Locale)"

theorem courant_fischer:
  fixes A :: "complex mat"

  defines "es ≡ cmplx_herm_mat.eigenvalues A"

  assumes carrier: "A ∈ carrier_mat n n"
  assumes herm: "hermitian A"
  assumes k: "k < n"

  shows "es!k = cf_setup.minimax A n (k + 1)"
        "es!k = cf_setup.maximin A n (k + 1)"
        "cf_setup.minimax_defined A n (k + 1)"
        "cf_setup.maximin_defined A n (k + 1)"
  by (rule cmplx_herm_mat.courant_fischer
      [OF cmplx_herm_mat.intro, OF carrier herm k, folded es_def])+

theorem cauchy_eigval_interlacing:
  fixes A W B :: "complex mat"
  fixes α β :: "complex list"
  fixes j m n :: nat

  defines "B ≡ W⇧H * A * W"
  defines "α ≡ cmplx_herm_mat.eigenvalues A"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes A: "A ∈ carrier_mat n n" "hermitian A"
  assumes j: "j < n" "j < m"
  assumes m: "0 < m" "m ≤ n"
  assumes W_dim: "W ∈ carrier_mat n m"
  assumes W_isom: "isometry_mat W n m"

  shows "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
  by (rule cmplx_herm_mat.cauchy_eigval_interlacing
      [OF cmplx_herm_mat.intro, OF A j m W_dim W_isom, folded B_def α_def β_def])+

corollary submatrix_eigval_interlacing:
  fixes A :: "complex mat"
  fixes I :: "nat set"

  defines "B ≡ submatrix A I I"
  defines "m ≡ card I"
  defines "α ≡ cmplx_herm_mat.eigenvalues A"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes A: "A ∈ carrier_mat n n" "hermitian A"
  assumes j: "j < m"
  assumes I: "I ⊆ {..<n}" "I ≠ {}" 

  shows "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
  by (rule cmplx_herm_mat.submatrix_eigval_interlacing
      [OF cmplx_herm_mat.intro, of A n j I, folded B_def m_def α_def β_def, OF A j I])+

corollary submatrix_eigval_interlacing':
  fixes A B :: "complex mat"
  fixes m :: "nat"
  fixes f :: "nat ⇒ nat"

  defines "B ≡ submatrix_of_inj A f f m m"
  defines "α ≡ cmplx_herm_mat.eigenvalues A"
  defines "β ≡ cmplx_herm_mat.eigenvalues B"

  assumes A: "A ∈ carrier_mat n n" "hermitian A"
  assumes f: "f : {..<m} → {..<n}"
  assumes inj: "inj_on f {..<m}"
  assumes j: "j < m"

  shows "α!(n - m + j) ≤ β!j" "β!j ≤ α!j" "set α ⊆ ℝ" "set β ⊆ ℝ" "length α = n" "length β = m"
  by (rule cmplx_herm_mat.submatrix_eigval_interlacing'
      [OF cmplx_herm_mat.intro, of A n f m, folded B_def α_def β_def, OF A f inj j])+

end