-
Notifications
You must be signed in to change notification settings - Fork 251
/
Orthogonal.lean
84 lines (63 loc) · 2.9 KB
/
Orthogonal.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
/-
Copyright (c) 2021 Lu-Ming Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lu-Ming Zhang
-/
import Mathlib.Data.Matrix.Basic
#align_import linear_algebra.matrix.orthogonal from "leanprover-community/mathlib"@"790e98fbb5ec433d89d833320954607e79ae9071"
/-!
# Orthogonal
This file contains definitions and properties concerning orthogonality of rows and columns.
## Main results
- `matrix.HasOrthogonalRows`:
`A.HasOrthogonalRows` means `A` has orthogonal (with respect to `dotProduct`) rows.
- `matrix.HasOrthogonalCols`:
`A.HasOrthogonalCols` means `A` has orthogonal (with respect to `dotProduct`) columns.
## Tags
orthogonal
-/
namespace Matrix
variable {α n m : Type*}
variable [Mul α] [AddCommMonoid α]
variable (A : Matrix m n α)
open Matrix
/-- `A.HasOrthogonalRows` means matrix `A` has orthogonal rows (with respect to
`Matrix.dotProduct`). -/
def HasOrthogonalRows [Fintype n] : Prop :=
∀ ⦃i₁ i₂⦄, i₁ ≠ i₂ → dotProduct (A i₁) (A i₂) = 0
#align matrix.has_orthogonal_rows Matrix.HasOrthogonalRows
/-- `A.HasOrthogonalCols` means matrix `A` has orthogonal columns (with respect to
`Matrix.dotProduct`). -/
def HasOrthogonalCols [Fintype m] : Prop :=
HasOrthogonalRows Aᵀ
#align matrix.has_orthogonal_cols Matrix.HasOrthogonalCols
/-- `Aᵀ` has orthogonal rows iff `A` has orthogonal columns. -/
@[simp]
theorem transpose_hasOrthogonalRows_iff_hasOrthogonalCols [Fintype m] :
Aᵀ.HasOrthogonalRows ↔ A.HasOrthogonalCols :=
Iff.rfl
#align matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols
/-- `Aᵀ` has orthogonal columns iff `A` has orthogonal rows. -/
@[simp]
theorem transpose_hasOrthogonalCols_iff_hasOrthogonalRows [Fintype n] :
Aᵀ.HasOrthogonalCols ↔ A.HasOrthogonalRows :=
Iff.rfl
#align matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows Matrix.transpose_hasOrthogonalCols_iff_hasOrthogonalRows
variable {A}
theorem HasOrthogonalRows.hasOrthogonalCols [Fintype m] (h : Aᵀ.HasOrthogonalRows) :
A.HasOrthogonalCols :=
h
#align matrix.has_orthogonal_rows.has_orthogonal_cols Matrix.HasOrthogonalRows.hasOrthogonalCols
theorem HasOrthogonalCols.transpose_hasOrthogonalRows [Fintype m] (h : A.HasOrthogonalCols) :
Aᵀ.HasOrthogonalRows :=
h
#align matrix.has_orthogonal_cols.transpose_has_orthogonal_rows Matrix.HasOrthogonalCols.transpose_hasOrthogonalRows
theorem HasOrthogonalCols.hasOrthogonalRows [Fintype n] (h : Aᵀ.HasOrthogonalCols) :
A.HasOrthogonalRows :=
h
#align matrix.has_orthogonal_cols.has_orthogonal_rows Matrix.HasOrthogonalCols.hasOrthogonalRows
theorem HasOrthogonalRows.transpose_hasOrthogonalCols [Fintype n] (h : A.HasOrthogonalRows) :
Aᵀ.HasOrthogonalCols :=
h
#align matrix.has_orthogonal_rows.transpose_has_orthogonal_cols Matrix.HasOrthogonalRows.transpose_hasOrthogonalCols
end Matrix