start ch 7 (#44)

FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean

@@ -44,3 +44,4 @@ import Mathlib.Tactic
       - (5)
 -/
 
+

FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean

@@ -16,6 +16,8 @@ limitations under the License.
 Authors: Moritz Firsching
 -/
 import Mathlib.Tactic
+import Mathlib.Data.Matrix.Basic
+import Mathlib.LinearAlgebra.Matrix.Hermitian
 /-!
 # The spectral theorem and Hadamard's determinant problem
 
@@ -30,3 +32,19 @@ import Mathlib.Tactic
   - Hadamard matreices esixt for all $n = 2^m$
   - Theorem 2.
 -/
+
+namespace chapter07
+
+open Matrix
+
+theorem Theorem₁ (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ) (h : IsHermitian A) :
+    ∃ Q : Matrix (Fin n) (Fin n) ℝ,
+    Q ∈ Matrix.orthogonalGroup (Fin n) ℝ ∧
+    ∃ (d : (Fin n) → ℝ), diagonal d = (Q.conjTranspose * A * Q) := by
+  sorry
+
+
+theorem Theorem₂ (n : ℕ) : ∃ (M : Matrix (Fin n) (Fin n) ℤ),
+    (∀ i j, M i j = -1 ∨ M i j = 1) ∧
+    M.det > Real.sqrt n.factorial := by
+  sorry

README.md

@@ -39,7 +39,7 @@ Status of the chapters:
   4. :x: [Representing numbers as sums of two squares](./src/chapters/04_Representing_numbers_as_sums_of_two_squares.lean)
   5. :thought_balloon: [The law of quadratic reciprocity](./src/chapters/05_The_law_of_quadratic_reciprocity.lean)
   6. :thought_balloon: [Every finite division ring is a field](./src/chapters/06_Every_finite_division_ring_is_a_field.lean)
-  7. :x: [The spectral theorem and Hadamard's determinant problem](./src/chapters/07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  7. :thought_ballon: [The spectral theorem and Hadamard's determinant problem](./src/chapters/07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
   8. :thought_balloon: [Some irrational numbers](./src/chapters/08_Some_irrational_numbers.lean)
   9. :x: [Four times ](./src/chapters/09_Four_times_pi²_over_6.lean)$\pi^2/6$