feat(linear_algebra/{bilinear,quadratic}_form): remove non-degeneracy…

… requirement from `exists_orthogonal_basis` and Sylvester's law of inertia (#9465)

This removes the `nondegenerate` hypothesis from `bilin_form.exists_orthogonal_basis`, and removes the `∀ i, B (v i) (v i) ≠ 0` statement from the goal. This property can be recovered in the case of a nondegenerate form with `is_Ortho.not_is_ortho_basis_self_of_nondegenerate`.

This also swaps the order of the binders in `is_Ortho` to make it expressible with `pairwise`.

docs/undergrad.yaml

@@ -206,7 +206,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
   Orthogonality:
     orthogonal elements: 'bilin_form.is_ortho'
     adjoint endomorphism: 'bilin_form.left_adjoint_of_nondegenerate'
-    Sylvester's law of inertia: 'quadratic_form.equivalent_one_neg_one_weighted_sum_squared'
+    Sylvester's law of inertia: 'quadratic_form.equivalent_one_zero_neg_one_weighted_sum_squared'
     real classification:
     complex classification:
     Gram-Schmidt orthogonalisation:

src/linear_algebra/bilinear_form.lean

@@ -550,10 +550,10 @@ lemma ne_zero_of_not_is_ortho_self {B : bilin_form K V}
 if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use
 `bilin_form.is_ortho` -/
 def is_Ortho {n : Type w} (B : bilin_form R M) (v : n → M) : Prop :=
-∀ i j : n, i ≠ j → B.is_ortho (v j) (v i)
+pairwise (B.is_ortho on v)
 
 lemma is_Ortho_def {n : Type w} {B : bilin_form R M} {v : n → M} :
-  B.is_Ortho v ↔ ∀ i j : n, i ≠ j → B (v j) (v i) = 0 := iff.rfl
+  B.is_Ortho v ↔ ∀ i j : n, i ≠ j → B (v i) (v j) = 0 := iff.rfl
 
 section
 
@@ -597,18 +597,12 @@ begin
   intros s w hs i hi,
   have : B (s.sum $ λ (i : n), w i • v i) (v i) = 0,
   { rw [hs, zero_left] },
-  have hsum : s.sum (λ (j : n), w j * B (v j) (v i)) =
-    s.sum (λ (j : n), if i = j then w j * B (v j) (v i) else 0),
-  { refine finset.sum_congr rfl (λ j hj, _),
-    by_cases (i = j),
-    { rw [if_pos h] },
-    { rw [if_neg h, is_Ortho_def.1 hv₁ _ _ h, mul_zero] } },
-  simp_rw [sum_left, smul_left, hsum, finset.sum_ite_eq] at this,
-  rw [if_pos, mul_eq_zero] at this,
-  cases this,
-  { assumption },
-  { exact false.elim (hv₂ i $ this) },
-  { assumption }
+  have hsum : s.sum (λ (j : n), w j * B (v j) (v i)) = w i * B (v i) (v i),
+  { apply finset.sum_eq_single_of_mem i hi,
+    intros j hj hij,
+    rw [is_Ortho_def.1 hv₁ _ _ hij, mul_zero], },
+  simp_rw [sum_left, smul_left, hsum] at this,
+  exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this,
 end
 
 end
@@ -1416,6 +1410,45 @@ begin
   rwa [restrict_apply, submodule.coe_mk, submodule.coe_mk, b] at b₁
 end
 
+/-- An orthogonal basis with respect to a nondegenerate bilinear form has no self-orthogonal
+elements. -/
+lemma is_Ortho.not_is_ortho_basis_self_of_nondegenerate
+  {n : Type w} [nontrivial R] {B : bilin_form R M} {v : basis n R M}
+  (h : B.is_Ortho v) (hB : B.nondegenerate) (i : n) :
+  ¬B.is_ortho (v i) (v i) :=
+begin
+  intro ho,
+  refine v.ne_zero i (hB (v i) $ λ m, _),
+  obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m,
+  rw [basis.repr_symm_apply, finsupp.total_apply, finsupp.sum, sum_right],
+  apply finset.sum_eq_zero,
+  rintros j -,
+  rw smul_right,
+  convert mul_zero _ using 2,
+  obtain rfl | hij := eq_or_ne i j,
+  { exact ho },
+  { exact h i j hij },
+end
+
+/-- Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate
+iff the basis has no elements which are self-orthogonal. -/
+lemma is_Ortho.nondegenerate_iff_not_is_ortho_basis_self {n : Type w} [nontrivial R]
+  [no_zero_divisors R] (B : bilin_form R M) (v : basis n R M) (hO : B.is_Ortho v) :
+  B.nondegenerate ↔ ∀ i, ¬B.is_ortho (v i) (v i) :=
+begin
+  refine ⟨hO.not_is_ortho_basis_self_of_nondegenerate, λ ho m hB, _⟩,
+  obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m,
+  rw linear_equiv.map_eq_zero_iff,
+  ext i,
+  rw [finsupp.zero_apply],
+  specialize hB (v i),
+  simp_rw [basis.repr_symm_apply, finsupp.total_apply, finsupp.sum, sum_left, smul_left] at hB,
+  rw finset.sum_eq_single i at hB,
+  { exact eq_zero_of_ne_zero_of_mul_right_eq_zero (ho i) hB, },
+  { intros j hj hij, convert mul_zero _ using 2, exact hO j i hij, },
+  { intros hi, convert zero_mul _ using 2, exact finsupp.not_mem_support_iff.mp hi }
+end
+
 section
 
 lemma to_lin_restrict_ker_eq_inf_orthogonal