start ch 7

mo271 · Jan 2, 2024 · 742e2a7 · 742e2a7
1 parent 7ca0042
commit 742e2a7
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 2 deletions.
diff --git a/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean b/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean
@@ -44,3 +44,4 @@ import Mathlib.Tactic
       - (5)
 -/
 
+
diff --git a/FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean b/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
diff --git a/README.md b/README.md
@@ -28,7 +28,7 @@ The last step only opens vscode in case you want to use that.
 Status of the chapters:
 
   - :x: chapter is just a stub
-  - :thought_balloon: work in progress, formalization of some statements still missing
+  - thought_balloon:: work in progress, formalization of some statements still missing
   - :speech_balloon: work in progress, all statements formalized, some proofs still missing
   - :tada: chapter is completely formalized (possibly excluding the Appendix)
 
@@ -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$