From 4fa4a28d5d4b204706f6134fb0721fff6b7170fd Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sat, 11 Jan 2025 17:11:38 +0000 Subject: [PATCH] refactor: Lint --- HepLean.lean | 2 +- HepLean/Lorentz/SL2C/SelfAdjoint.lean | 41 +++++++++++---------- HepLean/Mathematics/SchurTriangulation.lean | 38 ++++++++++--------- 3 files changed, 43 insertions(+), 38 deletions(-) diff --git a/HepLean.lean b/HepLean.lean index e443ce3..7f7367a 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -105,8 +105,8 @@ import HepLean.Mathematics.Fin.Involutions import HepLean.Mathematics.LinearMaps import HepLean.Mathematics.List import HepLean.Mathematics.PiTensorProduct -import HepLean.Mathematics.SchurTriangulation import HepLean.Mathematics.SO3.Basic +import HepLean.Mathematics.SchurTriangulation import HepLean.Meta.AllFilePaths import HepLean.Meta.Basic import HepLean.Meta.Informal.Basic diff --git a/HepLean/Lorentz/SL2C/SelfAdjoint.lean b/HepLean/Lorentz/SL2C/SelfAdjoint.lean index 9dc08cc..d0a5ec3 100644 --- a/HepLean/Lorentz/SL2C/SelfAdjoint.lean +++ b/HepLean/Lorentz/SL2C/SelfAdjoint.lean @@ -24,14 +24,16 @@ noncomputable def toSelfAdjointMap' (M : ℂ²ˣ²) : ℍ₂ →ₗ[ℝ] ℍ₂ map_smul' | r, ⟨A, _⟩ => Subtype.ext <| by simp open Complex (I normSq) in -theorem toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (detM : M.det = 1) - : LinearMap.det (toSelfAdjointMap' M) = 1 := +lemma toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (detM : M.det = 1) : + LinearMap.det (toSelfAdjointMap' M) = 1 := let b : Basis (Fin 2 ⊕ Fin 2) ℝ ℍ₂ := Basis.ofEquivFun { toFun := fun ⟨A, _⟩ => ![(A 0 0).re, (A 1 1).re] ⊕ᵥ ![(A 0 1).re, (A 0 1).im] map_add' := fun _ _ => funext fun | .inl 0 | .inl 1 | .inr 0 | .inr 1 => rfl map_smul' := fun _ _ => funext fun | .inl 0 | .inl 1 | .inr 0 | .inr 1 => by simp invFun := fun p => { - val := let z : ℂ := ⟨p (.inr 0), p (.inr 1)⟩ ; !![p (.inl 0), z; conj z, p (.inl 1)] + val := + let z : ℂ := ⟨p (.inr 0), p (.inr 1)⟩ + !![p (.inl 0), z; conj z, p (.inl 1)] property := Matrix.ext fun | 0, 0 | 0, 1 | 1, 0 | 1, 1 => by simp } left_inv := fun ⟨A, hA⟩ => Subtype.ext <| Matrix.ext fun @@ -46,12 +48,11 @@ theorem toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (de let E₂ : ℂ²ˣ² := !![0, 1; conj 1, 0] -- b (.inr 0) let E₃ : ℂ²ˣ² := !![0, I; conj I, 0] -- b (.inr 1) let F : Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) ℝ := LinearMap.toMatrix b b (toSelfAdjointMap' M) - let A := F.toBlocks₁₁ ; let B := F.toBlocks₁₂ ; let C := F.toBlocks₂₁ ; let D := F.toBlocks₂₂ - let x := M 0 0 ; let y := M 1 1 ; have hM10 : M 1 0 = 0 := hM <| show 0 < 1 by decide + let A := F.toBlocks₁₁; let B := F.toBlocks₁₂; let C := F.toBlocks₂₁; let D := F.toBlocks₂₂ + let x := M 0 0; let y := M 1 1; have hM10 : M 1 0 = 0 := hM <| show 0 < 1 by decide have he : M = !![x, _; 0, y] := Matrix.ext fun | 0, 0 | 0, 1 | 1, 1 => rfl | 1, 0 => hM10 have he' : Mᴴ = !![conj x, 0; _, conj y] := Matrix.ext fun | 0, 0 | 1, 0 | 1, 1 => rfl | 0, 1 => by simp [hM10] - have detA_one : normSq x * normSq y = 1 := congrArg Complex.re <| calc ↑(normSq x * normSq y) _ = x * conj x * (y * conj y) := by simp [Complex.mul_conj] @@ -64,10 +65,10 @@ theorem toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (de _ = 1 := detM have detD_one : D.det = 1 := let z := x * conj y - have k₀ : (M * E₂ * Mᴴ) 0 1 = z := by rw [he', he] ; simp [E₂] + have k₀ : (M * E₂ * Mᴴ) 0 1 = z := by rw [he', he]; simp [E₂] have k₁ : (M * E₃ * Mᴴ) 0 1 = ⟨-z.im, z.re⟩ := calc - _ = x * I * conj y := by rw [he', he] ; simp [E₃] + _ = x * I * conj y := by rw [he', he]; simp [E₃] _ = Complex.I * z := by ring _ = ⟨-z.im, z.re⟩ := z.I_mul have hD : D = !![z.re, -z.im; z.im, z.re] := Matrix.ext fun @@ -81,33 +82,33 @@ theorem toSelfAdjointMap_det_one' {M : ℂ²ˣ²} (hM : M.IsUpperTriangular) (de letI : Invertible D.det := detD_one ▸ invertibleOne letI : Invertible D := D.invertibleOfDetInvertible have hE : A - B * ⅟D * C = !![normSq x, _; 0, normSq y] := - have k : (M * E₀ * Mᴴ) 0 1 = 0 := by rw [he', he] ; simp [E₀] + have k : (M * E₀ * Mᴴ) 0 1 = 0 := by rw [he', he]; simp [E₀] have hC00 : C 0 0 = 0 := congrArg Complex.re k have hC10 : C 1 0 = 0 := congrArg Complex.im k Matrix.ext fun | 0, 1 => rfl | 1, 0 => have hA10 : A 1 0 = 0 := congrArg Complex.re <| - show (M * E₀ * Mᴴ) 1 1 = 0 by rw [he', he] ; simp [E₀] + show (M * E₀ * Mᴴ) 1 1 = 0 by rw [he', he]; simp [E₀] show A 1 0 - (B * ⅟D) 1 ⬝ᵥ (C · 0) = 0 by simp [hC00, hC10, hA10] | 0, 0 => have hA00 : A 0 0 = normSq x := congrArg Complex.re <| - show (M * E₀ * Mᴴ) 0 0 = normSq x by rw [he', he] ; simp [E₀, x.mul_conj] + show (M * E₀ * Mᴴ) 0 0 = normSq x by rw [he', he]; simp [E₀, x.mul_conj] show A 0 0 - (B * ⅟D) 0 ⬝ᵥ (C · 0) = normSq x by simp [hC00, hC10, hA00] | 1, 1 => have hA11 : A 1 1 = normSq y := congrArg Complex.re <| - show (M * E₁ * Mᴴ) 1 1 = normSq y by rw [he', he] ; simp [E₁, y.mul_conj] + show (M * E₁ * Mᴴ) 1 1 = normSq y by rw [he', he]; simp [E₁, y.mul_conj] have hB10 : B 1 0 = 0 := congrArg Complex.re <| - show (M * E₂ * Mᴴ) 1 1 = 0 by rw [he', he] ; simp [E₂] + show (M * E₂ * Mᴴ) 1 1 = 0 by rw [he', he]; simp [E₂] have hB11 : B 1 1 = 0 := congrArg Complex.re <| - show (M * E₃ * Mᴴ) 1 1 = 0 by rw [he', he] ; simp [E₃] + show (M * E₃ * Mᴴ) 1 1 = 0 by rw [he', he]; simp [E₃] calc A 1 1 - (B * ⅟D * C) 1 1 _ = A 1 1 - B 1 ⬝ᵥ ((⅟D * C) · 1) := by noncomm_ring _ = normSq y := by simp [hB10, hB11, hA11] calc LinearMap.det (toSelfAdjointMap' M) _ = F.det := (LinearMap.det_toMatrix ..).symm _ = D.det * (A - B * ⅟D * C).det := F.fromBlocks_toBlocks ▸ Matrix.det_fromBlocks₂₂ .. - _ = 1 := by rw [hE] ; simp [detD_one, detA_one] + _ = 1 := by rw [hE]; simp [detD_one, detA_one] /-- This promotes `Lorentz.SL2C.toSelfAdjointMap M` and its definitional equivalence, `Lorentz.SL2C.toSelfAdjointMap' M`, to a linear equivalence by recognising the linear inverse to be @@ -124,17 +125,17 @@ noncomputable def toSelfAdjointEquiv (M : ℂ²ˣ²) [Invertible M] : ℍ₂ ≃ _ = M * M⁻¹ * A * (M * M⁻¹)ᴴ := by noncomm_ring [Matrix.conjTranspose_mul] _ = A := by simp -theorem toSelfAdjointMap_mul (M N : ℂ²ˣ²) - : toSelfAdjointMap' (M * N) = toSelfAdjointMap' M ∘ₗ toSelfAdjointMap' N := +lemma toSelfAdjointMap_mul (M N : ℂ²ˣ²) : + toSelfAdjointMap' (M * N) = toSelfAdjointMap' M ∘ₗ toSelfAdjointMap' N := LinearMap.ext fun A => Subtype.ext <| show M * N * A * (M * N)ᴴ = M * (N * A * Nᴴ) * Mᴴ by noncomm_ring [Matrix.conjTranspose_mul] -theorem toSelfAdjointMap_similar_det (M N : ℂ²ˣ²) [Invertible M] - : LinearMap.det (toSelfAdjointMap' (M * N * M⁻¹)) = LinearMap.det (toSelfAdjointMap' N) := +lemma toSelfAdjointMap_similar_det (M N : ℂ²ˣ²) [Invertible M] : + LinearMap.det (toSelfAdjointMap' (M * N * M⁻¹)) = LinearMap.det (toSelfAdjointMap' N) := let e := toSelfAdjointEquiv M let f := toSelfAdjointMap' N suffices toSelfAdjointMap' (M * N * M⁻¹) = e ∘ₗ f ∘ₗ e.symm from this ▸ f.det_conj e - by rw [toSelfAdjointMap_mul, toSelfAdjointMap_mul] ; rfl + by rw [toSelfAdjointMap_mul, toSelfAdjointMap_mul]; rfl end SL2C end Lorentz diff --git a/HepLean/Mathematics/SchurTriangulation.lean b/HepLean/Mathematics/SchurTriangulation.lean index 7e642dc..ede3bb7 100644 --- a/HepLean/Mathematics/SchurTriangulation.lean +++ b/HepLean/Mathematics/SchurTriangulation.lean @@ -22,10 +22,10 @@ def finAddEquivSigmaCond : Fin (m + n) ≃ Σ b, cond b (Fin m) (Fin n) := variable {i : Fin (m + n)} -theorem finAddEquivSigmaCond_true (h : i < m) : finAddEquivSigmaCond i = ⟨true, i, h⟩ := +lemma finAddEquivSigmaCond_true (h : i < m) : finAddEquivSigmaCond i = ⟨true, i, h⟩ := congrArg sumEquivSigmalCond <| finSumFinEquiv_symm_apply_castAdd ⟨i, h⟩ -theorem finAddEquivSigmaCond_false (h : ¬ i < m) : finAddEquivSigmaCond i = ⟨false, i.subNat' h⟩ := +lemma finAddEquivSigmaCond_false (h : ¬ i < m) : finAddEquivSigmaCond i = ⟨false, i.subNat' h⟩ := let j : Fin n := i.subNat' h calc finAddEquivSigmaCond i _ = finAddEquivSigmaCond (Fin.natAdd m j) := @@ -66,15 +66,16 @@ variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] section variable [FiniteDimensional 𝕜 E] [Fintype n] [DecidableEq n] -theorem toMatrixOrthonormal_apply_apply (b : OrthonormalBasis n 𝕜 E) (f : Module.End 𝕜 E) (i j : n) - : toMatrixOrthonormal b f i j = ⟪b i, f (b j)⟫_𝕜 := +lemma toMatrixOrthonormal_apply_apply (b : OrthonormalBasis n 𝕜 E) (f : Module.End 𝕜 E) + (i j : n) : + toMatrixOrthonormal b f i j = ⟪b i, f (b j)⟫_𝕜 := calc _ = b.repr (f (b j)) i := f.toMatrix_apply .. _ = ⟪b i, f (b j)⟫_𝕜 := b.repr_apply_apply .. -theorem toMatrixOrthonormal_reindex [Fintype m] [DecidableEq m] - (b : OrthonormalBasis m 𝕜 E) (e : m ≃ n) (f : Module.End 𝕜 E) - : toMatrixOrthonormal (b.reindex e) f = Matrix.reindex e e (toMatrixOrthonormal b f) := +lemma toMatrixOrthonormal_reindex [Fintype m] [DecidableEq m] + (b : OrthonormalBasis m 𝕜 E) (e : m ≃ n) (f : Module.End 𝕜 E) : + toMatrixOrthonormal (b.reindex e) f = Matrix.reindex e e (toMatrixOrthonormal b f) := Matrix.ext fun i j => calc toMatrixOrthonormal (b.reindex e) f i j _ = (b.reindex e).repr (f (b.reindex e j)) i := f.toMatrix_apply .. @@ -101,8 +102,8 @@ variable [IsAlgClosed 𝕜] /-- **Don't use this definition directly.** This is the key algorithm behind `Matrix.schur_triangulation`. -/ protected noncomputable def SchurTriangulationAux.of - [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : Module.End 𝕜 E) - : SchurTriangulationAux f := + [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : Module.End 𝕜 E) : + SchurTriangulationAux f := haveI : Decidable (Nontrivial E) := Classical.propDecidable _ if hE : Nontrivial E then let μ : f.Eigenvalues := default @@ -137,7 +138,9 @@ protected noncomputable def SchurTriangulationAux.of by simp have hf {bi i' bj j'} (hi : e i = ⟨bi, i'⟩) (hj : e j = ⟨bj, j'⟩) := calc toMatrixOrthonormal basis f i j - _ = toMatrixOrthonormal bE f (e i) (e j) := by rw [f.toMatrixOrthonormal_reindex] ; rfl + _ = toMatrixOrthonormal bE f (e i) (e j) := by + rw [f.toMatrixOrthonormal_reindex] + rfl _ = ⟪bE (e i), f (bE (e j))⟫_𝕜 := f.toMatrixOrthonormal_apply_apply .. _ = ⟪(B bi i' : E), f (B bj j')⟫_𝕜 := by rw [hB, hB, hi, hj] @@ -198,8 +201,8 @@ variable [RCLike 𝕜] [IsAlgClosed 𝕜] [Fintype n] [DecidableEq n] [LinearOrd `Matrix.schurTriangulationUnitary`, and `Matrix.schurTriangulation` for which this is their simultaneous definition. This is `LinearMap.SchurTriangulationAux` adapted for matrices in the Euclidean space. -/ -noncomputable def schurTriangulationAux - : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n) × UpperTriangular n 𝕜 := +noncomputable def schurTriangulationAux : + OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n) × UpperTriangular n 𝕜 := let f := toEuclideanLin A let ⟨d, hd, b, hut⟩ := LinearMap.SchurTriangulationAux.of f let e : Fin d ≃o n := Fintype.orderIsoFinOfCardEq n (finrank_euclideanSpace.symm.trans hd) @@ -208,8 +211,9 @@ noncomputable def schurTriangulationAux suffices B.IsUpperTriangular from ⟨b', B, this⟩ fun i j (hji : j < i) => calc LinearMap.toMatrixOrthonormal b' f i j - _ = LinearMap.toMatrixOrthonormal b f (e.symm i) (e.symm j) := - by rw [f.toMatrixOrthonormal_reindex] ; rfl + _ = LinearMap.toMatrixOrthonormal b f (e.symm i) (e.symm j) := by + rw [f.toMatrixOrthonormal_reindex] + rfl _ = 0 := hut (e.symm.lt_iff_lt.mpr hji) /-- The change of basis that induces the upper triangular form `A.schurTriangulation` of a matrix @@ -231,8 +235,8 @@ noncomputable def schurTriangulation : UpperTriangular n 𝕜 := /-- **Schur triangulation**, **Schur decomposition** for matrices over an algebraically closed field. In particular, a complex matrix can be converted to upper-triangular form by a change of basis. In other words, any complex matrix is unitarily similar to an upper triangular matrix. -/ -theorem schur_triangulation - : A = A.schurTriangulationUnitary * A.schurTriangulation * star A.schurTriangulationUnitary := +lemma schur_triangulation : + A = A.schurTriangulationUnitary * A.schurTriangulation * star A.schurTriangulationUnitary := let U := A.schurTriangulationUnitary have h : U * A.schurTriangulation.val = A * U := let b := A.schurTriangulationBasis.toBasis @@ -243,6 +247,6 @@ theorem schur_triangulation _ = A * U := by simp calc A _ = A * U * star U := by simp [mul_assoc] - _ = U * A.schurTriangulation * star U := by rw [←h] + _ = U * A.schurTriangulation * star U := by rw [← h] end Matrix