[Merged by Bors] - refactor(QuadraticForm/Real): migrate to SignType

Mathlib/Data/Sign.lean

@@ -146,14 +146,12 @@ def fin3Equiv : SignType ≃* Fin 3 where
     | ⟨0, _⟩ => 0
     | ⟨1, _⟩ => 1
     | ⟨2, _⟩ => -1
-    | ⟨n + 3, h⟩ => (h.not_le le_add_self).elim
   left_inv a := by cases a <;> rfl
   right_inv a :=
     match a with
     | ⟨0, _⟩ => by simp
     | ⟨1, _⟩ => by simp
     | ⟨2, _⟩ => by simp
-    | ⟨n + 3, h⟩ => by simp at h
   map_mul' a b := by
     cases a <;> cases b <;> rfl
 #align sign_type.fin3_equiv SignType.fin3Equiv
@@ -430,16 +428,18 @@ theorem sign_mul (x y : α) : sign (x * y) = sign x * sign y := by
 #align sign_mul sign_mul
 
 @[simp] theorem sign_mul_abs (x : α) : (sign x * |x| : α) = x := by
-  rcases lt_trichotomy x 0 with (hx | rfl | hx)
-  · rw [sign_neg hx, abs_of_neg hx, coe_neg_one, neg_one_mul, neg_neg]
-  · rw [abs_zero, mul_zero]
-  · rw [sign_pos hx, abs_of_pos hx, coe_one, one_mul]
+  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]
 
 @[simp] theorem abs_mul_sign (x : α) : (|x| * sign x : α) = x := by
-  rcases lt_trichotomy x 0 with (hx | rfl | hx)
-  · rw [sign_neg hx, abs_of_neg hx, coe_neg_one, mul_neg_one, neg_neg]
-  · rw [abs_zero, zero_mul]
-  · rw [sign_pos hx, abs_of_pos hx, coe_one, mul_one]
+  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]
+
+@[simp]
+theorem sign_mul_self (x : α) : sign x * x = |x| := by
+  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]
+
+@[simp]
+theorem self_mul_sign (x : α) : x * sign x = |x| := by
+  rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]
 
 /-- `SignType.sign` as a `MonoidWithZeroHom` for a nontrivial ordered semiring. Note that linearity
 is required; consider ℂ with the order `z ≤ w` iff they have the same imaginary part and

Mathlib/LinearAlgebra/QuadraticForm/Real.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Kexing Ying, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
-import Mathlib.Analysis.SpecialFunctions.Pow.Real
-import Mathlib.Data.Real.Sign
+import Mathlib.Data.Sign
+import Mathlib.Algebra.CharP.Invertible
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.Abs
 
 #align_import linear_algebra.quadratic_form.real from "leanprover-community/mathlib"@"0b9eaaa7686280fad8cce467f5c3c57ee6ce77f8"
 
@@ -26,73 +28,67 @@ namespace QuadraticForm
 
 open scoped BigOperators
 
-open Real Finset
+open Finset SignType
 
 variable {ι : Type*} [Fintype ι]
 
 /-- The isometry between a weighted sum of squares with weights `u` on the
 (non-zero) real numbers and the weighted sum of squares with weights `sign ∘ u`. -/
 noncomputable def isometryEquivSignWeightedSumSquares (w : ι → ℝ) :
-    IsometryEquiv (weightedSumSquares ℝ w) (weightedSumSquares ℝ (Real.sign ∘ w)) := by
+    IsometryEquiv (weightedSumSquares ℝ w)
+      (weightedSumSquares ℝ (fun i ↦ (sign (w i) : ℝ))) := by
   let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h
-  have hu' : ∀ i : ι, (Real.sign (u i) * u i) ^ (-(1 / 2 : ℝ)) ≠ 0 := by
-    intro i
-    exact (ne_of_lt (Real.rpow_pos_of_pos (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _) _)).symm
-  convert
-    (weightedSumSquares ℝ w).isometryEquivBasisRepr
-      ((Pi.basisFun ℝ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hu' i).unit)
+  have hu : ∀ i : ι, 1 / √|(u i : ℝ)| ≠ 0 := fun i ↦
+    have : (u i : ℝ) ≠ 0 := (u i).ne_zero
+    by positivity
+  have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by
+    by_cases hi : w i = 0 <;> field_simp [hi, u]
+  convert (weightedSumSquares ℝ w).isometryEquivBasisRepr
+    ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i))
   ext1 v
