refactor(analysis/inner_product_space): rename is_self_adjoint to `…

…is_symmetric` and add `is_self_adjoint` (#15326)

We rename the current `inner_product_space.is_self_adjoint` to `linear_map.is_symmetric` (which states that `inner (A x) y = inner x (A y)` for all `x,y : E`) and add a new definition `is_self_adjoint` for `has_star R`. This definition is used to state theorems that were previously stated for `linear_map.is_symmetric`, but are actually about self-adjointness for `continuous_linear_map`. 
The Hellinger-Toeplitz theorem then becomes the construction of a self-adjoint operator from a symmetric operator, which is consistent with the functional analysis literature.
Moreover, since the definitions are now in the correct namespaces, we can use dot-notation. Consequently, most parts of `inner_product_space/rayleigh` and `inner_product_space/spectrum` now use `is_self_adjoint` and are also now in the `continuous_linear_map.is_self_adjoint` namespace. For the finite-dimensional case we use `is_symmetric`, since continuity is not used anywhere.
Finally, there are some minor cleanups in the matrix diagonalization file.



Co-authored-by: Moritz Doll <doll@uni-bremen.de>

docs/overview.yaml

@@ -183,7 +183,7 @@ Linear algebra:
     polar form of a quadratic: 'quadratic_form.polar'
   Finite-dimensional inner product spaces (see also Hilbert spaces, below):
     existence of orthonormal basis: 'orthonormal_basis'
-    diagonalization of self-adjoint endomorphisms: 'inner_product_space.is_self_adjoint.diagonalization_basis_apply_self_apply'
+    diagonalization of self-adjoint endomorphisms: 'linear_map.is_symmetric.diagonalization_basis_apply_self_apply'
 
 Topology:
   General topology:
@@ -267,12 +267,12 @@ Analysis:
   Hilbert spaces:
     Inner product space, over $R$ or $C$: 'inner_product_space'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
-    self-adjoint endomorphism: 'inner_product_space.is_self_adjoint'
+    self-adjoint operator: 'is_self_adjoint'
     orthogonal projection: 'orthogonal_projection'
     reflection: 'reflection'
     orthogonal complement: 'submodule.orthogonal'
     existence of Hilbert basis: 'exists_hilbert_basis'
-    eigenvalues from Rayleigh quotient: 'inner_product_space.is_self_adjoint.has_eigenvector_of_is_local_extr_on'
+    eigenvalues from Rayleigh quotient: 'is_self_adjoint.has_eigenvector_of_is_local_extr_on'
     Fréchet-Riesz representation of the dual of a Hilbert space: 'inner_product_space.to_dual'
     Lax-Milgram theorem: 'is_coercive.continuous_linear_equiv_of_bilin'
 

docs/undergrad.yaml

@@ -223,9 +223,9 @@ Bilinear and Quadratic Forms Over a Vector Space:
     unitary group: 'matrix.unitary_group'
     special orthogonal group: ''
     special unitary group: ''
-    self-adjoint endomorphism: 'inner_product_space.is_self_adjoint'
+    self-adjoint endomorphism: 'is_self_adjoint'
     normal endomorphism: 'https://en.wikipedia.org/wiki/Normal_operator'
-    diagonalization of a self-adjoint endomorphism: 'inner_product_space.is_self_adjoint.diagonalization_basis_apply_self_apply'
+    diagonalization of a self-adjoint endomorphism: 'linear_map.is_symmetric.diagonalization_basis_apply_self_apply'
     diagonalization of normal endomorphisms: 'https://en.wikipedia.org/wiki/Spectral_theorem#Normal_matrices'
     simultaneous diagonalization of two real quadratic forms, with one positive-definite: 'https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_spectral#Formalisation_alg%C3%A9brique'
     decomposition of an orthogonal transformation as a product of reflections: 'linear_isometry_equiv.reflections_generate'

src/algebra/star/module.lean

@@ -72,7 +72,7 @@ variables (R : Type*) (A : Type*)
 
 /-- The self-adjoint elements of a star module, as a submodule. -/
 def self_adjoint.submodule : submodule R A :=
-{ smul_mem' := self_adjoint.smul_mem,
+{ smul_mem' := is_self_adjoint.smul,
   ..self_adjoint A }
 
 /-- The skew-adjoint elements of a star module, as a submodule. -/

src/algebra/star/self_adjoint.lean

@@ -37,15 +37,122 @@ We also define `is_star_normal R`, a `Prop` that states that an element `x` sati
 
 -/
 
-variables (R : Type*) {A : Type*}
+variables {R A : Type*}
+
+/-- An element is self-adjoint if it is equal to its star. -/
+def is_self_adjoint [has_star R] (x : R) : Prop := star x = x
+
+/-- An element of a star monoid is normal if it commutes with its adjoint. -/
+class is_star_normal [has_mul R] [has_star R] (x : R) : Prop :=
+(star_comm_self : commute (star x) x)
+
+export is_star_normal (star_comm_self)
+
+lemma star_comm_self' [has_mul R] [has_star R] (x : R) [is_star_normal x] :
+  (star x) * x = x * star x :=
+is_star_normal.star_comm_self
+
+namespace is_self_adjoint
+
+lemma star_eq [has_star R] {x : R} (hx : is_self_adjoint x) : star x = x := hx
+
+lemma _root_.is_self_adjoint_iff [has_star R] {x : R} : is_self_adjoint x ↔ star x = x := iff.rfl
+
+section add_group
+variables [add_group R] [star_add_monoid R]
+
+variables (R)
+
+lemma _root_.is_self_adjoint_zero : is_self_adjoint (0 : R) := star_zero R
+
+variables {R}
+
+lemma add {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) : is_self_adjoint (x + y) :=
+by simp only [is_self_adjoint_iff, star_add, hx.star_eq, hy.star_eq]
+
+lemma neg {x : R} (hx : is_self_adjoint x) : is_self_adjoint (-x) :=
+by simp only [is_self_adjoint_iff, star_neg, hx.star_eq]
+
+lemma sub {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) : is_self_adjoint (x - y) :=
+by simp only [is_self_adjoint_iff, star_sub, hx.star_eq, hy.star_eq]
+
+lemma bit0 {x : R} (hx : is_self_adjoint x) : is_self_adjoint (bit0 x) :=
+by simp only [is_self_adjoint_iff, star_bit0, hx.star_eq]
+
+end add_group
+
+section non_unital_semiring
+variables [non_unital_semiring R] [star_ring R]
+
+lemma conjugate {x : R} (hx : is_self_adjoint x) (z : R) : is_self_adjoint (z * x * star z) :=
+by simp only [is_self_adjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
+
+lemma conjugate' {x : R} (hx : is_self_adjoint x) (z : R) : is_self_adjoint (star z * x * z) :=
+by simp only [is_self_adjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
+
+lemma is_star_normal {x : R} (hx : is_self_adjoint x) : is_star_normal x :=
+⟨by simp only [hx.star_eq]⟩
+
+end non_unital_semiring
+
+section ring
+variables [ring R] [star_ring R]
+
+variables (R)
+
+lemma _root_.is_self_adjoint_one : is_self_adjoint (1 : R) := star_one R
+
+variables {R}
+
+lemma bit1 {x : R} (hx : is_self_adjoint x) : is_self_adjoint (bit1 x) :=
+by simp only [is_self_adjoint_iff, star_bit1, hx.star_eq]
+
+lemma pow {x : R} (hx : is_self_adjoint x) (n : ℕ) : is_self_adjoint (x ^ n):=
+by simp only [is_self_adjoint_iff, star_pow, hx.star_eq]
+
+end ring
+
+section non_unital_comm_ring
+variables [non_unital_comm_ring R] [star_ring R]
+
+lemma mul {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) : is_self_adjoint (x * y) :=
+by simp only [is_self_adjoint_iff, star_mul', hx.star_eq, hy.star_eq]
+
+end non_unital_comm_ring
+
+section field
+variables [field R] [star_ring R]
+
+lemma inv {x : R} (hx : is_self_adjoint x) : is_self_adjoint x⁻¹ :=
+by simp only [is_self_adjoint_iff, star_inv', hx.star_eq]
+
+lemma div {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) : is_self_adjoint (x / y) :=
+by simp only [is_self_adjoint_iff, star_div', hx.star_eq, hy.star_eq]
+
+lemma zpow {x : R} (hx : is_self_adjoint x) (n : ℤ) : is_self_adjoint (x ^ n):=
+by simp only [is_self_adjoint_iff, star_zpow₀, hx.star_eq]
+
+end field
+
+section has_smul
+variables [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A]
+
+lemma smul [has_smul R A] [star_module R A] (r : R) {x : A} (hx : is_self_adjoint x) :
+  is_self_adjoint (r • x) :=
+by simp only [is_self_adjoint_iff, star_smul, star_trivial, hx.star_eq]
+
+end has_smul
+
+end is_self_adjoint
+
+variables (R)
 
 /-- The self-adjoint elements of a star additive group, as an additive subgroup. -/
 def self_adjoint [add_group R] [star_add_monoid R] : add_subgroup R :=
-{ carrier := {x | star x = x},
+{ carrier := {x | is_self_adjoint x},
   zero_mem' := star_zero R,
-  add_mem' := λ x y (hx : star x = x) (hy : star y = y),
-                show star (x + y) = x + y, by simp only [star_add x y, hx, hy],
-  neg_mem' := λ x (hx : star x = x), show star (-x) = -x, by simp only [hx, star_neg] }
+  add_mem' := λ _ _ hx, hx.add,
+  neg_mem' := λ _ hx, hx.neg }
 
 /-- The skew-adjoint elements of a star additive group, as an additive subgroup. -/
 def skew_adjoint [add_comm_group R] [star_add_monoid R] : add_subgroup R :=
@@ -57,16 +164,6 @@ def skew_adjoint [add_comm_group R] [star_add_monoid R] : add_subgroup R :=
 
 variables {R}
 
-/-- An element of a star monoid is normal if it commutes with its adjoint. -/
-class is_star_normal [has_mul R] [has_star R] (x : R) : Prop :=
-(star_comm_self : commute (star x) x)
-
-export is_star_normal (star_comm_self)
-
-lemma star_comm_self' [has_mul R] [has_star R] (x : R) [is_star_normal x] :
-  (star x) * x = x * star x :=
-is_star_normal.star_comm_self
-
 namespace self_adjoint
 
 section add_group
@@ -79,66 +176,49 @@ by { rw [←add_subgroup.mem_carrier], exact iff.rfl }
 
 instance : inhabited (self_adjoint R) := ⟨0⟩
 
-lemma bit0_mem {x : R} (hx : x ∈ self_adjoint R) : bit0 x ∈ self_adjoint R :=
-by simp only [mem_iff, star_bit0, mem_iff.mp hx]
-
 end add_group
 
 section ring
 variables [ring R] [star_ring R]
 
-instance : has_one (self_adjoint R) := ⟨⟨1, by rw [mem_iff, star_one]⟩⟩
+instance : has_one (self_adjoint R) := ⟨⟨1, is_self_adjoint_one R⟩⟩
 
 @[simp, norm_cast] lemma coe_one : ↑(1 : self_adjoint R) = (1 : R) := rfl
 
 instance [nontrivial R] : nontrivial (self_adjoint R) := ⟨⟨0, 1, subtype.ne_of_val_ne zero_ne_one⟩⟩
 
-lemma one_mem : (1 : R) ∈ self_adjoint R := by simp only [mem_iff, star_one]
-
 instance : has_nat_cast (self_adjoint R) :=
-⟨λ n, ⟨n, by induction n; simp [zero_mem, add_mem, one_mem, *]⟩⟩
+⟨λ n, ⟨n, nat.rec_on n (by simp [zero_mem])
+  (λ k hk, (@nat.cast_succ R _ k).symm ▸ add_mem hk (is_self_adjoint_one R))⟩⟩
 
 instance : has_int_cast (self_adjoint R) :=
-⟨λ n, ⟨n, by cases n; simp [add_mem, one_mem,
-  show ↑n ∈ self_adjoint R, from (n : self_adjoint R).2]⟩⟩
-
-lemma bit1_mem {x : R} (hx : x ∈ self_adjoint R) : bit1 x ∈ self_adjoint R :=
-by simp only [mem_iff, star_bit1, mem_iff.mp hx]
-
-lemma conjugate {x : R} (hx : x ∈ self_adjoint R) (z : R) : z * x * star z ∈ self_adjoint R :=
-by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, mul_assoc]
-
-lemma conjugate' {x : R} (hx : x ∈ self_adjoint R) (z : R) : star z * x * z ∈ self_adjoint R :=
-by simp only [mem_iff, star_mul, star_star, mem_iff.mp hx, mul_assoc]
-
-lemma is_star_normal_of_mem {x : R} (hx : x ∈ self_adjoint R) : is_star_normal x :=
-⟨by { simp only [mem_iff] at hx, simp only [hx] }⟩
-
-instance (x : self_adjoint R) : is_star_normal (x : R) :=
-is_star_normal_of_mem (set_like.coe_mem _)
+⟨λ n, ⟨n,
+  begin
+    cases n;
+    simp [show ↑n ∈ self_adjoint R, from (n : self_adjoint R).2],
+    refine add_mem (is_self_adjoint_one R).neg (n : self_adjoint R).2.neg,
+  end ⟩ ⟩
 
 instance : has_pow (self_adjoint R) ℕ :=
-⟨λ x n, ⟨(x : R) ^ n, by simp only [mem_iff, star_pow, star_coe_eq]⟩⟩
+⟨λ x n, ⟨(x : R) ^ n, x.prop.pow n⟩⟩
 
 @[simp, norm_cast] lemma coe_pow (x : self_adjoint R) (n : ℕ) : ↑(x ^ n) = (x : R) ^ n := rfl
 
 end ring
 
-section comm_ring
-variables [comm_ring R] [star_ring R]
-
-lemma mul_mem {x y : R} (hx : x ∈ self_adjoint R) (hy : y ∈ self_adjoint R) :
-  x * y ∈ self_adjoint R :=
-begin
-  rw mem_iff at ⊢ hx hy,
-  rw [star_mul', hx, hy]
-end
+section non_unital_comm_ring
+variables [non_unital_comm_ring R] [star_ring R]
 
 instance : has_mul (self_adjoint R) :=
-⟨λ x y, ⟨(x : R) * y, mul_mem x.prop y.prop⟩⟩
+⟨λ x y, ⟨(x : R) * y, x.prop.mul y.prop⟩⟩
 
 @[simp, norm_cast] lemma coe_mul (x y : self_adjoint R) : ↑(x * y) = (x : R) * y := rfl
 
+end non_unital_comm_ring
+
+section comm_ring
+variables [comm_ring R] [star_ring R]
+
 instance : comm_ring (self_adjoint R) :=
 function.injective.comm_ring _ subtype.coe_injective
   (self_adjoint R).coe_zero coe_one (self_adjoint R).coe_add coe_mul (self_adjoint R).coe_neg
@@ -152,17 +232,17 @@ section field
 variables [field R] [star_ring R]
 
 instance : has_inv (self_adjoint R) :=
-{ inv := λ x, ⟨(x.val)⁻¹, by simp only [mem_iff, star_inv', star_coe_eq, subtype.val_eq_coe]⟩ }
+{ inv := λ x, ⟨(x.val)⁻¹, x.prop.inv⟩ }
 
 @[simp, norm_cast] lemma coe_inv (x : self_adjoint R) : ↑(x⁻¹) = (x : R)⁻¹ := rfl
 
 instance : has_div (self_adjoint R) :=
-{ div := λ x y, ⟨x / y, by simp only [mem_iff, star_div', star_coe_eq, subtype.val_eq_coe]⟩ }
+{ div := λ x y, ⟨x / y, x.prop.div y.prop⟩ }
 
 @[simp, norm_cast] lemma coe_div (x y : self_adjoint R) : ↑(x / y) = (x / y : R) := rfl
 
 instance : has_pow (self_adjoint R) ℤ :=
-{ pow := λ x z, ⟨x ^ z, by simp only [mem_iff, star_zpow₀, star_coe_eq, subtype.val_eq_coe]⟩ }
+{ pow := λ x z, ⟨x ^ z, x.prop.zpow z⟩ }
 
 @[simp, norm_cast] lemma coe_zpow (x : self_adjoint R) (z : ℤ) : ↑(x ^ z) = (x : R) ^ z := rfl
 
@@ -177,7 +257,7 @@ instance : has_rat_cast (self_adjoint R) :=
 rfl
 
 instance has_qsmul : has_smul ℚ (self_adjoint R) :=
-⟨λ a x, ⟨a • x, by rw rat.smul_def; exact mul_mem (rat_cast_mem a) x.prop⟩⟩
+⟨λ a x, ⟨a • x, by rw rat.smul_def; exact (rat_cast_mem a).mul x.prop⟩⟩
 
 @[simp, norm_cast] lemma coe_rat_smul (x : self_adjoint R) (a : ℚ) : ↑(a • x) = a • (x : R) :=
 rfl
@@ -193,12 +273,8 @@ end field
 section has_smul
 variables [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A]
 
-lemma smul_mem [has_smul R A] [star_module R A] (r : R) {x : A}
-  (h : x ∈ self_adjoint A) : r • x ∈ self_adjoint A :=
-by rw [mem_iff, star_smul, star_trivial, mem_iff.mp h]
-
 instance [has_smul R A] [star_module R A] : has_smul R (self_adjoint A) :=
-⟨λ r x, ⟨r • x, smul_mem r x.prop⟩⟩
+⟨λ r x, ⟨r • x, x.prop.smul r⟩⟩
 
 @[simp, norm_cast] lemma coe_smul [has_smul R A] [star_module R A] (r : R) (x : self_adjoint A) :
   ↑(r • x) = r • (x : A) := rfl