feat(linear_algebra/eigenspace): add generalized eigenspaces (#4015)

Add the definition of generalized eigenspaces, eigenvectors and eigenvalues. Add some basic lemmas about them.

Another step towards #3864.

Author: abentkamp

src/algebra/group_power.lean

@@ -69,12 +69,16 @@ namespace commute
 variables [monoid M] {a b : M}
 
 @[simp] theorem pow_right (h : commute a b) (n : ℕ) : commute a (b ^ n) := h.pow_right n
+
 @[simp] theorem pow_left (h : commute a b) (n : ℕ) : commute (a ^ n) b := (h.symm.pow_right n).symm
+
 @[simp] theorem pow_pow (h : commute a b) (m n : ℕ) : commute (a ^ m) (b ^ n) :=
 (h.pow_left m).pow_right n
 
 @[simp] theorem self_pow (a : M) (n : ℕ) : commute a (a ^ n) := (commute.refl a).pow_right n
+
 @[simp] theorem pow_self (a : M) (n : ℕ) : commute (a ^ n) a := (commute.refl a).pow_left n
+
 @[simp] theorem pow_pow_self (a : M) (m n : ℕ) : commute (a ^ m) (a ^ n) :=
 (commute.refl a).pow_pow m n
 
@@ -87,12 +91,15 @@ section monoid
 variables [monoid M] [monoid N] [add_monoid A] [add_monoid B]
 
 @[simp] theorem pow_zero (a : M) : a^0 = 1 := rfl
+
 @[simp] theorem zero_nsmul (a : A) : 0 •ℕ a = 0 := rfl
 
 theorem pow_succ (a : M) (n : ℕ) : a^(n+1) = a * a^n := rfl
+
 theorem succ_nsmul (a : A) (n : ℕ) : (n+1) •ℕ a = a + n •ℕ a := rfl
 
 @[simp] theorem pow_one (a : M) : a^1 = a := mul_one _
+
 @[simp] theorem one_nsmul (a : A) : 1 •ℕ a = a := add_zero _
 
 @[simp] lemma pow_ite (P : Prop) [decidable P] (a : M) (b c : ℕ) :
@@ -108,55 +115,77 @@ by split_ifs; refl
 by simp
 
 theorem pow_mul_comm' (a : M) (n : ℕ) : a^n * a = a * a^n := commute.pow_self a n
+
 theorem nsmul_add_comm' : ∀ (a : A) (n : ℕ), n •ℕ a + a = a + n •ℕ a :=
 @pow_mul_comm' (multiplicative A) _
 
 theorem pow_succ' (a : M) (n : ℕ) : a^(n+1) = a^n * a :=
 by rw [pow_succ, pow_mul_comm']
+
 theorem succ_nsmul' (a : A) (n : ℕ) : (n+1) •ℕ a = n •ℕ a + a :=
 @pow_succ' (multiplicative A) _ _ _
 
 theorem pow_two (a : M) : a^2 = a * a :=
 show a*(a*1)=a*a, by rw mul_one
+
 theorem two_nsmul (a : A) : 2 •ℕ a = a + a :=
 @pow_two (multiplicative A) _ a
 
 theorem pow_add (a : M) (m n : ℕ) : a^(m + n) = a^m * a^n :=
 by induction n with n ih; [rw [add_zero, pow_zero, mul_one],
   rw [pow_succ', ← mul_assoc, ← ih, ← pow_succ', add_assoc]]
+
 theorem add_nsmul : ∀ (a : A) (m n : ℕ), (m + n) •ℕ a = m •ℕ a + n •ℕ a :=
 @pow_add (multiplicative A) _
 
 @[simp] theorem one_pow (n : ℕ) : (1 : M)^n = 1 :=
 by induction n with n ih; [refl, rw [pow_succ, ih, one_mul]]
+
 @[simp] theorem nsmul_zero (n : ℕ) : n •ℕ (0 : A) = 0 :=
 by induction n with n ih; [refl, rw [succ_nsmul, ih, zero_add]]
 
 theorem pow_mul (a : M) (m n : ℕ) : a^(m * n) = (a^m)^n :=
 by induction n with n ih; [rw mul_zero, rw [nat.mul_succ, pow_add, pow_succ', ih]]; refl
+
 theorem mul_nsmul' : ∀ (a : A) (m n : ℕ), m * n •ℕ a = n •ℕ (m •ℕ a) :=
 @pow_mul (multiplicative A) _
 
 theorem pow_mul' (a : M) (m n : ℕ) : a^(m * n) = (a^n)^m :=
 by rw [mul_comm, pow_mul]
+
 theorem mul_nsmul (a : A) (m n : ℕ) : m * n •ℕ a = m •ℕ (n •ℕ a) :=
 @pow_mul' (multiplicative A) _ a m n
 
+theorem pow_mul_pow_sub (a : M) {m n : ℕ} (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n :=
+by rw [←pow_add, nat.add_sub_cancel' h]
+
+theorem nsmul_add_sub_nsmul (a : A) {m n : ℕ} (h : m ≤ n) : (m •ℕ a) + ((n - m) •ℕ a) = n •ℕ a :=
+@pow_mul_pow_sub (multiplicative A) _ _ _ _ h
+
+theorem pow_sub_mul_pow (a : M) {m n : ℕ} (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n :=
+by rw [←pow_add, nat.sub_add_cancel h]
+
+theorem sub_nsmul_nsmul_add (a : A) {m n : ℕ} (h : m ≤ n) : ((n - m) •ℕ a) + (m •ℕ a) = n •ℕ a :=
+@pow_sub_mul_pow (multiplicative A) _ _ _ _ h
+
 @[simp] theorem nsmul_one [has_one A] : ∀ n : ℕ, n •ℕ (1 : A) = n :=
 add_monoid_hom.eq_nat_cast
   ⟨λ n, n •ℕ (1 : A), zero_nsmul _, λ _ _, add_nsmul _ _ _⟩
   (one_nsmul _)
 
 theorem pow_bit0 (a : M) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
+
 theorem bit0_nsmul (a : A) (n : ℕ) : bit0 n •ℕ a = n •ℕ a + n •ℕ a := add_nsmul _ _ _
 
 theorem pow_bit1 (a : M) (n : ℕ) : a ^ bit1 n = a^n * a^n * a :=
 by rw [bit1, pow_succ', pow_bit0]
+
 theorem bit1_nsmul : ∀ (a : A) (n : ℕ), bit1 n •ℕ a = n •ℕ a + n •ℕ a + a :=
 @pow_bit1 (multiplicative A) _
 
 theorem pow_mul_comm (a : M) (m n : ℕ) : a^m * a^n = a^n * a^m :=
 commute.pow_pow_self a m n
+
 theorem nsmul_add_comm : ∀ (a : A) (m n : ℕ), m •ℕ a + n •ℕ a = n •ℕ a + m •ℕ a :=
 @pow_mul_comm (multiplicative A) _
 
@@ -167,6 +196,7 @@ begin
   { refl },
   { rw [list.repeat_succ, list.prod_cons, ih], refl, }
 end
+
 @[simp, priority 500]
 theorem list.sum_repeat : ∀ (a : A) (n : ℕ), (list.repeat a n).sum = n •ℕ a :=
 @list.prod_repeat (multiplicative A) _
@@ -215,6 +245,7 @@ variables [comm_monoid M] [add_comm_monoid A]
 
 theorem mul_pow (a b : M) (n : ℕ) : (a * b)^n = a^n * b^n :=
 (commute.all a b).mul_pow n
+
 theorem nsmul_add : ∀ (a b : A) (n : ℕ), n •ℕ (a + b) = n •ℕ a + n •ℕ b :=
 @mul_pow (multiplicative A) _
 
@@ -239,18 +270,21 @@ section nat
 @[simp] theorem inv_pow (a : G) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=
 by induction n with n ih; [exact one_inv.symm,
   rw [pow_succ', pow_succ, ih, mul_inv_rev]]
+
 @[simp] theorem neg_nsmul : ∀ (a : A) (n : ℕ), n •ℕ (-a) = -(n •ℕ a) :=
 @inv_pow (multiplicative A) _
 
 theorem pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
 have h1 : m - n + n = m, from nat.sub_add_cancel h,
 have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
 eq_mul_inv_of_mul_eq h2
+
 theorem nsmul_sub : ∀ (a : A) {m n : ℕ}, n ≤ m → (m - n) •ℕ a = m •ℕ a - n •ℕ a :=
 @pow_sub (multiplicative A) _
 
 theorem pow_inv_comm (a : G) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
 (commute.refl a).inv_left.pow_pow m n
+
 theorem nsmul_neg_comm : ∀ (a : A) (m n : ℕ), m •ℕ (-a) + n •ℕ a = n •ℕ a + m •ℕ (-a) :=
 @pow_inv_comm (multiplicative A) _
 end nat
@@ -278,26 +312,32 @@ def gsmul (n : ℤ) (a : A) : A :=
 infix ` •ℤ `:70 := gsmul
 
 @[simp] theorem gpow_coe_nat (a : G) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl
+
 @[simp] theorem gsmul_coe_nat (a : A) (n : ℕ) : n •ℤ a = n •ℕ a := rfl
 
 theorem gpow_of_nat (a : G) (n : ℕ) : a ^ of_nat n = a ^ n := rfl
+
 theorem gsmul_of_nat (a : A) (n : ℕ) : of_nat n •ℤ a = n •ℕ a := rfl
 
 @[simp] theorem gpow_neg_succ_of_nat (a : G) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl
+
 @[simp] theorem gsmul_neg_succ_of_nat (a : A) (n : ℕ) : -[1+n] •ℤ a = - (n.succ •ℕ a) := rfl
 
 local attribute [ematch] le_of_lt
 open nat
 
 @[simp] theorem gpow_zero (a : G) : a ^ (0:ℤ) = 1 := rfl
+
 @[simp] theorem zero_gsmul (a : A) : (0:ℤ) •ℤ a = 0 := rfl
 
 @[simp] theorem gpow_one (a : G) : a ^ (1:ℤ) = a := pow_one a
+
 @[simp] theorem one_gsmul (a : A) : (1:ℤ) •ℤ a = a := add_zero _
 
 @[simp] theorem one_gpow : ∀ (n : ℤ), (1 : G) ^ n = 1
 | (n : ℕ) := one_pow _
 | -[1+ n] := show _⁻¹=(1:G), by rw [_root_.one_pow, one_inv]
+
 @[simp] theorem gsmul_zero : ∀ (n : ℤ), n •ℤ (0 : A) = 0 :=
 @one_gpow (multiplicative A) _
 
@@ -313,6 +353,7 @@ by simp only [mul_inv_rev, gpow_one, gpow_neg]
 @gpow_neg (multiplicative A) _
 
 theorem gpow_neg_one (x : G) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x
+
 theorem neg_one_gsmul (x : A) : (-1:ℤ) •ℤ x = -x := congr_arg has_neg.neg $ one_nsmul x
 
 theorem gsmul_one [has_one A] (n : ℤ) : n •ℤ (1 : A) = n :=
@@ -321,6 +362,7 @@ by cases n; simp
 theorem inv_gpow (a : G) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
 | (n : ℕ) := inv_pow a n
 | -[1+ n] := congr_arg has_inv.inv $ inv_pow a (n+1)
+
 theorem gsmul_neg (a : A) (n : ℤ) : gsmul n (- a) = - gsmul n a :=
 @inv_gpow (multiplicative A) _ a n
 
@@ -363,11 +405,13 @@ lemma sub_gsmul (m n : ℤ) (a : A) : (m - n) •ℤ a = m •ℤ a - n •ℤ a
 
 theorem gpow_one_add (a : G) (i : ℤ) : a ^ (1 + i) = a * a ^ i :=
 by rw [gpow_add, gpow_one]
+
 theorem one_add_gsmul : ∀ (a : A) (i : ℤ), (1 + i) •ℤ a = a + i •ℤ a :=
 @gpow_one_add (multiplicative A) _
 
 theorem gpow_mul_comm (a : G) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i :=
 by rw [← gpow_add, ← gpow_add, add_comm]
+
 theorem gsmul_add_comm : ∀ (a : A) (i j), i •ℤ a + j •ℤ a = j •ℤ a + i •ℤ a :=
 @gpow_mul_comm (multiplicative A) _
 
@@ -380,14 +424,17 @@ theorem gsmul_mul' : ∀ (a : A) (m n : ℤ), m * n •ℤ a = n •ℤ (m •
 
 theorem gpow_mul' (a : G) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
 by rw [mul_comm, gpow_mul]
+
 theorem gsmul_mul (a : A) (m n : ℤ) : m * n •ℤ a = m •ℤ (n •ℤ a) :=
 by rw [mul_comm, gsmul_mul']
 
 theorem gpow_bit0 (a : G) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := gpow_add _ _ _
+
 theorem bit0_gsmul (a : A) (n : ℤ) : bit0 n •ℤ a = n •ℤ a + n •ℤ a := gpow_add _ _ _
 
 theorem gpow_bit1 (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a :=
 by rw [bit1, gpow_add]; simp [gpow_bit0]
+
 theorem bit1_gsmul : ∀ (a : A) (n : ℤ), bit1 n •ℤ a = n •ℤ a + n •ℤ a + a :=
 @gpow_bit1 (multiplicative A) _
 

src/linear_algebra/eigenspace.lean

@@ -10,15 +10,21 @@ import linear_algebra.finsupp
 /-!
 # Eigenvectors and eigenvalues
 
-This file defines eigenspaces and eigenvalues.
+This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized
+counterparts.
 
 An eigenspace of a linear map `f` for a scalar `μ` is the kernel of the map `(f - μ • id)`. The
 nonzero elements of an eigenspace are eigenvectors `x`. They have the property `f x = μ • x`. If
 there are eigenvectors for a scalar `μ`, the scalar `μ` is called an eigenvalue.
 
 There is no consensus in the literature whether `0` is an eigenvector. Our definition of
-`eigenvector` permits only nonzero vectors. For an eigenvector `x` that may also be `0`, we write
-`x ∈ eigenspace f μ`.
+`has_eigenvector` permits only nonzero vectors. For an eigenvector `x` that may also be `0`, we
+write `x ∈ f.eigenspace μ`.
+
+A generalized eigenspace of a linear map `f` for a natural number `k` and a scalar `μ` is the kernel
+of the map `(f - μ • id) ^ k`. The nonzero elements of a generalized eigenspace are generalized
+eigenvectors `x`. If there are generalized eigenvectors for a natural number `k` and a scalar `μ`,
+the scalar `μ` is called a generalized eigenvalue.
 
 ## Notations
 
@@ -242,5 +248,68 @@ begin
       exact h_lμ_eq_0 μ h_cases } }
 end
 
+/-- The generalized eigenspace for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the
+    kernel of `(f - μ • id) ^ k`. -/
+def generalized_eigenspace [comm_ring K] [module K V]
+  (f : End K V) (μ : K) (k : ℕ) : submodule K V :=
+((f - am μ) ^ k).ker
+
+/-- A nonzero element of a generalized eigenspace is a generalized eigenvector. -/
+def has_generalized_eigenvector [comm_ring K] [module K V]
+  (f : End K V) (μ : K) (k : ℕ) (x : V) : Prop :=
+x ≠ 0 ∧ x ∈ generalized_eigenspace f μ k
+
+/-- A scalar `μ` is a generalized eigenvalue for a linear map `f` and an exponent `k ∈ ℕ` if there
+    are generalized eigenvectors for `f`, `k`, and `μ`. -/
+def has_generalized_eigenvalue [comm_ring K] [module K V]
+  (f : End K V) (μ : K) (k : ℕ) : Prop :=
+generalized_eigenspace f μ k ≠ ⊥
+
+/-- The exponent of a generalized eigenvalue is never 0. -/
+lemma exp_ne_zero_of_has_generalized_eigenvalue [comm_ring K] [module K V]
+  {f : End K V} {μ : K} {k : ℕ} (h : f.has_generalized_eigenvalue μ k) :
+  k ≠ 0 :=
+begin
+  rintro rfl,
+  exact h linear_map.ker_id
+end
+
+/-- A generalized eigenspace for some exponent `k` is contained in
+    the generalized eigenspace for exponents larger than `k`. -/
+lemma generalized_eigenspace_mono [field K] [vector_space K V]
+  {f : End K V} {μ : K} {k : ℕ} {m : ℕ} (hm : k ≤ m) :
+  f.generalized_eigenspace μ k ≤ f.generalized_eigenspace μ m :=
+begin
+  simp only [generalized_eigenspace, ←pow_sub_mul_pow _ hm],
+  exact linear_map.ker_le_ker_comp ((f - am μ) ^ k) ((f - am μ) ^ (m - k))
+end
+
+/-- A generalized eigenvalue for some exponent `k` is also
+    a generalized eigenvalue for exponents larger than `k`. -/
+lemma has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le [field K] [vector_space K V]
+  {f : End K V} {μ : K} {k : ℕ} {m : ℕ} (hm : k ≤ m) (hk : f.has_generalized_eigenvalue μ k) :
+  f.has_generalized_eigenvalue μ m :=
+begin
+  unfold has_generalized_eigenvalue at *,
+  contrapose! hk,
+  rw [←le_bot_iff, ←hk],
+  exact generalized_eigenspace_mono hm
+end
+
+/-- The eigenspace is a subspace of the generalized eigenspace. -/
+lemma eigenspace_le_generalized_eigenspace [field K] [vector_space K V]
+  {f : End K V} {μ : K} {k : ℕ} (hk : 0 < k) :
+  f.eigenspace μ ≤ f.generalized_eigenspace μ k :=
+generalized_eigenspace_mono (nat.succ_le_of_lt hk)
+
+/-- All eigenvalues are generalized eigenvalues. -/
+lemma has_generalized_eigenvalue_of_has_eigenvalue [field K] [vector_space K V]
+  {f : End K V} {μ : K} {k : ℕ} (hk : 0 < k) (hμ : f.has_eigenvalue μ) :
+  f.has_generalized_eigenvalue μ k :=
+begin
+  apply has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le hk,
+  rwa [has_generalized_eigenvalue, generalized_eigenspace, pow_one]
+end
+
 end End
 end module