-  rw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]
-  refine' sum_congr rfl fun j hj => _
-  have hsum :
-    (∑ i : ι, v i • ((isUnit_iff_ne_zero.2 <| hu' i).unit : ℝ) • (Pi.basisFun ℝ ι) i) j =
-      v j • (Real.sign (u j) * u j) ^ (-(1 / 2 : ℝ)) := by
-    classical
-    rw [Finset.sum_apply, sum_eq_single j, Pi.basisFun_apply, IsUnit.unit_spec,
-      LinearMap.stdBasis_apply, Pi.smul_apply, Pi.smul_apply, Function.update_same, smul_eq_mul,
-      smul_eq_mul, smul_eq_mul, mul_one]
-    intro i _ hij
-    rw [Pi.basisFun_apply, LinearMap.stdBasis_apply, Pi.smul_apply, Pi.smul_apply,
-      Function.update_noteq hij.symm, Pi.zero_apply, smul_eq_mul, smul_eq_mul,
-      mul_zero, mul_zero]
-    intro hj'; exact False.elim (hj' hj)
-  simp_rw [Basis.unitsSMul_apply]
-  erw [hsum]
-  simp only [u, Function.comp, smul_eq_mul]
-  split_ifs with h
-  · simp only [h, zero_smul, zero_mul, Real.sign_zero]
-  have hwu : w j = u j := by simp only [u, dif_neg h, Units.val_mk0]
-  simp only [Units.val_mk0]
-  rw [hwu]
-  suffices (u j : ℝ).sign * v j * v j =
-      (Real.sign (u j) * u j) ^ (-(1 / 2 : ℝ)) * (Real.sign (u j) * u j) ^ (-(1 / 2 : ℝ)) *
-            u j * v j * v j by
-    erw [← mul_assoc, this]; ring
-  rw [← Real.rpow_add (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _),
-    show -(1 / 2 : ℝ) + -(1 / 2) = -1 by ring, Real.rpow_neg_one, mul_inv, inv_sign,
-    mul_assoc (Real.sign (u j)) (u j)⁻¹, inv_mul_cancel (Units.ne_zero _), mul_one]
+  classical
+  suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
+    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu]
+  exact sum_congr rfl fun j _ ↦ by ring
 #align quadratic_form.isometry_sign_weighted_sum_squares QuadraticForm.isometryEquivSignWeightedSumSquares
 
+/-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted
+sum of squares with the weights being ±1, `SignType` version. -/
+theorem equivalent_sign_ne_zero_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
+    [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) :
+    ∃ w : Fin (FiniteDimensional.finrank ℝ M) → SignType,
+      (∀ i, w i ≠ 0) ∧ Equivalent Q (weightedSumSquares ℝ fun i ↦ (w i : ℝ)) :=
+  let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
+  ⟨sign ∘ ((↑) : ℝˣ → ℝ) ∘ w, fun i => sign_ne_zero.2 (w i).ne_zero,
+    ⟨hw₁.trans (isometryEquivSignWeightedSumSquares (((↑) : ℝˣ → ℝ) ∘ w))⟩⟩
+
 /-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted
 sum of squares with the weights being ±1. -/
 theorem equivalent_one_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
     [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) :
     ∃ w : Fin (FiniteDimensional.finrank ℝ M) → ℝ,
       (∀ i, w i = -1 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) :=
-  let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
-  ⟨Real.sign ∘ ((↑) : ℝˣ → ℝ) ∘ w, fun i => sign_apply_eq_of_ne_zero (w i) (w i).ne_zero,
-    ⟨hw₁.trans (isometryEquivSignWeightedSumSquares (((↑) : ℝˣ → ℝ) ∘ w))⟩⟩
+  let ⟨w, hw₀, hw⟩ := Q.equivalent_sign_ne_zero_weighted_sum_squared hQ
+  ⟨(w ·), fun i ↦ by cases hi : w i <;> simp_all, hw⟩
 #align quadratic_form.equivalent_one_neg_one_weighted_sum_squared QuadraticForm.equivalent_one_neg_one_weighted_sum_squared
 
+/-- **Sylvester's law of inertia**: A real quadratic form is equivalent to a weighted
+sum of squares with the weights being ±1 or 0, `SignType` version. -/
+theorem equivalent_signType_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
+    [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
+    ∃ w : Fin (FiniteDimensional.finrank ℝ M) → SignType,
+      Equivalent Q (weightedSumSquares ℝ fun i ↦ (w i : ℝ)) :=
+  let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares
+  ⟨sign ∘ w, ⟨hw₁.trans (isometryEquivSignWeightedSumSquares w)⟩⟩
+
 /-- **Sylvester's law of inertia**: A real quadratic form is equivalent to a weighted
 sum of squares with the weights being ±1 or 0. -/
 theorem equivalent_one_zero_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M]
     [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
     ∃ w : Fin (FiniteDimensional.finrank ℝ M) → ℝ,
       (∀ i, w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) :=
-  let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares
-  ⟨Real.sign ∘ ((↑) : ℝ → ℝ) ∘ w, fun i => sign_apply_eq (w i),
-    ⟨hw₁.trans (isometryEquivSignWeightedSumSquares w)⟩⟩
+  let ⟨w, hw⟩ := Q.equivalent_signType_weighted_sum_squared
+  ⟨(w ·), fun i ↦ by cases h : w i <;> simp [h], hw⟩
 #align quadratic_form.equivalent_one_zero_neg_one_weighted_sum_squared QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared
 
 end QuadraticForm