fix(analysis/inner_product_space/pi_L2): add missing type cast functions (#18574)

The preferred way to convert between `ι → 𝕜` and `euclidean_space 𝕜 ι` is via `pi_Lp.equiv`, as this preserves the right typing information.

We use the local notation `⟪x, y⟫ₑ` to refer the euclidean inner product of `x y : ι → 𝕜`, which inserts the casting within the notation.

This adds a new definition `matrix.to_euclidean_lin` as a shorthand to turn a matrix into a `linear_map` over `euclidean_space`.

It also generalizes `inner_matrix_row_row` and `inner_matrix_col_col` away from `fin n` to arbitrary index types.

Author: eric-wieser

src/analysis/inner_product_space/adjoint.lean

@@ -434,14 +434,13 @@ open_locale complex_conjugate
 
 /-- The adjoint of the linear map associated to a matrix is the linear map associated to the
 conjugate transpose of that matrix. -/
-lemma conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
-  to_lin' A.conj_transpose =
-  @linear_map.adjoint _ (euclidean_space 𝕜 n) (euclidean_space 𝕜 m) _ _ _ _ _ (to_lin' A) :=
+lemma to_euclidean_lin_conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
+  A.conj_transpose.to_euclidean_lin = A.to_euclidean_lin.adjoint :=
 begin
-  rw @linear_map.eq_adjoint_iff _ (euclidean_space 𝕜 m) (euclidean_space 𝕜 n),
+  rw linear_map.eq_adjoint_iff,
   intros x y,
-  convert dot_product_assoc (conj ∘ (id x : m → 𝕜)) y A using 1,
-  simp [dot_product, mul_vec, ring_hom.map_sum,  ← star_ring_end_apply, mul_comm],
+  simp_rw [euclidean_space.inner_eq_star_dot_product, pi_Lp_equiv_to_euclidean_lin,
+    to_lin'_apply, star_mul_vec, conj_transpose_conj_transpose, dot_product_mul_vec],
 end
 
 end matrix

src/analysis/inner_product_space/pi_L2.lean

@@ -138,6 +138,9 @@ lemma finrank_euclidean_space_fin {n : ℕ} :
 lemma euclidean_space.inner_eq_star_dot_product (x y : euclidean_space 𝕜 ι) :
   ⟪x, y⟫ = matrix.dot_product (star $ pi_Lp.equiv _ _ x) (pi_Lp.equiv _ _ y) := rfl
 
+lemma euclidean_space.inner_pi_Lp_equiv_symm (x y : ι → 𝕜) :
+  ⟪(pi_Lp.equiv 2 _).symm x, (pi_Lp.equiv 2 _).symm y⟫ = matrix.dot_product (star x) y := rfl
+
 /-- A finite, mutually orthogonal family of subspaces of `E`, which span `E`, induce an isometry
 from `E` to `pi_Lp 2` of the subspaces equipped with the `L2` inner product. -/
 def direct_sum.is_internal.isometry_L2_of_orthogonal_family
@@ -815,18 +818,41 @@ section matrix
 
 open_locale matrix
 
-variables {n m : ℕ}
+variables {m n : Type*}
+
+namespace matrix
+variables [fintype m] [fintype n] [decidable_eq n]
+
+/-- `matrix.to_lin'` adapted for `euclidean_space 𝕜 _`. -/
+def to_euclidean_lin : matrix m n 𝕜 ≃ₗ[𝕜] (euclidean_space 𝕜 n →ₗ[𝕜] euclidean_space 𝕜 m) :=
+matrix.to_lin' ≪≫ₗ linear_equiv.arrow_congr
+  (pi_Lp.linear_equiv _ 𝕜 (λ _ : n, 𝕜)).symm (pi_Lp.linear_equiv _ 𝕜 (λ _ : m, 𝕜)).symm
+
+@[simp]
+lemma to_euclidean_lin_pi_Lp_equiv_symm (A : matrix m n 𝕜) (x : n → 𝕜) :
+  A.to_euclidean_lin ((pi_Lp.equiv _ _).symm x) = (pi_Lp.equiv _ _).symm (A.to_lin' x) := rfl
+
+@[simp]
+lemma pi_Lp_equiv_to_euclidean_lin (A : matrix m n 𝕜) (x : euclidean_space 𝕜 n) :
+  pi_Lp.equiv _ _ (A.to_euclidean_lin x) = A.to_lin' (pi_Lp.equiv _ _ x) := rfl
+
+/- `matrix.to_euclidean_lin` is the same as `matrix.to_lin` applied to `pi_Lp.basis_fun`, -/
+lemma to_euclidean_lin_eq_to_lin :
+  (to_euclidean_lin : matrix m n 𝕜 ≃ₗ[𝕜] _) =
+    matrix.to_lin (pi_Lp.basis_fun _ _ _) (pi_Lp.basis_fun _ _ _) := rfl
+
+end matrix
 
-local notation `⟪`x`, `y`⟫ₘ` := @inner 𝕜 (euclidean_space 𝕜 (fin m)) _ x y
-local notation `⟪`x`, `y`⟫ₙ` := @inner 𝕜 (euclidean_space 𝕜 (fin n)) _ x y
+local notation `⟪`x`, `y`⟫ₑ` := @inner 𝕜 _ _ ((pi_Lp.equiv 2 _).symm x) ((pi_Lp.equiv 2 _).symm y)
 
-/-- The inner product of a row of A and a row of B is an entry of B ⬝ Aᴴ. -/
-lemma inner_matrix_row_row (A B : matrix (fin n) (fin m) 𝕜) (i j : (fin n)) :
-  ⟪A i, B j⟫ₘ = (B ⬝ Aᴴ) j i := by {simp only [inner, matrix.mul_apply, star_ring_end_apply,
-    matrix.conj_transpose_apply,mul_comm]}
+/-- The inner product of a row of `A` and a row of `B` is an entry of `B ⬝ Aᴴ`. -/
+lemma inner_matrix_row_row [fintype n] (A B : matrix m n 𝕜) (i j : m) :
+  ⟪A i, B j⟫ₑ = (B ⬝ Aᴴ) j i :=
+by simp_rw [euclidean_space.inner_pi_Lp_equiv_symm, matrix.mul_apply', matrix.dot_product_comm,
+  matrix.conj_transpose_apply, pi.star_def]
 
-/-- The inner product of a column of A and a column of B is an entry of Aᴴ ⬝ B -/
-lemma inner_matrix_col_col (A B : matrix (fin n) (fin m) 𝕜) (i j : (fin m)) :
-  ⟪Aᵀ i, Bᵀ j⟫ₙ = (Aᴴ ⬝ B) i j := rfl
+/-- The inner product of a column of `A` and a column of `B` is an entry of `Aᴴ ⬝ B`. -/
+lemma inner_matrix_col_col [fintype m] (A B : matrix m n 𝕜) (i j : n) :
+  ⟪Aᵀ i, Bᵀ j⟫ₑ = (Aᴴ ⬝ B) i j := rfl
 
 end matrix

src/linear_algebra/matrix/hermitian.lean

@@ -25,7 +25,7 @@ variables {α β : Type*} {m n : Type*} {A : matrix n n α}
 
 open_locale matrix
 
-local notation `⟪`x`, `y`⟫` := @inner α (pi_Lp 2 (λ (_ : n), α)) _ x y
+local notation `⟪`x`, `y`⟫` := @inner α _ _ x y
 
 section non_unital_semiring
 
@@ -200,14 +200,11 @@ funext h.coe_re_apply_self
 
 /-- A matrix is hermitian iff the corresponding linear map is self adjoint. -/
 lemma is_hermitian_iff_is_symmetric [fintype n] [decidable_eq n] {A : matrix n n α} :
-  is_hermitian A ↔ linear_map.is_symmetric
-    ((pi_Lp.linear_equiv 2 α (λ _ : n, α)).symm.conj A.to_lin' : module.End α (pi_Lp 2 _)) :=
+  is_hermitian A ↔ A.to_euclidean_lin.is_symmetric :=
 begin
   rw [linear_map.is_symmetric, (pi_Lp.equiv 2 (λ _ : n, α)).symm.surjective.forall₂],
-  simp only [linear_equiv.conj_apply, linear_map.comp_apply, linear_equiv.coe_coe,
-    pi_Lp.linear_equiv_apply, pi_Lp.linear_equiv_symm_apply, linear_equiv.symm_symm],
-  simp_rw [euclidean_space.inner_eq_star_dot_product, equiv.apply_symm_apply, to_lin'_apply,
-    star_mul_vec, dot_product_mul_vec],
+  simp only [to_euclidean_lin_pi_Lp_equiv_symm, euclidean_space.inner_pi_Lp_equiv_symm,
+    to_lin'_apply, star_mul_vec, dot_product_mul_vec],
   split,
   { rintro (h : Aᴴ = A) x y,
     rw h },

src/linear_algebra/matrix/ldl.lean

@@ -30,8 +30,7 @@ decomposed as `S = LDLᴴ` where `L` is a lower-triangular matrix and `D` is a d
 variables {𝕜 : Type*} [is_R_or_C 𝕜]
 variables {n : Type*} [linear_order n] [is_well_order n (<)] [locally_finite_order_bot n]
 
-local notation `⟪`x`, `y`⟫` :=
-@inner 𝕜 (n → 𝕜) (pi_Lp.inner_product_space (λ _, 𝕜)).to_has_inner x y
+local notation `⟪`x`, `y`⟫ₑ` := @inner 𝕜 _ _ ((pi_Lp.equiv 2 _).symm x) ((pi_Lp.equiv _ _).symm y)
 
 open matrix
 open_locale matrix
@@ -42,7 +41,7 @@ applying Gram-Schmidt-Orthogonalization w.r.t. the inner product induced by `S
 basis vectors `pi.basis_fun`. -/
 noncomputable def LDL.lower_inv : matrix n n 𝕜 :=
 @gram_schmidt
-  𝕜 (n → 𝕜) _ (inner_product_space.of_matrix hS.transpose) n _ _ _ (λ k, pi.basis_fun 𝕜 n k)
+  𝕜 (n → 𝕜) _ (inner_product_space.of_matrix hS.transpose) n _ _ _ (pi.basis_fun 𝕜 n)
 
 lemma LDL.lower_inv_eq_gram_schmidt_basis :
   LDL.lower_inv hS = ((pi.basis_fun 𝕜 n).to_matrix
@@ -64,15 +63,15 @@ begin
 end
 
 lemma LDL.lower_inv_orthogonal {i j : n} (h₀ : i ≠ j) :
-  ⟪(LDL.lower_inv hS i), Sᵀ.mul_vec (LDL.lower_inv hS j)⟫ = 0 :=
+  ⟪(LDL.lower_inv hS i), Sᵀ.mul_vec (LDL.lower_inv hS j)⟫ₑ = 0 :=
 show @inner 𝕜 (n → 𝕜) (inner_product_space.of_matrix hS.transpose).to_has_inner
     (LDL.lower_inv hS i)
     (LDL.lower_inv hS j) = 0,
 by apply gram_schmidt_orthogonal _ _ h₀
 
 /-- The entries of the diagonal matrix `D` of the LDL decomposition. -/
 noncomputable def LDL.diag_entries : n → 𝕜 :=
-  λ i, ⟪star (LDL.lower_inv hS i), S.mul_vec (star (LDL.lower_inv hS i))⟫
+λ i, ⟪star (LDL.lower_inv hS i), S.mul_vec (star (LDL.lower_inv hS i))⟫ₑ
 
 /-- The diagonal matrix `D` of the LDL decomposition. -/
 noncomputable def LDL.diag : matrix n n 𝕜 := matrix.diagonal (LDL.diag_entries hS)
@@ -88,12 +87,12 @@ lemma LDL.diag_eq_lower_inv_conj : LDL.diag hS = LDL.lower_inv hS ⬝ S ⬝ (LDL
 begin
   ext i j,
   by_cases hij : i = j,
-  { simpa only [hij, LDL.diag, diagonal_apply_eq, LDL.diag_entries, matrix.mul_assoc, inner,
-      pi.star_apply, is_R_or_C.star_def, star_ring_end_self_apply] },
+  { simpa only [hij, LDL.diag, diagonal_apply_eq, LDL.diag_entries, matrix.mul_assoc,
+      euclidean_space.inner_pi_Lp_equiv_symm, star_star] },
   { simp only [LDL.diag, hij, diagonal_apply_ne, ne.def, not_false_iff, mul_mul_apply],
     rw [conj_transpose, transpose_map, transpose_transpose, dot_product_mul_vec,
       (LDL.lower_inv_orthogonal hS (λ h : j = i, hij h.symm)).symm,
-      ← inner_conj_symm, mul_vec_transpose, euclidean_space.inner_eq_star_dot_product,
+      ← inner_conj_symm, mul_vec_transpose, euclidean_space.inner_pi_Lp_equiv_symm,
       ← is_R_or_C.star_def, ← star_dot_product_star, dot_product_comm, star_star],
     refl }
 end

src/linear_algebra/matrix/spectrum.lean

@@ -90,18 +90,14 @@ theorem spectral_theorem :
 begin
   rw [eigenvector_matrix_inv, pi_Lp.basis_to_matrix_basis_fun_mul],
   ext i j,
-  have : linear_map.is_symmetric _ := is_hermitian_iff_is_symmetric.1 hA,
+  have := is_hermitian_iff_is_symmetric.1 hA,
   convert this.diagonalization_basis_apply_self_apply finrank_euclidean_space
     (euclidean_space.single j 1)
-    ((fintype.equiv_of_card_eq (fintype.card_fin _)).symm i),
-  { dsimp only [linear_equiv.conj_apply_apply, pi_Lp.linear_equiv_apply,
-      pi_Lp.linear_equiv_symm_apply, pi_Lp.equiv_single, linear_map.std_basis,
-      linear_map.coe_single, pi_Lp.equiv_symm_single, linear_equiv.symm_symm,
-      eigenvector_basis, to_lin'_apply],
-    simp only [basis.to_matrix, basis.coe_to_orthonormal_basis_repr, basis.equiv_fun_apply],
-    simp_rw [orthonormal_basis.coe_to_basis_repr_apply, orthonormal_basis.repr_reindex,
-      linear_equiv.symm_symm, pi_Lp.linear_equiv_apply, pi_Lp.equiv_single, mul_vec_single,
-      mul_one],
+    ((fintype.equiv_of_card_eq (fintype.card_fin _)).symm i) using 1,
+  { dsimp only [euclidean_space.single, to_euclidean_lin_pi_Lp_equiv_symm, to_lin'_apply,
+      matrix.of_apply, is_hermitian.eigenvector_basis],
+    simp_rw [mul_vec_single, mul_one, orthonormal_basis.coe_to_basis_repr_apply,
+      orthonormal_basis.repr_reindex],
     refl },
   { simp only [diagonal_mul, (∘), eigenvalues, eigenvector_basis],
     rw [basis.to_matrix_apply,