diff --git a/Monlib/LinearAlgebra/InnerAut.lean b/Monlib/LinearAlgebra/InnerAut.lean index e749bbd..c907530 100644 --- a/Monlib/LinearAlgebra/InnerAut.lean +++ b/Monlib/LinearAlgebra/InnerAut.lean @@ -10,7 +10,7 @@ import Monlib.LinearAlgebra.MyMatrix.PosEqLinearMapIsPositive import Monlib.LinearAlgebra.MyTensorProduct import Monlib.RepTheory.AutMat import Monlib.Preq.StarAlgEquiv -import Mathlib.Tactic.Explode +-- import Mathlib.Tactic.Explode #align_import linear_algebra.innerAut diff --git a/Monlib/LinearAlgebra/IsProj'.lean b/Monlib/LinearAlgebra/IsProj'.lean index a0c3738..04c7360 100644 --- a/Monlib/LinearAlgebra/IsProj'.lean +++ b/Monlib/LinearAlgebra/IsProj'.lean @@ -39,7 +39,7 @@ end variable {E 𝕜 : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] -theorem orthogonalProjection_eq_linear_proj' {K : Submodule 𝕜 E} [CompleteSpace K] : +theorem orthogonalProjection_eq_linear_proj' {K : Submodule 𝕜 E} [HasOrthogonalProjection K] : (orthogonalProjection K : E →ₗ[𝕜] K) = Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace := by @@ -49,15 +49,15 @@ theorem orthogonalProjection_eq_linear_proj' {K : Submodule 𝕜 E} [CompleteSpa rw [ContinuousLinearMap.coe_coe, map_add, orthogonalProjection_mem_subspace_eq_self, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero] -theorem orthogonalProjection_eq_linear_proj'' {K : Submodule 𝕜 E} [CompleteSpace K] (x : E) : +theorem orthogonalProjection_eq_linear_proj'' {K : Submodule 𝕜 E} [HasOrthogonalProjection K] (x : E) : orthogonalProjection K x = Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace x := by rw [← orthogonalProjection_eq_linear_proj] -noncomputable def orthogonalProjection' (U : Submodule 𝕜 E) [CompleteSpace U] : E →L[𝕜] E := +noncomputable def orthogonalProjection' (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : E →L[𝕜] E := U.subtypeL.comp (orthogonalProjection U) -theorem orthogonalProjection'_apply (U : Submodule 𝕜 E) [CompleteSpace U] (x : E) : +theorem orthogonalProjection'_apply (U : Submodule 𝕜 E) [HasOrthogonalProjection U] (x : E) : orthogonalProjection' U x = orthogonalProjection U x := rfl @@ -66,24 +66,25 @@ local notation "P" => orthogonalProjection local notation "↥P" => orthogonalProjection' @[simp] -theorem ContinuousLinearMap.range_toLinearMap {p : E →L[𝕜] E} : LinearMap.range (p.toLinearMap) = LinearMap.range p := +theorem ContinuousLinearMap.range_toLinearMap {F : Type*} [NormedAddCommGroup F] + [InnerProductSpace 𝕜 F] {p : E →L[𝕜] F} : LinearMap.range (p.toLinearMap) = LinearMap.range p := rfl open ContinuousLinearMap @[simp] -theorem orthogonalProjection.range (U : Submodule 𝕜 E) [CompleteSpace U] : +theorem orthogonalProjection.range (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : LinearMap.range (↥P U) = U := by simp_rw [orthogonalProjection', ← range_toLinearMap, coe_comp, orthogonalProjection_eq_linear_proj', Submodule.coe_subtypeL, LinearMap.range_comp, Submodule.linearProjOfIsCompl_range, Submodule.map_subtype_top] @[simp] -theorem orthogonalProjection'_eq (U : Submodule 𝕜 E) [CompleteSpace U] : +theorem orthogonalProjection'_eq (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : ↥P U = U.subtypeL.comp (P U) := rfl -theorem orthogonal_projection'_eq_linear_proj {K : Submodule 𝕜 E} [CompleteSpace K] : +theorem orthogonal_projection'_eq_linear_proj {K : Submodule 𝕜 E} [HasOrthogonalProjection K] : (K.subtypeL.comp (orthogonalProjection K) : E →ₗ[𝕜] E) = (K.subtype).comp (Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace) := @@ -92,7 +93,7 @@ theorem orthogonal_projection'_eq_linear_proj {K : Submodule 𝕜 E} [CompleteSp simp_rw [ContinuousLinearMap.coe_coe, LinearMap.comp_apply, ContinuousLinearMap.comp_apply, Submodule.subtypeL_apply, Submodule.subtype_apply, orthogonalProjection_eq_linear_proj''] -theorem orthogonalProjection'_eq_linear_proj' {K : Submodule 𝕜 E} [CompleteSpace K] (x : E) : +theorem orthogonalProjection'_eq_linear_proj' {K : Submodule 𝕜 E} [HasOrthogonalProjection K] (x : E) : (orthogonalProjection' K : E →ₗ[𝕜] E) x = (K.subtype).comp (Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace) x := diff --git a/Monlib/LinearAlgebra/IsReal.lean b/Monlib/LinearAlgebra/IsReal.lean index 2e6b5d7..c1d34e8 100644 --- a/Monlib/LinearAlgebra/IsReal.lean +++ b/Monlib/LinearAlgebra/IsReal.lean @@ -5,7 +5,13 @@ Authors: Monica Omar -/ import Mathlib.Algebra.Star.StarAlgHom import Mathlib.Algebra.Star.BigOperators -import Monlib.LinearAlgebra.InnerAut +-- import Monlib.LinearAlgebra.InnerAut +import Mathlib.Algebra.Algebra.Spectrum +import Monlib.LinearAlgebra.End +import Monlib.Preq.StarAlgEquiv +import Mathlib.Analysis.RCLike.Basic +import Mathlib.Analysis.InnerProductSpace.Basic +import Mathlib.Algebra.Algebra.Bilinear import Mathlib.Algebra.Algebra.Basic #align_import linear_algebra.is_real @@ -27,11 +33,11 @@ variable {E F K : Type _} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] @[simps] -def LinearMap.real (φ : E →ₗ[K] F) : E →ₗ[K] F - where +def LinearMap.real (φ : E →ₗ[K] F) : + E →ₗ[K] F where toFun x := star (φ (star x)) - map_add' x y := by simp only [star_add, map_add] - map_smul' r x := by simp only [star_smul, _root_.map_smul, star_star, RingHom.id_apply] + map_add' _ _ := by simp only [star_add, map_add] + map_smul' _ _ := by simp only [star_smul, _root_.map_smul, star_star, RingHom.id_apply] theorem LinearMap.isReal_iff (φ : E →ₗ[K] F) : φ.IsReal ↔ φ.real = φ := by simp_rw [LinearMap.IsReal, LinearMap.ext_iff, LinearMap.real_apply, diff --git a/Monlib/LinearAlgebra/MyIps/MatIps.lean b/Monlib/LinearAlgebra/MyIps/MatIps.lean index a64578c..da592f9 100644 --- a/Monlib/LinearAlgebra/MyIps/MatIps.lean +++ b/Monlib/LinearAlgebra/MyIps/MatIps.lean @@ -401,7 +401,7 @@ protected theorem basis_apply (hφ : φ.IsFaithfulPosMap) (ij : n × n) : hφ.basis ij = stdBasisMatrix ij.1 ij.2 (1 : ℂ) * hφ.matrixIsPosDef.rpow (-(1 / 2 : ℝ)) := by rw [IsFaithfulPosMap.basis, Basis.mk_apply] -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y protected noncomputable def toMatrix (hφ : φ.IsFaithfulPosMap) : (Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) ≃ₐ[ℂ] Matrix (n × n) (n × n) ℂ := @@ -501,14 +501,14 @@ protected theorem toMatrix_symm_apply (hφ : φ.IsFaithfulPosMap) end Module.Dual.IsFaithfulPosMap -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j k l) -/ theorem Module.Dual.eq_rankOne_of_faithful_pos_map (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : x = ∑ i : n, ∑ j : n, ∑ k : n, ∑ l : n, - hφ.toMatrix x (i, j) (k, l) • | hφ.basis (i, j)⟩⟨ hφ.basis (k, l)| := + hφ.toMatrix x (i, j) (k, l) • |hφ.basis (i, j)⟩⟨ hφ.basis (k, l)| := by rw [← Module.Dual.IsFaithfulPosMap.toMatrix_symm_apply, AlgEquiv.symm_apply_apply] end SingleBlock diff --git a/Monlib/LinearAlgebra/MyIps/MinimalProj.lean b/Monlib/LinearAlgebra/MyIps/MinimalProj.lean index af2d1a0..65123d3 100644 --- a/Monlib/LinearAlgebra/MyIps/MinimalProj.lean +++ b/Monlib/LinearAlgebra/MyIps/MinimalProj.lean @@ -136,31 +136,72 @@ local notation "P" => orthogonalProjection theorem self_adjoint_proj_commutes [InnerProductSpace 𝕜 E] [CompleteSpace E] {p q : E →L[𝕜] E} (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : p.comp q = p ↔ q.comp p = p := by - have : Function.Injective fun a₁ : E →L[𝕜] E => star a₁ := - by - intro x y h - exact star_injective h constructor <;> intro h <;> - · apply_fun adjoint - simp only [adjoint_comp, isSelfAdjoint_iff'.mp hpa, isSelfAdjoint_iff'.mp hqa, h] + · apply_fun adjoint using star_injective + simp only [adjoint_comp, isSelfAdjoint_iff'.mp hpa, isSelfAdjoint_iff'.mp hqa, h] local notation "↥P" => orthogonalProjection' -theorem orthogonalProjection.idempotent [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) - [CompleteSpace U] : IsIdempotentElem (↥P U) := +theorem orthogonalProjection.isIdempotentElem [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) + [HasOrthogonalProjection U] : IsIdempotentElem (↥P U) := by rw [IsIdempotentElem] ext simp_rw [mul_apply, orthogonalProjection'_eq, comp_apply, Submodule.subtypeL_apply, orthogonalProjection_mem_subspace_eq_self] -def ContinuousLinearMap.IsOrthogonalProjection [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : Prop := - IsIdempotentElem T ∧ LinearMap.ker T = (LinearMap.range T)ᗮ +class ContinuousLinearMap.IsOrthogonalProjection [InnerProductSpace 𝕜 E] + (T : E →L[𝕜] E) : Prop := + isIdempotent : IsIdempotentElem T + kerEqRangeOrtho : LinearMap.ker T = (LinearMap.range T)ᗮ + +lemma ContinuousLinearMap.IsOrthogonalProjection.eq [InnerProductSpace 𝕜 E] + {T : E →L[𝕜] E} (hT : T.IsOrthogonalProjection) : + IsIdempotentElem T ∧ (LinearMap.ker T = (LinearMap.range T)ᗮ) := +⟨hT.1, hT.2⟩ + +theorem IsIdempotentElem.clm_to_lm [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} : + IsIdempotentElem T ↔ IsIdempotentElem (T : E →ₗ[𝕜] E) := + by + simp_rw [IsIdempotentElem, LinearMap.mul_eq_comp, ← coe_comp, coe_inj] + rfl + +lemma ContinuousLinearMap.HasOrthogonalProjection_of_isOrthogonalProjection [InnerProductSpace 𝕜 E] + {T : E →L[𝕜] E} [h : T.IsOrthogonalProjection] : HasOrthogonalProjection (LinearMap.range T) := +by + constructor + intro x + rw [← h.kerEqRangeOrtho] + simp only [LinearMap.mem_range, LinearMap.mem_ker, map_sub, exists_exists_eq_and] + simp_rw [← mul_apply, h.isIdempotent.eq] + exact ⟨x, sub_self _⟩ + +lemma ker_to_clm [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} : + LinearMap.ker (T : E →ₗ[𝕜] E) = LinearMap.ker T := rfl + +lemma subtype_compL_ker [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) + (f : E →L[𝕜] U) : + LinearMap.ker (U.subtypeL ∘L f) = (LinearMap.ker f) := + by + rw [← ker_to_clm] + simp only [coe_comp, Submodule.coe_subtypeL, LinearMap.ker_comp, + Submodule.ker_subtype, Submodule.comap_bot] + rfl + +lemma orthogonalProjection.isOrthogonalProjection [InnerProductSpace 𝕜 E] + {U : Submodule 𝕜 E} [h : HasOrthogonalProjection U] : + (↥P U).IsOrthogonalProjection := +by + refine ⟨orthogonalProjection.isIdempotentElem _, ?_⟩ + rw [orthogonalProjection.range, ← ker_orthogonalProjection, orthogonalProjection'_eq, + subtype_compL_ker] + +open LinearMap in /-- given any idempotent operator $T ∈ L(V)$, then `is_compl T.ker T.range`, in other words, there exists unique $v ∈ \textnormal{ker}(T)$ and $w ∈ \textnormal{range}(T)$ such that $x = v + w$ -/ -theorem LinearMap.IsIdempotent.isCompl_range_ker {V R : Type _} [Ring R] [AddCommGroup V] - [Module R V] (T : V →ₗ[R] V) (h : IsIdempotentElem T) : IsCompl (ker T) (range T) := +theorem IsIdempotentElem.isCompl_range_ker {V R : Type _} [Ring R] [AddCommGroup V] + [Module R V] {T : V →ₗ[R] V} (h : IsIdempotentElem T) : IsCompl (ker T) (range T) := by constructor · rw [disjoint_iff] @@ -192,21 +233,7 @@ theorem LinearMap.IsIdempotent.isCompl_range_ker {V R : Type _} [Ring R] [AddCom theorem IsCompl.of_orthogonal_projection [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (h : T.IsOrthogonalProjection) : IsCompl (LinearMap.ker T) (LinearMap.range T) := - LinearMap.IsIdempotent.isCompl_range_ker _ ((IsIdempotentElem.toLinearMap _).mp h.1) - -theorem orthogonalProjection.isOrthogonalProjection [InnerProductSpace ℂ E] {U : Submodule ℂ E} - [CompleteSpace E] [CompleteSpace U] : (↥P U).IsOrthogonalProjection := - ⟨(orthogonalProjection.idempotent U : IsIdempotentElem (U.subtypeL.comp (P U) : E →L[ℂ] E)), - (ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_ker_isOrtho_to_range (U.subtypeL.comp (P U) : E →L[ℂ] E) - (orthogonalProjection.idempotent U : - IsIdempotentElem (U.subtypeL.comp (P U) : E →L[ℂ] E))).mp - (orthogonalProjection_isSelfAdjoint U)⟩ - -theorem IsIdempotentElem.clm_to_lm [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} : - IsIdempotentElem T ↔ IsIdempotentElem (T : E →ₗ[𝕜] E) := - by - simp_rw [IsIdempotentElem, LinearMap.mul_eq_comp, ← coe_comp, coe_inj] - rfl +IsIdempotentElem.isCompl_range_ker ((IsIdempotentElem.toLinearMap _).mp h.1) /-- $P_V P_U = P_U$ if and only if $P_V - P_U$ is an orthogonal projection -/ theorem sub_of_isOrthogonalProjection [InnerProductSpace ℂ E] [CompleteSpace E] @@ -217,8 +244,8 @@ theorem sub_of_isOrthogonalProjection [InnerProductSpace ℂ E] [CompleteSpace E let q := ↥P V have pp : p = U.subtypeL.comp (P U) := rfl have qq : q = V.subtypeL.comp (P V) := rfl - have hp : IsIdempotentElem p := orthogonalProjection.idempotent U - have hq : IsIdempotentElem q := orthogonalProjection.idempotent V + have hp : IsIdempotentElem p := orthogonalProjection.isIdempotentElem U + have hq : IsIdempotentElem q := orthogonalProjection.isIdempotentElem V have hpa := orthogonalProjection_isSelfAdjoint U have hqa := orthogonalProjection_isSelfAdjoint V have h2 := self_adjoint_proj_commutes hpa hqa @@ -312,67 +339,67 @@ end section -/-- instance for `≤` on bounded linear maps -/ -instance {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - [CompleteSpace E] : LE (E →L[𝕜] E) := - by - refine' { le := _ } - intro u v - exact IsPositive (v - u) - -theorem ContinuousLinearMap.isSelfAdjoint_zero {E : Type*} - [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : - IsSelfAdjoint (0 : E →L[𝕜] E) := -_root_.isSelfAdjoint_zero _ - -/-- when `a,b` are self-adjoint operators, then - if `a ≤ b` and `b ≤ a`, then `a = b` -/ -theorem IsSelfAdjoint.HasLe.le_antisymm {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] {a b : E →L[𝕜] E} (ha : IsSelfAdjoint a) - (hb : IsSelfAdjoint b) (hab : a ≤ b) (hba : b ≤ a) : a = b := - by - simp_rw [LE.le] at * - rw [ContinuousLinearMap.IsSelfAdjoint.ext_iff_inner_map ha hb] - intro x - have hba2 := hba.2 x - rw [← neg_le_neg_iff, reApplyInnerSelf_apply, ← map_neg, ← inner_neg_left, ← neg_apply, - neg_sub, neg_zero] at hba2 - symm - have := (hab.2 x) - simp_rw [reApplyInnerSelf_apply] at this - rw [← sub_eq_zero, ← inner_sub_left, ← sub_apply, ← IsSelfAdjoint.inner_re_eq hab.1 x, RCLike.ofReal_eq_zero, - _root_.le_antisymm hba2 this] - -/-- we always have `a ≤ a` -/ -@[refl, simp] -theorem ContinuousLinearMap.hasLe.le_refl {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] {a : E →L[𝕜] E} : a ≤ a := by - simp_rw [LE.le, sub_self, isPositive_zero] - -/-- when `a,b` are self-adjoint operators, then - if `a ≤ b` and `b ≤ c`, then `a ≤ c` -/ -@[simp] -theorem IsSelfAdjoint.HasLe.le_trans {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] {a b c : E →L[𝕜] E} - (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := - by - simp_rw [LE.le] at * - rw [← add_zero c, ← sub_self b, ← add_sub_assoc, add_sub_right_comm, add_sub_assoc] - exact IsPositive.add hbc hab - -/-- `p ≤ q` means `q - p` is positive -/ -@[refl, simp] -theorem ContinuousLinearMap.IsPositive.hasLe {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] {p q : E →L[𝕜] E} : p ≤ q ↔ (q - p).IsPositive := by - rfl - -/-- saying `p` is positive is the same as saying `0 ≤ p` -/ -@[simp] -theorem ContinuousLinearMap.IsPositive.is_nonneg {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} : p.IsPositive ↔ 0 ≤ p := - by - nth_rw 1 [← sub_zero p] - rfl +-- /-- instance for `≤` on bounded linear maps -/ +-- instance {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] +-- [CompleteSpace E] : LE (E →L[𝕜] E) := +-- by +-- refine' { le := _ } +-- intro u v +-- exact IsPositive (v - u) + +-- theorem ContinuousLinearMap.isSelfAdjoint_zero {E : Type*} +-- [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : +-- IsSelfAdjoint (0 : E →L[𝕜] E) := +-- _root_.isSelfAdjoint_zero _ + +-- /-- when `a,b` are self-adjoint operators, then +-- if `a ≤ b` and `b ≤ a`, then `a = b` -/ +-- theorem IsSelfAdjoint.HasLe.le_antisymm {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] +-- [InnerProductSpace 𝕜 E] [CompleteSpace E] {a b : E →L[𝕜] E} (ha : IsSelfAdjoint a) +-- (hb : IsSelfAdjoint b) (hab : a ≤ b) (hba : b ≤ a) : a = b := +-- by +-- simp_rw [LE.le] at * +-- rw [ContinuousLinearMap.IsSelfAdjoint.ext_iff_inner_map ha hb] +-- intro x +-- have hba2 := hba.2 x +-- rw [← neg_le_neg_iff, reApplyInnerSelf_apply, ← map_neg, ← inner_neg_left, ← neg_apply, +-- neg_sub, neg_zero] at hba2 +-- symm +-- have := (hab.2 x) +-- simp_rw [reApplyInnerSelf_apply] at this +-- rw [← sub_eq_zero, ← inner_sub_left, ← sub_apply, ← IsSelfAdjoint.inner_re_eq hab.1 x, RCLike.ofReal_eq_zero, +-- _root_.le_antisymm hba2 this] + +-- /-- we always have `a ≤ a` -/ +-- @[refl, simp] +-- theorem ContinuousLinearMap.hasLe.le_refl {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] +-- [InnerProductSpace 𝕜 E] [CompleteSpace E] {a : E →L[𝕜] E} : a ≤ a := by +-- simp_rw [LE.le, sub_self, isPositive_zero] + +-- /-- when `a,b` are self-adjoint operators, then +-- if `a ≤ b` and `b ≤ c`, then `a ≤ c` -/ +-- @[simp] +-- theorem IsSelfAdjoint.HasLe.le_trans {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] +-- [InnerProductSpace 𝕜 E] [CompleteSpace E] {a b c : E →L[𝕜] E} +-- (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := +-- by +-- simp_rw [LE.le] at * +-- rw [← add_zero c, ← sub_self b, ← add_sub_assoc, add_sub_right_comm, add_sub_assoc] +-- exact IsPositive.add hbc hab + +-- /-- `p ≤ q` means `q - p` is positive -/ +-- @[refl, simp] +-- theorem ContinuousLinearMap.IsPositive.hasLe {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] +-- [InnerProductSpace 𝕜 E] [CompleteSpace E] {p q : E →L[𝕜] E} : p ≤ q ↔ (q - p).IsPositive := by +-- rfl + +-- /-- saying `p` is positive is the same as saying `0 ≤ p` -/ +-- @[simp] +-- theorem ContinuousLinearMap.IsPositive.is_nonneg {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] +-- [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} : p.IsPositive ↔ 0 ≤ p := +-- by +-- nth_rw 1 [← sub_zero p] +-- rfl end @@ -381,7 +408,7 @@ theorem SelfAdjointAndIdempotent.is_positive {𝕜 E : Type _} [RCLike 𝕜] [No [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) (hpa : IsSelfAdjoint p) : 0 ≤ p := by - rw [← ContinuousLinearMap.IsPositive.is_nonneg] + rw [ContinuousLinearMap.nonneg_iff_isPositive] refine' ⟨hpa, _⟩ rw [← hp.eq] simp_rw [reApplyInnerSelf_apply, mul_apply] @@ -392,7 +419,7 @@ theorem SelfAdjointAndIdempotent.is_positive {𝕜 E : Type _} [RCLike 𝕜] [No /-- an idempotent is positive if and only if it is self-adjoint -/ theorem IsIdempotentElem.is_positive_iff_self_adjoint [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : 0 ≤ p ↔ IsSelfAdjoint p := - ⟨fun h => (ContinuousLinearMap.IsPositive.is_nonneg.mpr h).1, fun h => + ⟨fun h => ((ContinuousLinearMap.nonneg_iff_isPositive _).mp h).1, fun h => SelfAdjointAndIdempotent.is_positive hp h⟩ theorem IsIdempotentElem.self_adjoint_is_positive_isOrthogonalProjection_tFAE {E : Type _} @@ -403,8 +430,7 @@ theorem IsIdempotentElem.self_adjoint_is_positive_isOrthogonalProjection_tFAE {E · exact hp.is_positive_iff_self_adjoint tfae_have 2 → 1 · intro h - rw [ContinuousLinearMap.IsOrthogonalProjection, ← - IsIdempotentElem.isSelfAdjoint_iff_ker_isOrtho_to_range _ hp] at h + rw [IsIdempotentElem.isSelfAdjoint_iff_ker_isOrtho_to_range _ hp] exact h.2 tfae_have 1 → 2 · intro h @@ -415,7 +441,7 @@ theorem IsIdempotentElem.self_adjoint_is_positive_isOrthogonalProjection_tFAE {E /-- orthogonal projections are obviously positive -/ theorem orthogonalProjection.is_positive [InnerProductSpace ℂ E] {U : Submodule ℂ E} [CompleteSpace E] [CompleteSpace U] : 0 ≤ U.subtypeL.comp (P U) := - SelfAdjointAndIdempotent.is_positive (orthogonalProjection.idempotent U) + SelfAdjointAndIdempotent.is_positive (orthogonalProjection.isIdempotentElem U) (orthogonalProjection_isSelfAdjoint U) theorem SelfAdjointAndIdempotent.sub_is_positive_of [InnerProductSpace 𝕜 E] [CompleteSpace E] @@ -433,8 +459,8 @@ theorem SelfAdjointAndIdempotent.sub_is_positive_of [InnerProductSpace 𝕜 E] [ theorem orthogonalProjection.sub_is_positive_of [InnerProductSpace ℂ E] {U V : Submodule ℂ E} [CompleteSpace U] [CompleteSpace V] [CompleteSpace E] (h : (↥P U).comp (↥P V) = ↥P U) : 0 ≤ ↥P V - ↥P U := - SelfAdjointAndIdempotent.sub_is_positive_of (orthogonalProjection.idempotent U) - (orthogonalProjection.idempotent V) (orthogonalProjection_isSelfAdjoint U) + SelfAdjointAndIdempotent.sub_is_positive_of (orthogonalProjection.isIdempotentElem U) + (orthogonalProjection.isIdempotentElem V) (orthogonalProjection_isSelfAdjoint U) (orthogonalProjection_isSelfAdjoint V) h /-- given orthogonal projections `Pᵤ,Pᵥ`, @@ -448,19 +474,23 @@ theorem orthogonal_projection_commutes_of_is_idempotent [InnerProductSpace ℂ E have pp : p = U.subtypeL.comp (P U) := rfl have qq : q = V.subtypeL.comp (P V) := rfl simp_rw [← pp, ← qq] at * - have hp : IsIdempotentElem p := orthogonalProjection.idempotent U - have hq : IsIdempotentElem q := orthogonalProjection.idempotent V + have hp : IsIdempotentElem p := orthogonalProjection.isIdempotentElem U + have hq : IsIdempotentElem q := orthogonalProjection.isIdempotentElem V exact coe_inj.mp (LinearMap.commutes_of_isIdempotentElem (IsIdempotentElem.clm_to_lm.mp hp) (IsIdempotentElem.clm_to_lm.mp hq) (IsIdempotentElem.clm_to_lm.mp h)).2 +set_option synthInstance.checkSynthOrder false in +scoped[FiniteDimensional] attribute [instance] FiniteDimensional.complete +open scoped FiniteDimensional + /-- copy of `linear_map.is_positive_iff_exists_adjoint_mul_self` -/ theorem ContinuousLinearMap.isPositive_iff_exists_adjoint_hMul_self [InnerProductSpace 𝕜 E] - [CompleteSpace E] {n : ℕ} [FiniteDimensional 𝕜 E] (hn : FiniteDimensional.finrank 𝕜 E = n) - (T : E →L[𝕜] E) : T.IsPositive ↔ ∃ S : E →L[𝕜] E, T = adjoint S * S := + [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) : + T.IsPositive ↔ ∃ S : E →L[𝕜] E, T = adjoint S * S := by - rw [← IsPositive.toLinearMap, LinearMap.isPositive_iff_exists_adjoint_hMul_self _ hn] + rw [← IsPositive.toLinearMap, LinearMap.isPositive_iff_exists_adjoint_hMul_self] constructor <;> rintro ⟨S, hS⟩ use LinearMap.toContinuousLinearMap S · ext @@ -474,17 +504,16 @@ open RCLike /-- in a finite-dimensional complex Hilbert space `E`, if `p,q` are self-adjoint operators, then `p ≤ q` iff `∀ x ∈ E : ⟪x, p x⟫ ≤ ⟪x, q x⟫` -/ -theorem ContinuousLinearMap.is_positive_le_iff_inner {n : ℕ} [InnerProductSpace ℂ E] - [FiniteDimensional ℂ E] (hn : FiniteDimensional.finrank ℂ E = n) {p q : E →L[ℂ] E} - (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : - p ≤ q ↔ ∀ x : E, re ⟪x, p x⟫_ℂ ≤ re ⟪x, q x⟫_ℂ := +theorem ContinuousLinearMap.is_positive_le_iff_inner [InnerProductSpace 𝕜 E] + [CompleteSpace E] + {p q : E →L[𝕜] E} (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : + p ≤ q ↔ ∀ x : E, re ⟪x, p x⟫_𝕜 ≤ re ⟪x, q x⟫_𝕜 := by - rw [ContinuousLinearMap.IsPositive.hasLe] + rw [ContinuousLinearMap.le_def] constructor · intro h x - obtain ⟨S, hS⟩ := (ContinuousLinearMap.isPositive_iff_exists_adjoint_hMul_self hn _).mp h - rw [← sub_nonneg, ← map_sub, ← inner_sub_right, ← sub_apply, hS, mul_apply, adjoint_inner_right] - exact inner_self_nonneg + rw [← sub_nonneg, ← map_sub, ← inner_sub_right, ← sub_apply] + exact IsPositive.inner_nonneg_right h x · intro h refine' ⟨IsSelfAdjoint.sub hqa hpa, fun x => _⟩ simp_rw [reApplyInnerSelf_apply, sub_apply, inner_sub_left, map_sub, sub_nonneg] @@ -509,15 +538,16 @@ theorem ContinuousLinearMap.hasLe_norm [InnerProductSpace 𝕜 E] [CompleteSpace theorem IsPositive.HasLe.sub [InnerProductSpace 𝕜 E] [CompleteSpace E] {p q : E →L[𝕜] E} : p ≤ q ↔ 0 ≤ q - p := by simp only [LE.le, sub_zero] -theorem self_adjoint_and_idempotent_is_positive_iff_commutes {n : ℕ} [InnerProductSpace ℂ E] - [FiniteDimensional ℂ E] (hn : FiniteDimensional.finrank ℂ E = n) {p q : E →L[ℂ] E} +theorem self_adjoint_and_idempotent_is_positive_iff_commutes + [InnerProductSpace ℂ E] + [CompleteSpace E] {p q : E →L[ℂ] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpa : IsSelfAdjoint p) (hqa : IsSelfAdjoint q) : p ≤ q ↔ q.comp p = p := by rw [← self_adjoint_proj_commutes hpa hqa, IsPositive.HasLe.sub] refine' ⟨fun h => _, fun h => SelfAdjointAndIdempotent.sub_is_positive_of hp hq hpa hqa h⟩ - rw [← ContinuousLinearMap.IsPositive.is_nonneg, ← ContinuousLinearMap.IsPositive.hasLe, - ContinuousLinearMap.is_positive_le_iff_inner hn hpa hqa] at h + rw [← IsPositive.HasLe.sub, + ContinuousLinearMap.is_positive_le_iff_inner hpa hqa] at h symm rw [← sub_eq_zero] nth_rw 1 [← mul_one p] @@ -532,19 +562,19 @@ theorem self_adjoint_and_idempotent_is_positive_iff_commutes {n : ℕ} [InnerPro /-- in a complex-finite-dimensional Hilbert space `E`, we have `Pᵤ ≤ Pᵤ` iff `PᵥPᵤ = Pᵤ` -/ -theorem orthogonal_projection_is_le_iff_commutes {n : ℕ} [InnerProductSpace ℂ E] - {U V : Submodule ℂ E} [CompleteSpace U] [CompleteSpace V] [FiniteDimensional ℂ E] - (hn : FiniteDimensional.finrank ℂ E = n) : ↥P U ≤ ↥P V ↔ (↥P V).comp (↥P U) = ↥P U := - self_adjoint_and_idempotent_is_positive_iff_commutes hn (orthogonalProjection.idempotent U) - (orthogonalProjection.idempotent V) (orthogonalProjection_isSelfAdjoint U) +theorem orthogonal_projection_is_le_iff_commutes [InnerProductSpace ℂ E] + {U V : Submodule ℂ E} [CompleteSpace E] [CompleteSpace U] [CompleteSpace V] : + ↥P U ≤ ↥P V ↔ (↥P V).comp (↥P U) = ↥P U := + self_adjoint_and_idempotent_is_positive_iff_commutes (orthogonalProjection.isIdempotentElem U) + (orthogonalProjection.isIdempotentElem V) (orthogonalProjection_isSelfAdjoint U) (orthogonalProjection_isSelfAdjoint V) -theorem orthogonalProjection.is_le_iff_subset {n : ℕ} [InnerProductSpace ℂ E] {U V : Submodule ℂ E} - [CompleteSpace U] [CompleteSpace V] [FiniteDimensional ℂ E] - (hn : FiniteDimensional.finrank ℂ E = n) : ↥P U ≤ ↥P V ↔ U ≤ V := by - simp_rw [orthogonal_projection_is_le_iff_commutes hn, ← coe_inj, coe_comp, +theorem orthogonalProjection.is_le_iff_subset [InnerProductSpace ℂ E] {U V : Submodule ℂ E} + [CompleteSpace E] + [CompleteSpace U] [CompleteSpace V] : ↥P U ≤ ↥P V ↔ U ≤ V := by + simp_rw [orthogonal_projection_is_le_iff_commutes, ← coe_inj, coe_comp, IsIdempotentElem.comp_idempotent_iff - (IsIdempotentElem.clm_to_lm.mp (orthogonalProjection.idempotent V)), + (IsIdempotentElem.clm_to_lm.mp (orthogonalProjection.isIdempotentElem V)), Submodule.map_top, range_toLinearMap, orthogonalProjection.range] theorem Submodule.map_to_linearMap [Module 𝕜 E] {p : E →L[𝕜] E} {U : Submodule 𝕜 E} : @@ -577,29 +607,31 @@ def orthogonalProjection.IsMinimalProjection [InnerProductSpace 𝕜 E] (U : Sub [CompleteSpace U] : Prop := FiniteDimensional.finrank 𝕜 U = 1 -/-- given self-adjoint operators `p,q` we have - `p = q` iff `p ≤ q` and `q ≤ p` -/ -@[simp] -theorem IsSelfAdjoint.HasLe.le_antisymm_iff [InnerProductSpace 𝕜 E] [CompleteSpace E] - {p q : E →L[𝕜] E} (hp : IsSelfAdjoint p) (hq : IsSelfAdjoint q) : p = q ↔ p ≤ q ∧ q ≤ p := - by - refine' ⟨fun h => _, fun h => IsSelfAdjoint.HasLe.le_antisymm hp hq h.1 h.2⟩ - rw [h, and_self_iff] +-- /-- given self-adjoint operators `p,q` we have + -- `p = q` iff `p ≤ q` and `q ≤ p` -/ +-- @[simp] +-- theorem IsSelfAdjoint.HasLe.le_antisymm_iff [InnerProductSpace 𝕜 E] [CompleteSpace E] +-- {p q : E →L[𝕜] E} : p = q ↔ p ≤ q ∧ q ≤ p := +-- by +-- refine' ⟨fun h => _, fun h => le_antisymm h.1 h.2⟩ +-- . rw [h, and_self_iff] open FiniteDimensional /-- when a submodule `U` has dimension `1`, then for any submodule `V`, we have `V ≤ U` if and only if `V = U` or `V = 0` -/ -theorem Submodule.le_finrank_one [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] - (U V : Submodule 𝕜 E) (hU : finrank 𝕜 U = 1) : V ≤ U ↔ V = U ∨ V = 0 := +theorem Submodule.le_finrank_one + {R M : Type*} [Field R] [AddCommGroup M] [Module R M] + (U V : Submodule R M) [Module.Finite R ↥U] [Module.Finite R ↥V] + (hU : FiniteDimensional.finrank R U = 1) : V ≤ U ↔ V = U ∨ V = 0 := by simp_rw [Submodule.zero_eq_bot] constructor · intro h - have : finrank 𝕜 V ≤ 1 := by + have : finrank R V ≤ 1 := by rw [← hU] apply Submodule.finrank_le_finrank_of_le h - have : finrank 𝕜 V = 0 ∨ finrank 𝕜 V = 1 := Order.le_succ_bot_iff.mp this + have : finrank R V = 0 ∨ finrank R V = 1 := Order.le_succ_bot_iff.mp this rcases this with (this_1 | this_1) · simp only [Submodule.finrank_eq_zero] at this_1 right @@ -616,17 +648,18 @@ theorem Submodule.le_finrank_one [InnerProductSpace 𝕜 E] [FiniteDimensional /-- for orthogonal projections `Pᵤ,Pᵥ`, if `Pᵤ` is a minimal orthogonal projection, then for any `Pᵥ` if `Pᵥ ≤ Pᵤ` and `Pᵥ ≠ 0`, then `Pᵥ = Pᵤ` -/ -theorem orthogonalProjection.isMinimalProjection_of {n : ℕ} [InnerProductSpace ℂ E] - [FiniteDimensional ℂ E] (hn : finrank ℂ E = n) (U W : Submodule ℂ E) - (hU : orthogonalProjection.IsMinimalProjection U) (hW : ↥P W ≤ ↥P U) (h : ↥P W ≠ 0) : +theorem orthogonalProjection.isMinimalProjection_of + [InnerProductSpace ℂ E] + [CompleteSpace E] + (U W : Submodule ℂ E) [Module.Finite ℂ ↥U] [Module.Finite ℂ ↥W] + (hU : orthogonalProjection.IsMinimalProjection U) + (hW : ↥P W ≤ ↥P U) (h : ↥P W ≠ 0) : ↥P W = ↥P U := by - simp_rw [orthogonalProjection'_eq, - IsSelfAdjoint.HasLe.le_antisymm_iff (orthogonalProjection_isSelfAdjoint W) - (orthogonalProjection_isSelfAdjoint U), + simp_rw [orthogonalProjection'_eq, le_antisymm_iff, ← orthogonalProjection'_eq] refine' ⟨hW, _⟩ - rw [orthogonalProjection.is_le_iff_subset hn] at hW ⊢ + rw [orthogonalProjection.is_le_iff_subset] at hW ⊢ have := Submodule.finrank_le_finrank_of_le hW simp_rw [orthogonalProjection.IsMinimalProjection] at hU rw [Submodule.le_finrank_one U W hU] at hW @@ -702,16 +735,30 @@ theorem rankOne.isMinimalProjection' [InnerProductSpace ℂ E] [CompleteSpace E] exact rankOne.isMinimalProjection y hy · contradiction +lemma LinearMap.range_of_isProj {R M : Type*} [CommSemiring R] [AddCommGroup M] [Module R M] + {p : M →ₗ[R] M} {U : Submodule R M} + (hp : LinearMap.IsProj U p) : + LinearMap.range p = U := +by + ext x + rw [mem_range] + refine ⟨λ ⟨y, hy⟩ => ?_, λ h => ⟨x, hp.map_id _ h⟩⟩ + . rw [← hy] + exact hp.map_mem y + +open scoped FiniteDimensional +set_option synthInstance.maxHeartbeats 200000 in /-- a linear operator is an orthogonal projection onto a submodule, if and only if it is self-adjoint and idempotent; so it always suffices to say `p = p⋆ = p²` -/ -theorem orthogonal_projection_iff [InnerProductSpace 𝕜 E] [CompleteSpace E] [FiniteDimensional 𝕜 E] - {p : E →L[𝕜] E} : (∃ U : Submodule 𝕜 E, ↥P U = p) ↔ IsSelfAdjoint p ∧ IsIdempotentElem p := +theorem orthogonal_projection_iff [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] + {p : E →L[𝕜] E} : (∃ (U : Submodule 𝕜 E), --(hU : CompleteSpace U) + ↥P U = p) + ↔ IsSelfAdjoint p ∧ IsIdempotentElem p := by constructor - · rintro ⟨U, hp⟩ - rw [← hp] - exact ⟨orthogonalProjection_isSelfAdjoint _, orthogonalProjection.idempotent _⟩ + · rintro ⟨U, rfl⟩ + exact ⟨orthogonalProjection_isSelfAdjoint _, orthogonalProjection.isIdempotentElem _⟩ · rintro ⟨h1, h2⟩ simp_rw [IsIdempotentElem, mul_def, ContinuousLinearMap.ext_iff, ← ContinuousLinearMap.coe_coe, coe_comp, ← LinearMap.ext_iff] at h2 @@ -722,27 +769,31 @@ theorem orthogonal_projection_iff [InnerProductSpace 𝕜 E] [CompleteSpace E] [ orthogonalProjection'_eq_linear_proj', ← hp'] rw [← LinearMap.linearProjOfIsCompl_of_proj p' (isProj'_eq hp)] use W - intro x - simp_rw [LinearMap.coe_comp, Submodule.coeSubtype] - suffices this : LinearMap.ker p' = Wᗮ - by simp_rw [this]; rfl - ext y - simp_rw [LinearMap.mem_ker, Submodule.mem_orthogonal] - constructor - · intro hp'y u hu - rw [← hp.2 u hu, ContinuousLinearMap.coe_coe, ← adjoint_inner_right, - IsSelfAdjoint.adjoint_eq h1, ← ContinuousLinearMap.coe_coe, ← isProj'_apply hp, ← hp', hp'y, - Submodule.coe_zero, inner_zero_right] - · intro h - rw [← Submodule.coe_eq_zero, ← @inner_self_eq_zero 𝕜, isProj'_apply hp, - ContinuousLinearMap.coe_coe, ← adjoint_inner_left, IsSelfAdjoint.adjoint_eq h1, ← - ContinuousLinearMap.coe_coe, ← LinearMap.comp_apply, h2, - h _ (LinearMap.IsProj.map_mem hp _)] - + . intro x + simp_rw [LinearMap.coe_comp, Submodule.coeSubtype] + suffices this : LinearMap.ker p' = Wᗮ + by simp_rw [this]; rfl + ext y + simp_rw [LinearMap.mem_ker, Submodule.mem_orthogonal] + constructor + · intro hp'y u hu + rw [← hp.2 u hu, ContinuousLinearMap.coe_coe, ← adjoint_inner_right, + IsSelfAdjoint.adjoint_eq h1, ← ContinuousLinearMap.coe_coe, ← isProj'_apply hp, ← hp', hp'y, + Submodule.coe_zero, inner_zero_right] + · intro h + rw [← Submodule.coe_eq_zero, ← @inner_self_eq_zero 𝕜, isProj'_apply hp, + ContinuousLinearMap.coe_coe, ← adjoint_inner_left, IsSelfAdjoint.adjoint_eq h1, ← + ContinuousLinearMap.coe_coe, ← LinearMap.comp_apply, h2, + h _ (LinearMap.IsProj.map_mem hp _)] + -- . have : p = W.subtype ∘ₗ p' := by rfl + -- rw [← LinearMap.range_of_isProj hp] + -- simp only [range_toLinearMap] + +set_option synthInstance.maxHeartbeats 200000 in /-- a linear operator is an orthogonal projection onto a submodule, if and only if it is a self-adjoint linear projection onto the submodule; also see `orthogonal_projection_iff` -/ -theorem orthogonal_projection_iff' [InnerProductSpace 𝕜 E] [CompleteSpace E] [FiniteDimensional 𝕜 E] +theorem orthogonal_projection_iff' [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {p : E →L[𝕜] E} (U : Submodule 𝕜 E) : ↥P U = p ↔ IsSelfAdjoint p ∧ LinearMap.IsProj U p := by constructor @@ -788,8 +839,9 @@ theorem orthogonal_projection_iff' [InnerProductSpace 𝕜 E] [CompleteSpace E] ContinuousLinearMap.coe_coe, ← adjoint_inner_left, IsSelfAdjoint.adjoint_eq h, ← ContinuousLinearMap.comp_apply, this, h' _ (LinearMap.IsProj.map_mem h2 _)] -theorem orthogonalProjection.isMinimalProjection_to_clm [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) - [CompleteSpace E] [FiniteDimensional 𝕜 E] : +set_option synthInstance.maxHeartbeats 200000 in +theorem orthogonalProjection.isMinimalProjection_to_clm [InnerProductSpace 𝕜 E] + [FiniteDimensional 𝕜 E] (U : Submodule 𝕜 E) : (↥P U).IsMinimalProjection U ↔ orthogonalProjection.IsMinimalProjection U := by refine' ⟨fun h => h.2.1, fun h => _⟩ @@ -812,7 +864,8 @@ theorem Submodule.isOrtho_iff_inner_eq' {𝕜 E : Type _} [RCLike 𝕜] [NormedA /-- `U` and `W` are mutually orthogonal if and only if `(P U).comp (P W) = 0`, where `P U` is `orthogonal_projection U` -/ theorem Submodule.is_pairwise_orthogonal_iff_orthogonal_projection_comp_eq_zero - [InnerProductSpace 𝕜 E] (U W : Submodule 𝕜 E) [CompleteSpace U] [CompleteSpace W] : + [InnerProductSpace 𝕜 E] (U W : Submodule 𝕜 E) + [HasOrthogonalProjection U] [HasOrthogonalProjection W] : U ⟂ W ↔ (↥P U).comp (↥P W) = 0 := by rw [Submodule.isOrtho_iff_inner_eq'] @@ -831,17 +884,18 @@ theorem Submodule.is_pairwise_orthogonal_iff_orthogonal_projection_comp_eq_zero ContinuousLinearMap.zero_apply, inner_zero_right] -- -theorem orthogonalProjection.orthogonal_complement_eq [InnerProductSpace 𝕜 E] [CompleteSpace E] - (U : Submodule 𝕜 E) [CompleteSpace ↥U] : ↥P Uᗮ = 1 - ↥P U := +theorem orthogonalProjection.orthogonal_complement_eq [InnerProductSpace 𝕜 E] + (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : ↥P Uᗮ = 1 - ↥P U := by have : 1 = id 𝕜 E := rfl simp_rw [this, id_eq_sum_orthogonalProjection_self_orthogonalComplement U, orthogonalProjection'_eq, add_sub_cancel'] -example {n : ℕ} [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {U W : Submodule ℂ E} - (h : finrank ℂ E = n) : (↥P U).comp (↥P W) = 0 ↔ ↥P U + ↥P W ≤ 1 := by +example [InnerProductSpace ℂ E] {U W : Submodule ℂ E} [CompleteSpace E] [CompleteSpace U] + [CompleteSpace W] : + (↥P U).comp (↥P W) = 0 ↔ ↥P U + ↥P W ≤ 1 := by simp_rw [← Submodule.is_pairwise_orthogonal_iff_orthogonal_projection_comp_eq_zero, - Submodule.isOrtho_iff_le, ← orthogonalProjection.is_le_iff_subset h, + Submodule.isOrtho_iff_le, ← orthogonalProjection.is_le_iff_subset, orthogonalProjection.orthogonal_complement_eq, add_comm (↥P U) (↥P W), LE.le, sub_add_eq_sub_sub] diff --git a/Monlib/LinearAlgebra/MyIps/Nontracial.lean b/Monlib/LinearAlgebra/MyIps/Nontracial.lean index dcac571..10ed991 100644 --- a/Monlib/LinearAlgebra/MyIps/Nontracial.lean +++ b/Monlib/LinearAlgebra/MyIps/Nontracial.lean @@ -47,9 +47,6 @@ variable [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} {k : Type _} [Fintype k] [DecidableEq k] {s : k → Type _} [∀ i, Fintype (s i)] [∀ i, DecidableEq (s i)] {ψ : ∀ i, Module.Dual ℂ (Matrix (s i) (s i) ℂ)} --- :TODO: make this a def: --- local notation "PiMat ℂ k s" => Π i, Matrix (s i) (s i) ℂ - open scoped Kronecker Matrix BigOperators TensorProduct Functional open Module.Dual @@ -185,7 +182,7 @@ theorem Qam.Nontracial.mul_comp_mul_adjoint [hφ : φ.IsFaithfulPosMap] : Finset.mem_univ, if_true] simp_rw [← Finset.mul_sum, ← trace_iff φ.matrix⁻¹, mul_comm] -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y theorem Module.Dual.IsFaithfulPosMap.inner_coord' [hφ : φ.IsFaithfulPosMap] (ij : n × n) (x : ℍ) : ⟪hφ.basis ij, x⟫_ℂ = (x * hφ.matrixIsPosDef.rpow (1 / 2)) ij.1 ij.2 := by @@ -193,7 +190,7 @@ theorem Module.Dual.IsFaithfulPosMap.inner_coord' [hφ : φ.IsFaithfulPosMap] (i IsFaithfulPosMap.inner_coord _ ij x] theorem rankOne_toMatrix [hφ : φ.IsFaithfulPosMap] (a b : Matrix n n ℂ) : - hφ.toMatrix (|a⟩⟨b| : l(ℍ)) = + hφ.toMatrix ((|a⟩⟨b|) : l(ℍ)) = col (reshape (a * hφ.matrixIsPosDef.rpow (1 / 2))) * (col (reshape (b * hφ.matrixIsPosDef.rpow (1 / 2))))ᴴ := by @@ -738,7 +735,7 @@ theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_right_inner {k : Type _} [F ⟪y, includeBlock x⟫_ℂ = ⟪y i, x⟫_ℂ := by rw [← inner_conj_symm, pi.IsFaithfulPosMap.includeBlock_left_inner, inner_conj_symm] -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y theorem pi_includeBlock_right_rankOne [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (a : PiMat ℂ k s) {i : k} (b : ℍ_ i) (c : PiMat ℂ k s) (j : k) : |a⟩⟨includeBlock b| c j = ⟪b, c i⟫_ℂ • a j := by @@ -1260,15 +1257,20 @@ theorem norm_hMul_norm_eq_norm_tmul {𝕜 B C : Type _} [RCLike 𝕜] [NormedAdd -- instance Pi.matrix.continuousSMul : ContinuousSMul ℂ PiMat ℂ k s := by infer_instance -theorem Pi.rankOneLm_real_apply [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (x y : PiMat ℂ k s) : - LinearMap.real (rankOneLm x y : (PiMat ℂ k s) →ₗ[ℂ] (PiMat ℂ k s)) = - (rankOneLm (star x) (Module.Dual.pi.IsFaithfulPosMap.sig hψ (-1) (star y))) := +theorem Pi.rankOneLm_real_apply {k₂ : Type*} [Fintype k₂] [DecidableEq k₂] + {s₂ : k₂ → Type*} [Π i, Fintype (s₂ i)] [Π i, DecidableEq (s₂ i)] + {φ : Π i, Module.Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} + [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + [hφ : ∀ i, (φ i).IsFaithfulPosMap] + (x : PiMat ℂ k s) (y : PiMat ℂ k₂ s₂) : + LinearMap.real (rankOneLm x y : (PiMat ℂ k₂ s₂) →ₗ[ℂ] (PiMat ℂ k s)) = + (rankOneLm (star x) (Module.Dual.pi.IsFaithfulPosMap.sig hφ (-1) (star y))) := by rw [LinearMap.ext_iff] intro x_1 simp_rw [rankOneLm_apply, LinearMap.real_apply, rankOneLm_apply, star_smul, ← starRingEnd_apply] - have := @Pi.inner_symm _ _ _ _ _ _ hψ (star x_1) y + have := @Pi.inner_symm _ _ _ _ _ _ hφ (star x_1) y rw [star_star] at this rw [← this, inner_conj_symm] @@ -1323,7 +1325,10 @@ theorem Module.Dual.pi.IsFaithfulPosMap.sig_zero' [hψ : ∀ i, (ψ i).IsFaithfu rw [Module.Dual.pi.IsFaithfulPosMap.sig_zero] rfl -theorem Pi.comp_sig_eq_iff [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (t : ℝ) (f g : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k s) : +theorem Pi.comp_sig_eq_iff + {A : Type*} [AddCommMonoid A] [Module ℂ A] + [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + (t : ℝ) (f g : PiMat ℂ k s →ₗ[ℂ] A) : f ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hψ t).toLinearMap = g ↔ f = g ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hψ (-t)).toLinearMap := by @@ -1334,7 +1339,8 @@ theorem Pi.comp_sig_eq_iff [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (t : ℝ) (f g all_goals rw [Module.Dual.pi.IsFaithfulPosMap.sig_zero', AlgEquiv.one_toLinearMap, LinearMap.comp_one] -theorem Pi.sig_comp_eq_iff [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (t : ℝ) (f g : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k s) : +theorem Pi.sig_comp_eq_iff {A : Type*} [AddCommMonoid A] [Module ℂ A] + [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (t : ℝ) (f g : A →ₗ[ℂ] PiMat ℂ k s) : (Module.Dual.pi.IsFaithfulPosMap.sig hψ t).toLinearMap ∘ₗ f = g ↔ f = (Module.Dual.pi.IsFaithfulPosMap.sig hψ (-t)).toLinearMap ∘ₗ g := by @@ -1345,17 +1351,24 @@ theorem Pi.sig_comp_eq_iff [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (t : ℝ) (f g all_goals rw [Module.Dual.pi.IsFaithfulPosMap.sig_zero', AlgEquiv.one_toLinearMap, LinearMap.one_comp] -theorem rankOneLm_eq_rankOne {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] (x y : E) : (rankOneLm x y : E →ₗ[𝕜] E) = (rankOne x y : E →L[𝕜] E) := +theorem rankOneLm_eq_rankOne {𝕜 E E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E] + [NormedAddCommGroup E₂] + [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E₂] (x : E) (y : E₂) : (rankOneLm x y : E₂ →ₗ[𝕜] E) = (rankOne x y : E₂ →L[𝕜] E) := rfl -theorem LinearMap.pi.adjoint_real_eq {ψ : ∀ i, Module.Dual ℂ (Matrix (s i) (s i) ℂ)} - [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k s) : +theorem LinearMap.pi.adjoint_real_eq {k₂ : Type*} [Fintype k₂] [DecidableEq k₂] + {s₂ : k₂ → Type*} [Π i, Fintype (s₂ i)] [Π i, DecidableEq (s₂ i)] + {φ : Π i, Module.Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} + {ψ : ∀ i, Module.Dual ℂ (Matrix (s i) (s i) ℂ)} + [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + [hφ : ∀ i, (φ i).IsFaithfulPosMap] (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) : (LinearMap.adjoint f).real = (Module.Dual.pi.IsFaithfulPosMap.sig hψ 1).toLinearMap ∘ₗ - (LinearMap.adjoint f.real) ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hψ (-1)).toLinearMap := + (LinearMap.adjoint f.real) ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hφ (-1)).toLinearMap := by - rw [← ext_inner_map] + rw [LinearMap.ext_iff] + intro x + apply ext_inner_right ℂ intro u nth_rw 1 [Pi.inner_symm] simp_rw [LinearMap.real_apply, star_star, LinearMap.adjoint_inner_right] diff --git a/Monlib/LinearAlgebra/MyIps/Pos.lean b/Monlib/LinearAlgebra/MyIps/Pos.lean index 5cca239..1722e70 100644 --- a/Monlib/LinearAlgebra/MyIps/Pos.lean +++ b/Monlib/LinearAlgebra/MyIps/Pos.lean @@ -104,7 +104,7 @@ local notation "α" => IsSymmetric.eigenvalues local notation "√" => Real.sqrt -variable {n : ℕ} [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) +variable [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) open scoped ComplexOrder @@ -127,32 +127,32 @@ open scoped BigOperators we can write `T x = ∑ i, √α i • √α i • ⟪e i, x⟫` for any `x ∈ E`, where `α i` are the eigenvalues of `T` and `e i` are the respective eigenvectors that form an eigenbasis (`isSymmetric.eigenvector_basis`) -/ -theorem sq_mul_sq_eq_self_of_isSymmetric_and_nonneg_spectrum [DecidableEq 𝕜] - (hn : FiniteDimensional.finrank 𝕜 E = n) (hT : T.IsSymmetric) (hT1 : (spectrum 𝕜 T).IsNonneg) - (v : E) : T v = ∑ i, (√ (α hT hn i) • √ (α hT hn i) : 𝕜) • ⟪e hT hn i, v⟫ • e hT hn i := +theorem sq_mul_sq_eq_self_of_isSymmetric_and_nonneg_spectrum + (hT : T.IsSymmetric) (hT1 : (spectrum 𝕜 T).IsNonneg) + (v : E) : T v = ∑ i, (√ (α hT rfl i) • √ (α hT rfl i) : 𝕜) • ⟪e hT rfl i, v⟫ • e hT rfl i := by - have : ∀ i : Fin n, 0 ≤ α hT hn i := fun i => + have : ∀ i, 0 ≤ α hT rfl i := fun i => by - specialize hT1 (hT.eigenvalues hn i) + specialize hT1 (hT.eigenvalues rfl i) simp only [zero_le_real, ofReal_re, true_and_iff] at hT1 apply hT1 - (Module.End.hasEigenvalue_iff_mem_spectrum.mp (hT.hasEigenvalue_eigenvalues hn i)) + (Module.End.hasEigenvalue_iff_mem_spectrum.mp (hT.hasEigenvalue_eigenvalues rfl i)) calc - T v = ∑ i, ⟪e hT hn i, v⟫ • T (e hT hn i) := by + T v = ∑ i, ⟪e hT rfl i, v⟫ • T (e hT rfl i) := by simp_rw [← OrthonormalBasis.repr_apply_apply, ← map_smul_of_tower, ← map_sum, - OrthonormalBasis.sum_repr (e hT hn) v] - _ = ∑ i, (√ (α hT hn i) • √ (α hT hn i) : 𝕜) • ⟪e hT hn i, v⟫ • e hT hn i := by + OrthonormalBasis.sum_repr (e hT rfl) v] + _ = ∑ i, (√ (α hT rfl i) • √ (α hT rfl i) : 𝕜) • ⟪e hT rfl i, v⟫ • e hT rfl i := by simp_rw [IsSymmetric.apply_eigenvectorBasis, smul_smul, real_smul_ofReal, ← ofReal_mul, ← Real.sqrt_mul (this _), Real.sqrt_mul_self (this _), mul_comm] /-- given a symmetric linear map `T` and a real number `r`, we can define a linear map `S` such that `S = T ^ r` -/ -noncomputable def rePow [DecidableEq 𝕜] (hn : FiniteDimensional.finrank 𝕜 E = n) +noncomputable def rePow (hT : T.IsSymmetric) (r : ℝ) : E →ₗ[𝕜] E where - toFun v := ∑ i : Fin n, (((α hT hn i : ℝ) ^ r : ℝ) : 𝕜) • ⟪e hT hn i, v⟫ • e hT hn i + toFun v := ∑ i, (((α hT rfl i : ℝ) ^ r : ℝ) : 𝕜) • ⟪e hT rfl i, v⟫ • e hT rfl i map_add' x y := by simp_rw [inner_add_right, add_smul, smul_add, Finset.sum_add_distrib] map_smul' r x := by simp_rw [inner_smul_right, ← smul_smul, Finset.smul_sum, RingHom.id_apply, smul_smul, ← @@ -160,65 +160,65 @@ noncomputable def rePow [DecidableEq 𝕜] (hn : FiniteDimensional.finrank 𝕜 section -noncomputable def cpow [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [DecidableEq ℂ] - (hn : FiniteDimensional.finrank ℂ E = n) (T : E →ₗ[ℂ] E) (hT : T.IsPositive) (c : ℂ) : E →ₗ[ℂ] E +noncomputable def cpow [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] + (T : E →ₗ[ℂ] E) (hT : T.IsPositive) (c : ℂ) : E →ₗ[ℂ] E where - toFun v := ∑ i : Fin n, (α hT.1 hn i ^ c : ℂ) • ⟪e hT.1 hn i, v⟫_ℂ • e hT.1 hn i + toFun v := ∑ i, (α hT.1 rfl i ^ c : ℂ) • ⟪e hT.1 rfl i, v⟫_ℂ • e hT.1 rfl i map_add' x y := by simp_rw [inner_add_right, add_smul, smul_add, Finset.sum_add_distrib] map_smul' r x := by simp_rw [inner_smul_right, ← smul_smul, Finset.smul_sum, RingHom.id_apply, smul_smul, ← mul_assoc, mul_comm] -theorem cpow_apply [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [DecidableEq ℂ] - (hn : FiniteDimensional.finrank ℂ E = n) (T : E →ₗ[ℂ] E) (hT : T.IsPositive) (c : ℂ) (v : E) : - T.cpow hn hT c v = ∑ i : Fin n, (α hT.1 hn i ^ c : ℂ) • ⟪e hT.1 hn i, v⟫_ℂ • e hT.1 hn i := +theorem cpow_apply [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] + (T : E →ₗ[ℂ] E) (hT : T.IsPositive) (c : ℂ) (v : E) : + T.cpow hT c v = ∑ i, (α hT.1 rfl i ^ c : ℂ) • ⟪e hT.1 rfl i, v⟫_ℂ • e hT.1 rfl i := rfl end -theorem rePow_apply [DecidableEq 𝕜] (hn : FiniteDimensional.finrank 𝕜 E = n) (hT : T.IsSymmetric) +theorem rePow_apply (hT : T.IsSymmetric) (r : ℝ) (v : E) : - T.rePow hn hT r v = ∑ i : Fin n, (((α hT hn i : ℝ) ^ r : ℝ) : 𝕜) • ⟪e hT hn i, v⟫ • e hT hn i := + T.rePow hT r v = ∑ i, (((α hT rfl i : ℝ) ^ r : ℝ) : 𝕜) • ⟪e hT rfl i, v⟫ • e hT rfl i := rfl /-- the square root of a symmetric linear map can then directly be defined with `re_pow` -/ -noncomputable def sqrt [DecidableEq 𝕜] (hn : FiniteDimensional.finrank 𝕜 E = n) +noncomputable def sqrt (h : T.IsSymmetric) : E →ₗ[𝕜] E := - T.rePow hn h (1 / 2 : ℝ) + T.rePow h (1 / 2 : ℝ) /-- the square root of a symmetric linear map `T` is written as `T x = ∑ i, √ (α i) • ⟪e i, x⟫ • e i` for any `x ∈ E`, where `α i` are the eigenvalues of `T` and `e i` are the respective eigenvectors that form an eigenbasis (`isSymmetric.eigenvector_basis`) -/ -theorem sqrt_apply (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq 𝕜] (hT : T.IsSymmetric) - (x : E) : T.sqrt hn hT x = ∑ i, (√ (α hT hn i) : 𝕜) • ⟪e hT hn i, x⟫ • e hT hn i := by +theorem sqrt_apply (hT : T.IsSymmetric) + (x : E) : T.sqrt hT x = ∑ i, (√ (α hT rfl i) : 𝕜) • ⟪e hT rfl i, x⟫ • e hT rfl i := by simp_rw [Real.sqrt_eq_rpow _]; rfl /-- given a symmetric linear map `T` with a non-negative spectrum, the square root of `T` composed with itself equals itself, i.e., `T.sqrt ^ 2 = T` -/ -theorem sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum [DecidableEq 𝕜] - (hn : FiniteDimensional.finrank 𝕜 E = n) (hT : T.IsSymmetric) (hT1 : (spectrum 𝕜 T).IsNonneg) : - T.sqrt hn hT ^ 2 = T := by +theorem sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum + (hT : T.IsSymmetric) (hT1 : (spectrum 𝕜 T).IsNonneg) : + T.sqrt hT ^ 2 = T := by simp_rw [pow_two, mul_eq_comp, LinearMap.ext_iff, comp_apply, sqrt_apply, inner_sum, inner_smul_real_right, smul_smul, inner_smul_right, ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.repr_self, EuclideanSpace.single_apply, mul_boole, smul_ite, smul_zero, Finset.sum_ite_eq, Finset.mem_univ, if_true, Algebra.mul_smul_comm, - sq_mul_sq_eq_self_of_isSymmetric_and_nonneg_spectrum T hn hT hT1, + sq_mul_sq_eq_self_of_isSymmetric_and_nonneg_spectrum T hT hT1, OrthonormalBasis.repr_apply_apply, ← smul_eq_mul, ← smul_assoc, forall_const] /-- given a symmetric linear map `T`, we have that its root is positive -/ -theorem IsSymmetric.sqrtIsPositive [DecidableEq 𝕜] (hn : FiniteDimensional.finrank 𝕜 E = n) - (hT : T.IsSymmetric) : (T.sqrt hn hT).IsPositive := +theorem IsSymmetric.sqrtIsPositive + (hT : T.IsSymmetric) : (T.sqrt hT).IsPositive := by - have : (T.sqrt hn hT).IsSymmetric := by + have : (T.sqrt hT).IsSymmetric := by intro x y - simp_rw [sqrt_apply T hn hT, inner_sum, sum_inner, smul_smul, inner_smul_right, inner_smul_left] - have : ∀ i : Fin n, conj (√ (α hT hn i) : 𝕜) = (√ (α hT hn i) : 𝕜) := fun i => by + simp_rw [sqrt_apply T hT, inner_sum, sum_inner, smul_smul, inner_smul_right, inner_smul_left] + have : ∀ i, conj (√ (α hT rfl i) : 𝕜) = (√ (α hT rfl i) : 𝕜) := fun i => by simp_rw [conj_eq_iff_re, ofReal_re] - simp_rw [mul_assoc, map_mul, this _, inner_conj_symm, mul_comm ⟪e hT hn _, y⟫ _, ← mul_assoc] + simp_rw [mul_assoc, map_mul, this _, inner_conj_symm, mul_comm ⟪e hT rfl _, y⟫ _, ← mul_assoc] refine' ⟨this, _⟩ intro x - simp_rw [sqrt_apply _ hn hT, inner_sum, map_sum, inner_smul_right] + simp_rw [sqrt_apply _ hT, inner_sum, map_sum, inner_smul_right] apply Finset.sum_nonneg' intro i simp_rw [← inner_conj_symm x _, ← OrthonormalBasis.repr_apply_apply, mul_conj, ← ofReal_pow, ← ofReal_mul, @@ -228,30 +228,30 @@ theorem IsSymmetric.sqrtIsPositive [DecidableEq 𝕜] (hn : FiniteDimensional.fi /-- `T` is positive if and only if `T` is symmetric (which is automatic from the definition of positivity) and has a non-negative spectrum -/ -theorem isPositive_iff_isSymmetric_and_nonneg_spectrum (hn : FiniteDimensional.finrank 𝕜 E = n) : +theorem isPositive_iff_isSymmetric_and_nonneg_spectrum : T.IsPositive ↔ T.IsSymmetric ∧ (spectrum 𝕜 T).IsNonneg := by classical refine' ⟨fun h => ⟨h.1, fun μ hμ => IsPositive.nonneg_spectrum T h μ hμ⟩, fun h => ⟨h.1, _⟩⟩ intro x - rw [← sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum T hn h.1 h.2, pow_two, mul_apply, ← + rw [← sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum T h.1 h.2, pow_two, mul_apply, ← adjoint_inner_left, isSelfAdjoint_iff'.mp - ((isSymmetric_iff_isSelfAdjoint _).mp (IsSymmetric.sqrtIsPositive T hn h.1).1)] + ((isSymmetric_iff_isSelfAdjoint _).mp (IsSymmetric.sqrtIsPositive T h.1).1)] exact inner_self_nonneg /-- `T` is positive if and only if there exists a linear map `S` such that `T = S.adjoint * S` -/ -theorem isPositive_iff_exists_adjoint_hMul_self (hn : FiniteDimensional.finrank 𝕜 E = n) : +theorem isPositive_iff_exists_adjoint_hMul_self : T.IsPositive ↔ ∃ S : E →ₗ[𝕜] E, T = adjoint S * S := by classical constructor - · rw [isPositive_iff_isSymmetric_and_nonneg_spectrum T hn] + · rw [isPositive_iff_isSymmetric_and_nonneg_spectrum T] rintro ⟨hT, hT1⟩ - use T.sqrt hn hT + use T.sqrt hT rw [isSelfAdjoint_iff'.mp - ((isSymmetric_iff_isSelfAdjoint _).mp (IsSymmetric.sqrtIsPositive T hn hT).1), + ((isSymmetric_iff_isSelfAdjoint _).mp (IsSymmetric.sqrtIsPositive T hT).1), ← pow_two] - exact (sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum T hn hT hT1).symm + exact (sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum T hT hT1).symm · intro h rcases h with ⟨S, rfl⟩ refine' ⟨isSymmetric_adjoint_mul_self S, _⟩ @@ -294,23 +294,21 @@ theorem IsPositive.adjointConj [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] E) simp_rw [comp_apply, adjoint_inner_right] exact h.2 _ -variable (hn : FiniteDimensional.finrank 𝕜 E = n) - -local notation "√T⋆" T => LinearMap.sqrt ((LinearMap.adjoint T) ∘ₗ T) hn (isSymmetric_adjoint_mul_self T) +local notation "√T⋆" T => LinearMap.sqrt ((LinearMap.adjoint T) ∘ₗ T) (isSymmetric_adjoint_mul_self T) /-- we have `(T.adjoint.comp T).sqrt` is positive, given any linear map `T` -/ -theorem sqrtAdjointSelfIsPositive [DecidableEq 𝕜] (T : E →ₗ[𝕜] E) : (√T⋆T).IsPositive := - IsSymmetric.sqrtIsPositive _ hn (isSymmetric_adjoint_mul_self T) +theorem sqrtAdjointSelfIsPositive (T : E →ₗ[𝕜] E) : (√T⋆T).IsPositive := + IsSymmetric.sqrtIsPositive _ (isSymmetric_adjoint_mul_self T) /-- given any linear map `T` and `x ∈ E` we have `‖(T.adjoint.comp T).sqrt x‖ = ‖T x‖` -/ -theorem norm_of_sqrt_adjoint_mul_self_eq [DecidableEq 𝕜] (T : E →ₗ[𝕜] E) (x : E) : +theorem norm_of_sqrt_adjoint_mul_self_eq (T : E →ₗ[𝕜] E) (x : E) : ‖(√T⋆T) x‖ = ‖T x‖ := by simp_rw [← sq_eq_sq (norm_nonneg _) (norm_nonneg _), ← @inner_self_eq_norm_sq 𝕜, ← adjoint_inner_left, isSelfAdjoint_iff'.mp - ((isSymmetric_iff_isSelfAdjoint _).mp (sqrtAdjointSelfIsPositive hn T).1), + ((isSymmetric_iff_isSelfAdjoint _).mp (sqrtAdjointSelfIsPositive T).1), ← mul_eq_comp, ← mul_apply, ← pow_two, mul_eq_comp] congr apply sqrt_sq_eq_self_of_isSymmetric_and_nonneg_spectrum @@ -319,12 +317,12 @@ theorem norm_of_sqrt_adjoint_mul_self_eq [DecidableEq 𝕜] (T : E →ₗ[𝕜] simp_rw [mul_apply, adjoint_inner_right] exact inner_self_nonneg -theorem invertible_iff_inner_map_self_pos (hn : FiniteDimensional.finrank 𝕜 E = n) +theorem invertible_iff_inner_map_self_pos (hT : T.IsPositive) : Function.Bijective T ↔ ∀ v : E, v ≠ 0 → 0 < re ⟪T v, v⟫ := by constructor · intro h v hv - cases' (isPositive_iff_exists_adjoint_hMul_self T hn).mp hT with S hS + cases' (isPositive_iff_exists_adjoint_hMul_self T).mp hT with S hS rw [hS, mul_apply, adjoint_inner_left, inner_self_eq_norm_sq] suffices S v ≠ 0 by rw [← norm_ne_zero_iff] at this @@ -348,7 +346,7 @@ theorem invertible_iff_inner_map_self_pos (hn : FiniteDimensional.finrank 𝕜 E rw [ha.1, inner_zero_left, zero_re', lt_self_iff_false] at h exact h -theorem ext_inner_left_iff {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] +theorem _root_.ext_inner_left_iff {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : x = y ↔ ∀ v : E, inner x v = (inner y v : 𝕜) := by constructor @@ -357,7 +355,7 @@ theorem ext_inner_left_iff {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E · rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero] intro h; exact h _ -theorem invertiblePos (T : E →ₗ[𝕜] E) [hTi : Invertible T] (hn : FiniteDimensional.finrank 𝕜 E = n) +theorem invertiblePos (T : E →ₗ[𝕜] E) [hTi : Invertible T] (hT : T.IsPositive) : IsPositive (⅟ T) := by have : Function.Bijective T := @@ -365,7 +363,7 @@ theorem invertiblePos (T : E →ₗ[𝕜] E) [hTi : Invertible T] (hn : FiniteDi refine' (Module.End_isUnit_iff T).mp _ exact isUnit_of_invertible T have t1 := this - rw [invertible_iff_inner_map_self_pos T hn hT] at this + rw [invertible_iff_inner_map_self_pos T hT] at this constructor · intro u v rw [← adjoint_inner_left] @@ -383,12 +381,11 @@ theorem invertiblePos (T : E →ₗ[𝕜] E) [hTi : Invertible T] (hn : FiniteDi exact le_of_lt this theorem IsSymmetric.rePow_eq_rankOne {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [DecidableEq 𝕜] {n : ℕ} - (hn : FiniteDimensional.finrank 𝕜 E = n) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (r : ℝ) : - LinearMap.rePow T hn hT r = + [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (r : ℝ) : + LinearMap.rePow T hT r = ∑ i, - ((hT.eigenvalues hn i ^ r : ℝ) : 𝕜) • - @rankOne 𝕜 E _ _ _ (hT.eigenvectorBasis hn i) (hT.eigenvectorBasis hn i) := + ((hT.eigenvalues rfl i ^ r : ℝ) : 𝕜) • + (rankOne (hT.eigenvectorBasis rfl i) (hT.eigenvectorBasis rfl i) : E →L[𝕜] E) := by simp_rw [LinearMap.ext_iff, LinearMap.rePow_apply, ContinuousLinearMap.coe_sum, ContinuousLinearMap.coe_smul, @@ -403,8 +400,8 @@ theorem IsSymmetric.invertible (hT : T.IsSymmetric) [Invertible T] : (⅟ T).IsS simp_rw [star_invOf] simp only [hT, invOf_inj] -theorem isPositive_and_invertible_pos_eigenvalues (hT : T.IsPositive) [Invertible T] [DecidableEq 𝕜] - (i : Fin n) : 0 < hT.1.eigenvalues hn i := +theorem isPositive_and_invertible_pos_eigenvalues (hT : T.IsPositive) [Invertible T] + (i : Fin (FiniteDimensional.finrank 𝕜 E)) : 0 < hT.1.eigenvalues rfl i := by -- have := linear_map.invertible_pos T hn hT, -- have fs : function.bijective ⇑(⅟ T), @@ -416,20 +413,20 @@ theorem isPositive_and_invertible_pos_eigenvalues (hT : T.IsPositive) [Invertibl mul_invOf_self, LinearMap.one_apply, and_self_iff, forall_const] obtain ⟨v, hv, gh⟩ := Module.End.has_eigenvector_iff_hasEigenvalue.mpr - (@LinearMap.IsSymmetric.hasEigenvalue_eigenvalues 𝕜 _ E _ _ T hT.1 _ n hn i) - have ugh := (LinearMap.invertible_iff_inner_map_self_pos T hn hT).mp fs v gh + (@LinearMap.IsSymmetric.hasEigenvalue_eigenvalues 𝕜 _ E _ _ T hT.1 _ _ rfl i) + have ugh := (LinearMap.invertible_iff_inner_map_self_pos T hT).mp fs v gh rw [hv, inner_smul_real_left, RCLike.smul_re, inner_self_eq_norm_sq, mul_pos_iff] at ugh simp_rw [not_lt_of_le (sq_nonneg _), and_false_iff, or_false_iff] at ugh exact ugh.1 -noncomputable def IsPositive.rePowIsInvertible [DecidableEq 𝕜] (hT : T.IsPositive) [Invertible T] - (r : ℝ) : Invertible (T.rePow hn hT.1 r) := by - apply Invertible.mk (T.rePow hn hT.1 (-r)) <;> ext1 <;> +noncomputable def IsPositive.rePowIsInvertible (hT : T.IsPositive) [Invertible T] + (r : ℝ) : Invertible (T.rePow hT.1 r) := by + apply Invertible.mk (T.rePow hT.1 (-r)) <;> ext1 <;> simp_rw [LinearMap.mul_apply, LinearMap.rePow_apply, inner_sum, inner_smul_right, - orthonormal_iff_ite.mp (hT.1.eigenvectorBasis hn).orthonormal, mul_boole, mul_ite, + orthonormal_iff_ite.mp (hT.1.eigenvectorBasis rfl).orthonormal, mul_boole, mul_ite, MulZeroClass.mul_zero, Finset.sum_ite_eq, Finset.mem_univ, if_true, smul_smul, ← mul_assoc, ← RCLike.ofReal_mul, ← - Real.rpow_add (LinearMap.isPositive_and_invertible_pos_eigenvalues _ hn hT _), + Real.rpow_add (LinearMap.isPositive_and_invertible_pos_eigenvalues _ hT _), LinearMap.one_apply] <;> simp only [add_neg_self, neg_add_self, Real.rpow_zero, RCLike.ofReal_one, one_mul, ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr] @@ -452,6 +449,10 @@ theorem IsPositive.smulNonneg {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGrou simp_rw [LinearMap.IsPositive, LinearMap.IsSymmetric, LinearMap.smul_apply, inner_smul_left, inner_smul_right, RCLike.conj_ofReal, RCLike.re_ofReal_mul, hT.1 _ _, forall₂_true_iff, true_and_iff, mul_nonneg hr (hT.2 _), forall_true_iff] +theorem IsPositive.smulNNReal {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] + [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (r : NNReal) : + (((r : ℝ) : 𝕜) • T).IsPositive := +hT.smulNonneg r.2 end FiniteDimensional @@ -470,7 +471,7 @@ theorem IsPositive.toLinearMap (T : E →L[𝕜] E) : T.toLinearMap.IsPositive end ContinuousLinearMap theorem rankOne.isPositive {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - [CompleteSpace E] (x : E) : (@rankOne 𝕜 E _ _ _ x x).IsPositive := + [CompleteSpace E] (x : E) : (rankOne x x : _ →L[𝕜] _).IsPositive := by refine' ⟨rankOne.isSelfAdjoint _, _⟩ intro y @@ -489,23 +490,23 @@ theorem LinearMap.IsPositive.nonneg_eigenvalue {E : Type _} [NormedAddCommGroup open scoped BigOperators -theorem LinearMap.isPositive_iff_eq_sum_rankOne {n : ℕ} [DecidableEq 𝕜] [FiniteDimensional 𝕜 E] - (hn : FiniteDimensional.finrank 𝕜 E = n) (T : E →ₗ[𝕜] E) : +theorem LinearMap.isPositive_iff_eq_sum_rankOne [FiniteDimensional 𝕜 E] + (T : E →ₗ[𝕜] E) : T.IsPositive ↔ ∃ (m : ℕ) (u : Fin m → E), T = ∑ i : Fin m, ((rankOne (u i) (u i) : E →L[𝕜] E) : E →ₗ[𝕜] E) := by constructor · intro hT - let a : Fin n → E := fun i => - (Real.sqrt (hT.1.eigenvalues hn i) : 𝕜) • hT.1.eigenvectorBasis hn i - refine' ⟨n, a, _⟩ + let a : Fin (FiniteDimensional.finrank 𝕜 E) → E := fun i => + (Real.sqrt (hT.1.eigenvalues rfl i) : 𝕜) • hT.1.eigenvectorBasis rfl i + refine' ⟨FiniteDimensional.finrank 𝕜 E, a, _⟩ intros ext1 simp_rw [LinearMap.sum_apply, ContinuousLinearMap.coe_coe, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, RCLike.conj_ofReal, mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← RCLike.ofReal_mul, ← - Real.sqrt_mul (hT.nonneg_eigenvalue (hT.1.hasEigenvalue_eigenvalues hn _)), - Real.sqrt_mul_self (hT.nonneg_eigenvalue (hT.1.hasEigenvalue_eigenvalues hn _)), + Real.sqrt_mul (hT.nonneg_eigenvalue (hT.1.hasEigenvalue_eigenvalues rfl _)), + Real.sqrt_mul_self (hT.nonneg_eigenvalue (hT.1.hasEigenvalue_eigenvalues rfl _)), mul_comm _ (inner _ _), ← smul_eq_mul, smul_assoc, ← hT.1.apply_eigenvectorBasis, ← LinearMap.map_smul, ← map_sum, ← OrthonormalBasis.repr_apply_apply, OrthonormalBasis.sum_repr] · rintro ⟨m, u, hu⟩ @@ -520,9 +521,9 @@ theorem LinearMap.isPositive_iff_eq_sum_rankOne {n : ℕ} [DecidableEq 𝕜] [Fi RCLike.ofReal_re, sq_nonneg] theorem LinearMap.IsSymmetric.rePowIsPositiveOfIsPositive {𝕜 E : Type _} [RCLike 𝕜] - [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [DecidableEq 𝕜] {n : ℕ} - (hn : FiniteDimensional.finrank 𝕜 E = n) {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (r : ℝ) : - (T.rePow hn hT.1 r).IsPositive := + [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] + {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (r : ℝ) : + (T.rePow hT.1 r).IsPositive := by haveI := FiniteDimensional.complete 𝕜 E simp_rw [LinearMap.IsSymmetric.rePow_eq_rankOne, ContinuousLinearMap.coe_sum] @@ -532,4 +533,4 @@ theorem LinearMap.IsSymmetric.rePowIsPositiveOfIsPositive {𝕜 E : Type _} [RCL · rw [ContinuousLinearMap.IsPositive.toLinearMap] exact rankOne.isPositive _ · apply Real.rpow_nonneg - exact hT.nonneg_eigenvalue (hT.1.hasEigenvalue_eigenvalues hn _) + exact hT.nonneg_eigenvalue (hT.1.hasEigenvalue_eigenvalues rfl _) diff --git a/Monlib/LinearAlgebra/MyIps/RankOne.lean b/Monlib/LinearAlgebra/MyIps/RankOne.lean index 3e53c6e..39278ac 100644 --- a/Monlib/LinearAlgebra/MyIps/RankOne.lean +++ b/Monlib/LinearAlgebra/MyIps/RankOne.lean @@ -21,7 +21,8 @@ This defines the rank one operator $| x \rangle\!\langle y |$ for continuous lin section rankOne -variable {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] +variable {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] -- local notation "L(" x ")" => x →L[ℂ] x @@ -29,80 +30,90 @@ local notation "⟪" x "," y "⟫_𝕜" => @inner 𝕜 _ _ x y /-- we define the rank one operator $| x \rangle\!\langle y |$ by $x \mapsto \langle y, z \rangle \cdot x$ -/ -def rankOne (x y : E) : E →L[𝕜] E where - toFun z := ⟪y,z⟫_𝕜 • x - map_add' u v := by simp_rw [inner_add_right, add_smul] - map_smul' r u := by simp_rw [inner_smul_right, RingHom.id_apply, smul_smul] - cont := Continuous.smul (Continuous.inner continuous_const continuous_id') (continuous_const) +def rankOne : E₁ →ₗ[𝕜] (E₂ →+ (E₂ →L[𝕜] E₁)) where + toFun x := + { toFun := λ y => + { toFun := λ z => ⟪y,z⟫_𝕜 • x + map_add' := λ _ _ => by simp_rw [inner_add_right, add_smul] + map_smul' := λ _ _ => by simp_rw [inner_smul_right, RingHom.id_apply, smul_smul] + cont := Continuous.smul (Continuous.inner continuous_const continuous_id') (continuous_const) } + map_add' := λ a b => by simp only [inner_add_left, add_smul]; rfl + map_zero' := by simp only [inner_zero_left, zero_smul]; rfl } + map_add' a b := by simp only [smul_add]; rfl + map_smul' r a := by + simp only [smul_smul, RingHom.id_apply, mul_comm _ r] + simp only [← smul_smul]; rfl -- local notation "|" x "⟩⟨" y "|" => rankOne x y @[simp] -theorem rankOne_apply {x y : E} (z : E) : (rankOne x y : E →L[𝕜] E) z = ⟪y,z⟫_𝕜 • x := +theorem rankOne_apply {x : E₁} {y : E₂} (z : E₂) : (rankOne x y : E₂ →L[𝕜] E₁) z = ⟪y,z⟫_𝕜 • x := rfl open ContinuousLinearMap /-- $| x \rangle\!\langle \alpha\cdot y | = \bar{\alpha} \cdot | x \rangle\!\langle y |$ -/ @[simp] -theorem rankOne.smul_apply {x y : E} {α : 𝕜} : - rankOne x (α • y) = (starRingEnd 𝕜) α • (rankOne x y : E →L[𝕜] E) := +theorem rankOne.smul_apply {x : E₁} {y : E₂} {α : 𝕜} : + rankOne x (α • y) = (starRingEnd 𝕜) α • (rankOne x y : E₂ →L[𝕜] E₁) := by ext simp_rw [ContinuousLinearMap.smul_apply, rankOne_apply, inner_smul_left, smul_smul] /-- $| \alpha \cdot x \rangle\!\langle y | = \alpha \cdot | x \rangle\!\langle y |$ -/ @[simp] -theorem rankOne.apply_smul {x y : E} {α : 𝕜} : rankOne (α • x) y = α • (rankOne x y : E →L[𝕜] E) := +theorem rankOne.apply_smul {x : E₁} {y : E₂} {α : 𝕜} : rankOne (α • x) y = α • (rankOne x y : E₂ →L[𝕜] E₁) := by - ext - simp_rw [ContinuousLinearMap.smul_apply, rankOne_apply, smul_smul, mul_comm] + simp only [LinearMapClass.map_smul, AddMonoidHom.coe_smul, Pi.smul_apply] @[simp] -theorem rankOne.smul_real_apply {x y : E} {α : ℝ} : - rankOne x ((α : 𝕜) • y) = (α : 𝕜) • (rankOne x y : E →L[𝕜] E) := by +theorem rankOne.smul_real_apply {x : E₁} {y : E₂} {α : ℝ} : + rankOne x ((α : 𝕜) • y) = (α : 𝕜) • (rankOne x y : E₂ →L[𝕜] E₁) := by simp_rw [rankOne.smul_apply, RCLike.conj_ofReal] /-- $| x \rangle\!\langle y | | z \rangle\!\langle w | = \langle y, z \rangle \cdot | x \rangle\!\langle w |$ -/ @[simp] -theorem rankOne.apply_rankOne (x y z w : E) : - (rankOne x y : E →L[𝕜] E) ∘L (rankOne z w : _) = ⟪y,z⟫_𝕜 • (rankOne x w : _) := +theorem rankOne.apply_rankOne {E₃ : Type*} [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₃] + (x : E₁) (y z : E₂) (w : E₃) : + (rankOne x y : E₂ →L[𝕜] E₁) ∘L (rankOne z w : _) = ⟪y,z⟫_𝕜 • (rankOne x w : _) := by ext r simp_rw [ContinuousLinearMap.smul_apply, comp_apply, rankOne_apply, inner_smul_right, mul_comm, smul_smul] /-- $u \circ | x \rangle\!\langle y | = | u(x) \rangle\!\langle y |$ -/ -theorem ContinuousLinearMap.comp_rankOne (x y : E) (u : E →L[𝕜] E) : u ∘L rankOne x y = rankOne (u x) y := +theorem ContinuousLinearMap.comp_rankOne {E₃ : Type*} [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₃] + (x : E₁) (y : E₂) (u : E₁ →L[𝕜] E₃) : u ∘L rankOne x y = rankOne (u x) y := by ext r simp_rw [comp_apply, rankOne_apply, map_smul] /-- $| x \rangle\!\langle y | \circ u = | x \rangle\!\langle u^*(y) |$ -/ -theorem ContinuousLinearMap.rankOne_comp [CompleteSpace E] (x y : E) (u : E →L[𝕜] E) : - rankOne x y ∘L (u : E →L[𝕜] E) = rankOne x (adjoint u y) := +theorem ContinuousLinearMap.rankOne_comp {E₃ : Type*} [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₃] + [CompleteSpace E₂] [CompleteSpace E₃] (x : E₁) (y : E₂) (u : E₃ →L[𝕜] E₂) : + rankOne x y ∘L (u : E₃ →L[𝕜] E₂) = rankOne x (adjoint u y) := by ext r simp_rw [comp_apply, rankOne_apply, adjoint_inner_left] /-- rank one operators given by norm one vectors are automatically idempotent -/ @[simp] -theorem rankOne.isIdempotentElem (x : E) (h : ‖x‖ = 1) : IsIdempotentElem (rankOne x x : E →L[𝕜] E) := by +theorem rankOne.isIdempotentElem (x : E₁) (h : ‖x‖ = 1) : IsIdempotentElem (rankOne x x : E₁ →L[𝕜] E₁) := by simp_rw [IsIdempotentElem, ContinuousLinearMap.ext_iff, mul_def, rankOne.apply_rankOne, inner_self_eq_norm_sq_to_K, h, RCLike.ofReal_one, one_pow, one_smul, forall_const] -theorem rankOne.isSymmetric (x : E) : LinearMap.IsSymmetric ((rankOne x x : E →L[𝕜] E) : E →ₗ[𝕜] E) := by +theorem rankOne.isSymmetric (x : E₁) : LinearMap.IsSymmetric ((rankOne x x : E₁ →L[𝕜] E₁) : E₁ →ₗ[𝕜] E₁) := by simp_rw [LinearMap.IsSymmetric, ContinuousLinearMap.coe_coe, rankOne_apply, inner_smul_left, inner_smul_right, inner_conj_symm, mul_comm, forall₂_true_iff] /-- rank one operators are automatically self-adjoint -/ @[simp] -theorem rankOne.isSelfAdjoint [CompleteSpace E] (x : E) : IsSelfAdjoint (rankOne x x : E →L[𝕜] E) := +theorem rankOne.isSelfAdjoint [CompleteSpace E₁] (x : E₁) : IsSelfAdjoint (rankOne x x : E₁ →L[𝕜] E₁) := isSelfAdjoint_iff_isSymmetric.mpr (rankOne.isSymmetric x) /-- $| x \rangle\!\langle y |^* = | y \rangle\!\langle x |$ -/ -theorem rankOne.adjoint [CompleteSpace E] (x y : E) : adjoint (rankOne x y) = (rankOne y x : E →L[𝕜] E) := +theorem rankOne.adjoint [CompleteSpace E₁] [CompleteSpace E₂] (x : E₁) (y : E₂) : adjoint (rankOne x y) = (rankOne y x : E₁ →L[𝕜] E₂) := by ext a apply @ext_inner_right 𝕜 @@ -110,26 +121,26 @@ theorem rankOne.adjoint [CompleteSpace E] (x y : E) : adjoint (rankOne x y) = (r simp_rw [adjoint_inner_left, rankOne_apply, inner_smul_left, inner_smul_right, inner_conj_symm, mul_comm] -theorem rankOne_inner_left (x y z w : E) : ⟪(rankOne x y : E →L[𝕜] E) z,w⟫_𝕜 = ⟪z,y⟫_𝕜 * ⟪x,w⟫_𝕜 := by +theorem rankOne_inner_left (x w : E₁) (y z : E₂) : ⟪(rankOne x y : E₂ →L[𝕜] E₁) z,w⟫_𝕜 = ⟪z,y⟫_𝕜 * ⟪x,w⟫_𝕜 := by rw [rankOne_apply, inner_smul_left, inner_conj_symm] -theorem rankOne_inner_right (x y z w : E) : ⟪x,(rankOne y z : E →L[𝕜] E) w⟫_𝕜 = ⟪z,w⟫_𝕜 * ⟪x,y⟫_𝕜 := by +theorem rankOne_inner_right (x y : E₁) (z w : E₂) : ⟪x,(rankOne y z : _ →L[𝕜] _) w⟫_𝕜 = ⟪z,w⟫_𝕜 * ⟪x,y⟫_𝕜 := by rw [rankOne_apply, inner_smul_right] -theorem ContinuousLinearMap.commutes_with_all_iff [CompleteSpace E] (T : E →L[𝕜] E) : - (∀ S : E →L[𝕜] E, Commute S T) ↔ ∃ α : 𝕜, T = α • 1 := +theorem ContinuousLinearMap.commutes_with_all_iff [CompleteSpace E₁] (T : E₁ →L[𝕜] E₁) : + (∀ S, Commute S T) ↔ ∃ α : 𝕜, T = α • 1 := by constructor · intro h - have h' : ∀ x y : E, rankOne x y ∘L T = T ∘L rankOne x y := fun x y => h _ + have h' : ∀ x y : E₁, rankOne x y ∘L T = T ∘L rankOne x y := fun x y => h _ simp_rw [ContinuousLinearMap.rankOne_comp, ContinuousLinearMap.comp_rankOne] at h' - have h'' : ∀ x y : E, (rankOne (adjoint T y) x : E →L[𝕜] E) = rankOne y (T x) := + have h'' : ∀ x y : E₁, (rankOne (adjoint T y) x : _ →L[𝕜] _) = rankOne y (T x) := by intro x y nth_rw 1 [← rankOne.adjoint] rw [h', rankOne.adjoint] simp_rw [ext_iff, rankOne_apply] at h' h'' - by_cases H : ∀ x : E, x = 0 + by_cases H : ∀ x : E₁, x = 0 · use 0 simp_rw [ext_iff] intro x @@ -145,41 +156,41 @@ theorem ContinuousLinearMap.commutes_with_all_iff [CompleteSpace E] (T : E →L[ · rintro ⟨α, hα⟩ S simp_rw [Commute, SemiconjBy, mul_def, hα, comp_smul, smul_comp, one_def, comp_id, id_comp] -theorem ContinuousLinearMap.centralizer [CompleteSpace E] : - (@Set.univ (E →L[𝕜] E)).centralizer = { x : E →L[𝕜] E | ∃ α : 𝕜, x = α • 1 } := +theorem ContinuousLinearMap.centralizer [CompleteSpace E₁] : + (@Set.univ (E₁ →L[𝕜] E₁)).centralizer = { x : E₁ →L[𝕜] E₁ | ∃ α : 𝕜, x = α • 1 } := by simp_rw [Set.centralizer, Set.mem_univ, true_imp_iff, ← ContinuousLinearMap.commutes_with_all_iff] rfl theorem ContinuousLinearMap.scalar_centralizer : - {x : E →L[𝕜] E | ∃ α : 𝕜, x = α • 1}.centralizer = @Set.univ (E →L[𝕜] E) := + {x : E₁ →L[𝕜] E₁ | ∃ α : 𝕜, x = α • 1}.centralizer = @Set.univ (E₁ →L[𝕜] E₁) := by simp_rw [Set.centralizer, Set.ext_iff, Set.mem_setOf, Set.mem_univ, iff_true_iff] rintro x y ⟨α, rfl⟩ simp only [Algebra.smul_mul_assoc, one_mul, Algebra.mul_smul_comm, mul_one] -theorem ContinuousLinearMap.centralizer_centralizer [CompleteSpace E] : - (@Set.univ (E →L[𝕜] E)).centralizer.centralizer = Set.univ := by +theorem ContinuousLinearMap.centralizer_centralizer [CompleteSpace E₁] : + (@Set.univ (E₁ →L[𝕜] E₁)).centralizer.centralizer = Set.univ := by rw [ContinuousLinearMap.centralizer, ContinuousLinearMap.scalar_centralizer] -theorem rankOne.zero_left {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x : E) : (rankOne 0 x : E →L[𝕜] E) = 0 := by +theorem rankOne.zero_left + (x : E₂) : (rankOne 0 x : E₂ →L[𝕜] E₁) = 0 := by ext1 simp_rw [rankOne_apply, smul_zero, ContinuousLinearMap.zero_apply] -theorem rankOne.zero_right {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x : E) : (rankOne x 0 : E →L[𝕜] E) = 0 := by +theorem rankOne.zero_right + (x : E₁) : (rankOne x 0 : E₂ →L[𝕜] E₁) = 0 := by ext1 simp_rw [rankOne_apply, inner_zero_left, zero_smul, ContinuousLinearMap.zero_apply] -theorem rankOne.ext_iff {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x y : E) (h : (rankOne x x : E →L[𝕜] E) = rankOne y y) : ∃ α : 𝕜ˣ, x = (α : 𝕜) • y := +theorem rankOne.ext_iff + (x y : E₁) (h : (rankOne x x : E₁ →L[𝕜] E₁) = rankOne y y) : ∃ α : 𝕜ˣ, x = (α : 𝕜) • y := by have : x = 0 ↔ y = 0 := by constructor <;> intro hh <;> simp only [hh, ContinuousLinearMap.ext_iff, rankOne.zero_left, ContinuousLinearMap.zero_apply, - @eq_comm _ (0 : E →L[𝕜] E), rankOne_apply, smul_eq_zero] at h + @eq_comm _ (0 : E₁ →L[𝕜] E₁), rankOne_apply, smul_eq_zero] at h on_goal 1 => specialize h y on_goal 2 => specialize h x all_goals @@ -200,7 +211,7 @@ theorem rankOne.ext_iff {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [ inv_mul_cancel ((@inner_self_ne_zero 𝕜 _ _ _ _ _).mpr Hx), one_smul] theorem ContinuousLinearMap.ext_inner_map {F : Type _} [NormedAddCommGroup F] - [InnerProductSpace 𝕜 F] (T S : E →L[𝕜] F) : T = S ↔ ∀ x y, ⟪T x,y⟫_𝕜 = ⟪S x,y⟫_𝕜 := + [InnerProductSpace 𝕜 F] (T S : E₁ →L[𝕜] F) : T = S ↔ ∀ x y, ⟪T x,y⟫_𝕜 = ⟪S x,y⟫_𝕜 := by simp only [ContinuousLinearMap.ext_iff] constructor @@ -214,17 +225,19 @@ open scoped BigOperators local notation "|" x "⟩⟨" y "|" => rankOne x y -/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (x_1 x_2) -/ -theorem ContinuousLinearMap.exists_sum_rankOne [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) : - ∃ x y : Fin (FiniteDimensional.finrank 𝕜 E) × Fin (FiniteDimensional.finrank 𝕜 E) → E, +theorem ContinuousLinearMap.exists_sum_rankOne [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (T : E₁ →L[𝕜] E₂) : + ∃ (x : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂) → E₂) + (y : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂) → E₁), T = ∑ i, |x i⟩⟨y i| := by - letI := FiniteDimensional.complete 𝕜 E - let e := stdOrthonormalBasis 𝕜 E - let a : Fin (FiniteDimensional.finrank 𝕜 E) × Fin (FiniteDimensional.finrank 𝕜 E) → E := fun ij => - e.repr (T (e ij.1)) ij.2 • e ij.2 - let b : Fin (FiniteDimensional.finrank 𝕜 E) × Fin (FiniteDimensional.finrank 𝕜 E) → E := fun ij => - e ij.1 + letI := FiniteDimensional.complete 𝕜 E₁ + letI := FiniteDimensional.complete 𝕜 E₂ + let e₁ := stdOrthonormalBasis 𝕜 E₁ + let e₂ := stdOrthonormalBasis 𝕜 E₂ + let b : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂) → E₁ := fun ij => + e₁ ij.1 + let a : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂) → E₂ := fun ij => + e₂.repr (T (e₁ ij.1)) ij.2 • e₂ ij.2 refine' ⟨a, b, _⟩ simp only [a, b] simp only [ContinuousLinearMap.ext_inner_map, sum_apply, sum_inner, rankOne_inner_left, @@ -232,19 +245,25 @@ theorem ContinuousLinearMap.exists_sum_rankOne [FiniteDimensional 𝕜 E] (T : E intro u v symm calc - ∑ x : Fin (FiniteDimensional.finrank 𝕜 E) × Fin (FiniteDimensional.finrank 𝕜 E), - ⟪u,e x.fst⟫_𝕜 * (⟪T (e x.fst),e x.snd⟫_𝕜 * ⟪e x.snd,v⟫_𝕜) = - ∑ x_1 : Fin (FiniteDimensional.finrank 𝕜 E), - ∑ x_2 : Fin (FiniteDimensional.finrank 𝕜 E), - ⟪u,e x_1⟫_𝕜 * (⟪T (e x_1),e x_2⟫_𝕜 * ⟪e x_2,v⟫_𝕜) := + ∑ x : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂), + ⟪u,e₁ x.fst⟫_𝕜 * (⟪T (e₁ x.fst),e₂ x.snd⟫_𝕜 * ⟪e₂ x.snd,v⟫_𝕜) = + ∑ x_1, ∑ x_2, + ⟪u,e₁ x_1⟫_𝕜 * (⟪T (e₁ x_1),e₂ x_2⟫_𝕜 * ⟪e₂ x_2,v⟫_𝕜) := by simp_rw [← Finset.sum_product', Finset.univ_product_univ] - _ = ∑ x_1, ⟪u,e x_1⟫_𝕜 * ⟪T (e x_1),v⟫_𝕜 := by + _ = ∑ x_1, ⟪u,e₁ x_1⟫_𝕜 * ⟪T (e₁ x_1),v⟫_𝕜 := by simp_rw [← Finset.mul_sum, OrthonormalBasis.sum_inner_mul_inner] _ = ⟪T u,v⟫_𝕜 := by simp_rw [← adjoint_inner_right T, OrthonormalBasis.sum_inner_mul_inner] -theorem LinearMap.exists_sum_rankOne [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : - ∃ x y : Fin (FiniteDimensional.finrank 𝕜 E) × Fin (FiniteDimensional.finrank 𝕜 E) → E, - T = ∑ i, ↑(|x i⟩⟨y i| : E →L[𝕜] E) := +/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (x_1 x_2) -/ +example [FiniteDimensional 𝕜 E₁] (T : E₁ →L[𝕜] E₁) : + ∃ x y : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₁) → E₁, + T = ∑ i, |x i⟩⟨y i| := +ContinuousLinearMap.exists_sum_rankOne T + +theorem LinearMap.exists_sum_rankOne [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (T : E₁ →ₗ[𝕜] E₂) : + ∃ (x : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂) → E₂) + (y : Fin (FiniteDimensional.finrank 𝕜 E₁) × Fin (FiniteDimensional.finrank 𝕜 E₂) → E₁), + T = ∑ i, ↑(|x i⟩⟨y i| : _ →L[𝕜] _) := by obtain ⟨a, b, h⟩ := ContinuousLinearMap.exists_sum_rankOne (toContinuousLinearMap T) refine' ⟨a, b, _⟩ @@ -266,76 +285,78 @@ end rankOne section rankOneLm -variable {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] +variable {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] +variable {E : Type _} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] local notation "⟪" x "," y "⟫_𝕜" => @inner 𝕜 _ _ x y /-- same as `rank_one`, but as a linear map -/ -def rankOneLm (x y : E) : E →ₗ[𝕜] E := +@[reducible, simps!] +def rankOneLm (x : E₁) (y : E₂) : E₂ →ₗ[𝕜] E₁ := (rankOne x y).toLinearMap -@[simp] -theorem rankOneLm_apply (x y z : E) : (rankOneLm x y : E →ₗ[𝕜] E) z = ⟪y,z⟫_𝕜 • x := - rfl +-- @[simp] +-- theorem rankOneLm_apply (x y z : E) : (rankOneLm x y : E →ₗ[𝕜] E) z = ⟪y,z⟫_𝕜 • x := +-- rfl -theorem rankOneLm_comp_rankOneLm (x y z w : E) : - (rankOneLm x y : E →ₗ[𝕜] E) ∘ₗ rankOneLm z w = ⟪y,z⟫_𝕜 • (rankOneLm x w : _) := by +theorem rankOneLm_comp_rankOneLm (x : E₁) (y z : E₂) (w : E) : + (rankOneLm x y : _ →ₗ[𝕜] _) ∘ₗ rankOneLm z w = ⟪y,z⟫_𝕜 • rankOneLm x w := by simp_rw [LinearMap.ext_iff, LinearMap.comp_apply, rankOneLm_apply, LinearMap.smul_apply, inner_smul_right, mul_smul, rankOneLm_apply, smul_smul, mul_comm, forall_true_iff] -theorem rankOneLm_apply_rank_one (x y z w v : E) : - (rankOneLm x y : E →ₗ[𝕜] E) ((rankOneLm z w : E →ₗ[𝕜] E) v) = (⟪y,z⟫_𝕜 * ⟪w,v⟫_𝕜) • x := by +theorem rankOneLm_apply_rank_one (x : E₁) (y z : E₂) (w v : E) : + (rankOneLm x y : _ →ₗ[𝕜] _) ((rankOneLm z w : _ →ₗ[𝕜] _) v) = (⟪y,z⟫_𝕜 * ⟪w,v⟫_𝕜) • x := by rw [← LinearMap.comp_apply, rankOneLm_comp_rankOneLm, LinearMap.smul_apply, rankOneLm_apply, smul_smul] -theorem rankOneLm_adjoint [FiniteDimensional 𝕜 E] (x y : E) : - LinearMap.adjoint (rankOneLm x y : E →ₗ[𝕜] E) = rankOneLm y x := +theorem rankOneLm_adjoint [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (x : E₁) (y : E₂) : + LinearMap.adjoint (rankOneLm x y : _ →ₗ[𝕜] _) = rankOneLm y x := by simp_rw [rankOneLm, LinearMap.adjoint_eq_toCLM_adjoint, - ContinuousLinearMap.coe_inj, ← @rankOne.adjoint 𝕜 _ _ _ _ (FiniteDimensional.complete 𝕜 E) x y] + ContinuousLinearMap.coe_inj, ← @rankOne.adjoint 𝕜 _ _ _ _ _ _ _ + (FiniteDimensional.complete 𝕜 E₁) (FiniteDimensional.complete 𝕜 E₂) x y] rfl open scoped BigOperators -theorem sum_rankOne {n : Type _} [Fintype n] (x : n → E) (y : E) : - (rankOne (∑ i, x i) y : E →L[𝕜] E) = ∑ i, rankOne (x i) y := +theorem sum_rankOne {n : Type _} {s : Finset n} (x : n → E₁) (y : E₂) : + (rankOne (∑ i in s, x i) y : E₂ →L[𝕜] E₁) = ∑ i in s, rankOne (x i) y := by - ext1 z - simp_rw [ContinuousLinearMap.sum_apply, rankOne_apply, Finset.smul_sum] + simp only [map_sum, AddMonoidHom.finset_sum_apply] -theorem rankOne_sum {n : Type _} [Fintype n] (x : E) (y : n → E) : - (rankOne x (∑ i, y i) : E →L[𝕜] E) = ∑ i, rankOne x (y i) := +theorem rankOne_sum {n : Type _} {s : Finset n} (x : E₁) (y : n → E₂) : + (rankOne x (∑ i in s, y i) : _ →L[𝕜] _) = ∑ i in s, rankOne x (y i) := by - ext1 z - simp_rw [ContinuousLinearMap.sum_apply, rankOne_apply, sum_inner, Finset.sum_smul] + simp only [map_sum] -theorem sum_rankOneLm {n : Type _} [Fintype n] (x : n → E) (y : E) : - (rankOneLm (∑ i : n, x i) y : E →ₗ[𝕜] E) = ∑ i : n, rankOneLm (x i) y := - by - rw [rankOneLm, sum_rankOne, ContinuousLinearMap.coe_sum] - rfl +theorem sum_rankOneLm {n : Type _} {s : Finset n} (x : n → E₁) (y : E₂) : + (rankOneLm (∑ i in s, x i) y : _ →ₗ[𝕜] _) = ∑ i in s, rankOneLm (x i) y := +by simp [rankOneLm, sum_rankOne] -theorem rankOneLm_sum {n : Type _} [Fintype n] (x : E) (y : n → E) : - (rankOneLm x (∑ i : n, y i) : E →ₗ[𝕜] E) = ∑ i : n, rankOneLm x (y i) := - by - rw [rankOneLm, rankOne_sum, ContinuousLinearMap.coe_sum] - rfl +theorem rankOneLm_sum {n : Type _} {s : Finset n} (x : E₁) (y : n → E₂) : + (rankOneLm x (∑ i in s, y i) : _ →ₗ[𝕜] _) = ∑ i in s, rankOneLm x (y i) := +by simp [rankOneLm, rankOne_sum] end rankOneLm -theorem LinearMap.ext_of_rankOne {𝕜 H H' : Type _} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] - [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] - {x y : (H →L[𝕜] H) →ₗ[𝕜] H'} (h : ∀ a b : H, x (rankOne a b) = y (rankOne a b)) : x = y := +theorem LinearMap.ext_of_rankOne {𝕜 H₁ H₂ H' : Type _} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] + [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] + [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] + [FiniteDimensional 𝕜 H₁] [FiniteDimensional 𝕜 H₂] + {x y : (H₁ →L[𝕜] H₂) →ₗ[𝕜] H'} (h : ∀ a b, x (rankOne a b) = y (rankOne a b)) : x = y := by ext a obtain ⟨α, β, rfl⟩ := ContinuousLinearMap.exists_sum_rankOne a simp_rw [map_sum, h] -theorem LinearMap.ext_of_rank_one' {𝕜 H H' : Type _} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] - [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 H] - {x y : (H →ₗ[𝕜] H) →ₗ[𝕜] H'} - (h : ∀ a b : H, x ↑(@rankOne 𝕜 _ _ _ _ a b) = y ↑(@rankOne 𝕜 _ _ _ _ a b)) : x = y := +theorem LinearMap.ext_of_rank_one' {𝕜 H₁ H₂ H' : Type _} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] + [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] + [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] + [FiniteDimensional 𝕜 H₁] [FiniteDimensional 𝕜 H₂] + {x y : (H₁ →ₗ[𝕜] H₂) →ₗ[𝕜] H'} + (h : ∀ a b, x (rankOne a b : _ →L[𝕜] _).toLinearMap = y (rankOne a b : _ →L[𝕜] _).toLinearMap) : x = y := by ext a obtain ⟨α, β, rfl⟩ := LinearMap.exists_sum_rankOne a @@ -345,7 +366,7 @@ open scoped BigOperators theorem rankOne.sum_orthonormalBasis_eq_id_lm {𝕜 : Type _} {E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type _} [Fintype ι] - (b : OrthonormalBasis ι 𝕜 E) : ∑ i, (@rankOne 𝕜 E _ _ _ (b i) (b i) : E →ₗ[𝕜] E) = 1 := + (b : OrthonormalBasis ι 𝕜 E) : ∑ i, (rankOne (b i) (b i) : E →L[𝕜] E).toLinearMap = 1 := by simp only [← ContinuousLinearMap.coe_sum, rankOne.sum_orthonormalBasis_eq_id b] rfl @@ -354,60 +375,64 @@ theorem ContinuousLinearMap.coe_eq_zero {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] (f : E₁ →L[𝕜] E₂) : (f : E₁ →ₗ[𝕜] E₂) = 0 ↔ f = 0 := by norm_cast -theorem rankOne.eq_zero_iff {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x y : E) : (rankOne x y : E →L[𝕜] E) = 0 ↔ x = 0 ∨ y = 0 := by +theorem rankOne.eq_zero_iff {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + (x : E₁) (y : E₂) : (rankOne x y : _ →L[𝕜] _) = 0 ↔ x = 0 ∨ y = 0 := by simp_rw [ContinuousLinearMap.ext_iff, rankOne_apply, ContinuousLinearMap.zero_apply, smul_eq_zero, forall_or_right, forall_inner_eq_zero_iff, or_comm] -theorem rankOne.left_add {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x y z : E) : (rankOne (x + y) z : E →L[𝕜] E) = rankOne x z + rankOne y z := +theorem rankOne.left_add {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + (x y : E₁) (z : E₂) : (rankOne (x + y) z : _ →L[𝕜] _) = rankOne x z + rankOne y z := by - ext - simp only [rankOne_apply, ContinuousLinearMap.add_apply, smul_add] + simp only [map_add, AddMonoidHom.add_apply] -theorem rankOne.right_add {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x y z : E) : (rankOne x (y + z) : E →L[𝕜] E) = rankOne x y + rankOne x z := +theorem rankOne.right_add {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + (x : E₁) (y z : E₂) : (rankOne x (y + z) : _ →L[𝕜] _) = rankOne x y + rankOne x z := by - ext - simp only [rankOne_apply, ContinuousLinearMap.add_apply, inner_add_left, add_smul] + simp only [map_add] -theorem rankOne.left_sub {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x y z : E) : (rankOne (x - y) z : E →L[𝕜] E) = rankOne x z - rankOne y z := +theorem rankOne.left_sub {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + (x y : E₁) (z : E₂) : (rankOne (x - y) z : _ →L[𝕜] _) = rankOne x z - rankOne y z := by - ext - simp only [rankOne_apply, ContinuousLinearMap.sub_apply, smul_sub] + simp only [map_sub, AddMonoidHom.sub_apply] -theorem rankOne.right_sub {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] - (x y z : E) : (rankOne x (y - z) : E →L[𝕜] E) = rankOne x y - rankOne x z := +theorem rankOne.right_sub {𝕜 E₁ E₂ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + (x : E₁) (y z : E₂) : (rankOne x (y - z) : _ →L[𝕜] _) = rankOne x y - rankOne x z := by - ext - simp only [rankOne_apply, ContinuousLinearMap.sub_apply, inner_sub_left, sub_smul] + simp only [map_sub] -theorem LinearMap.rankOne_comp {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (x y : E) (u : E →ₗ[𝕜] E) : - ((rankOne x y : E →L[𝕜] E) : E →ₗ[𝕜] E) ∘ₗ u = (rankOne x (adjoint u y) : E →L[𝕜] E) := +theorem LinearMap.rankOne_comp {𝕜 E₁ E₂ E₃ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + [InnerProductSpace 𝕜 E₃] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 E₃] (x : E₁) (y : E₂) (u : E₃ →ₗ[𝕜] E₂) : + (rankOne x y : _ →L[𝕜] _).toLinearMap ∘ₗ u = (rankOne x (adjoint u y) : _ →L[𝕜] _) := by ext simp_rw [LinearMap.comp_apply, ContinuousLinearMap.coe_coe, rankOne_apply, LinearMap.adjoint_inner_left] -theorem LinearMap.rankOne_comp' {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (x y : E) (u : E →ₗ[𝕜] E) : - ((rankOne x y : E →L[𝕜] E) : E →ₗ[𝕜] E) ∘ₗ adjoint u = (rankOne x (u y) : E →L[𝕜] E) := by - rw [LinearMap.rankOne_comp, LinearMap.adjoint_adjoint] +theorem LinearMap.rankOne_comp' {𝕜 E₁ E₂ E₃ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + [InnerProductSpace 𝕜 E₃] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 E₃] (x : E₁) (y : E₂) (u : E₂ →ₗ[𝕜] E₃) : + (rankOne x y : _ →L[𝕜] _).toLinearMap ∘ₗ adjoint u = (rankOne x (u y) : _ →L[𝕜] _) := +by rw [LinearMap.rankOne_comp, LinearMap.adjoint_adjoint] theorem OrthonormalBasis.orthogonalProjection'_eq_sum_rankOne {ι 𝕜 : Type _} [RCLike 𝕜] {E : Type _} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {U : Submodule 𝕜 E} - [CompleteSpace ↥U] (b : OrthonormalBasis ι 𝕜 ↥U) : + [CompleteSpace U] (b : OrthonormalBasis ι 𝕜 ↥U) : orthogonalProjection' U = ∑ i : ι, rankOne (b i : E) (b i : E) := by ext simp_rw [orthogonalProjection'_apply, b.orthogonalProjection_eq_sum, ContinuousLinearMap.sum_apply, rankOne_apply, Submodule.coe_sum, Submodule.coe_smul_of_tower] -theorem LinearMap.comp_rankOne {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] (x y : E) (u : E →ₗ[𝕜] E) : - u ∘ₗ ((rankOne x y : E →L[𝕜] E) : E →ₗ[𝕜] E) = (rankOne (u x) y : E →L[𝕜] E) := +theorem LinearMap.comp_rankOne {𝕜 E₁ E₂ E₃ : Type _} [RCLike 𝕜] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] + [InnerProductSpace 𝕜 E₃] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 E₃] (x : E₁) (y : E₂) (u : E₁ →ₗ[𝕜] E₃) : + u ∘ₗ (rankOne x y : _ →L[𝕜] _).toLinearMap = (rankOne (u x) y : _ →L[𝕜] _) := by ext simp_rw [LinearMap.comp_apply, ContinuousLinearMap.coe_coe, rankOne_apply, _root_.map_smul] diff --git a/Monlib/LinearAlgebra/MyIps/Vn.lean b/Monlib/LinearAlgebra/MyIps/Vn.lean index 98e9829..f3cd02d 100644 --- a/Monlib/LinearAlgebra/MyIps/Vn.lean +++ b/Monlib/LinearAlgebra/MyIps/Vn.lean @@ -67,7 +67,7 @@ theorem elem_idempotent_iff_ker_and_range_invariantUnder_commutant (M : VonNeuma rw [← VonNeumannAlgebra.commutant_commutant M] intro m hm; ext x obtain ⟨v, w, hvw, _⟩ := - Submodule.existsUnique_add_of_isCompl (LinearMap.IsIdempotent.isCompl_range_ker e.toLinearMap (IsIdempotentElem.clm_to_lm.mp h)) x + Submodule.existsUnique_add_of_isCompl (IsIdempotentElem.isCompl_range_ker (IsIdempotentElem.clm_to_lm.mp h)) x obtain ⟨y, hy⟩ := SetLike.coe_mem w -- let hvv := SetLike.coe_mem v -- let hvv : H := (@Subtype.val H (fun x ↦ x ∈ ↑(LinearMap.ker ↑e)) v : H) diff --git a/Monlib/LinearAlgebra/MyMatrix/PosDefRpow.lean b/Monlib/LinearAlgebra/MyMatrix/PosDefRpow.lean index b5dd4ab..b37e3e6 100644 --- a/Monlib/LinearAlgebra/MyMatrix/PosDefRpow.lean +++ b/Monlib/LinearAlgebra/MyMatrix/PosDefRpow.lean @@ -46,7 +46,7 @@ theorem PosDef.rpow_mul_rpow (r₁ r₂ : ℝ) {Q : Matrix n n 𝕜} (hQ : PosDe Function.comp_apply, ← RCLike.ofReal_mul, ← Real.rpow_add (hQ.pos_eigenvalues _)] rfl -theorem PosSemidef.rpow_mul_rpow (r₁ r₂ : NNRealˣ) (h : r₁ + (r₂ : NNReal) ≠ 0) +theorem PosSemidef.rpow_mul_rpow (r₁ r₂ : NNRealˣ) {Q : Matrix n n 𝕜} (hQ : PosSemidef Q) : hQ.rpow r₁ * hQ.rpow r₂ = hQ.rpow (r₁ + r₂) := by diff --git a/Monlib/LinearAlgebra/MyMatrix/PosEqLinearMapIsPositive.lean b/Monlib/LinearAlgebra/MyMatrix/PosEqLinearMapIsPositive.lean index 62379fa..bd0f8dd 100644 --- a/Monlib/LinearAlgebra/MyMatrix/PosEqLinearMapIsPositive.lean +++ b/Monlib/LinearAlgebra/MyMatrix/PosEqLinearMapIsPositive.lean @@ -89,10 +89,8 @@ theorem Matrix.posSemidef_eq_linearMap_positive [Fintype n] [DecidableEq n] (x : theorem Matrix.posSemidef_iff [Fintype n] [DecidableEq n] (x : Matrix n n 𝕜) : x.PosSemidef ↔ ∃ y : Matrix n n 𝕜, x = yᴴ * y := by - have : FiniteDimensional.finrank 𝕜 (PiLp 2 fun _x : n => 𝕜) = Fintype.card n := by - simp_rw [finrank_euclideanSpace] simp_rw [Matrix.posSemidef_eq_linearMap_positive, - LinearMap.isPositive_iff_exists_adjoint_hMul_self _ this, + LinearMap.isPositive_iff_exists_adjoint_hMul_self, ← LinearEquiv.eq_symm_apply] have thisor : ∀ x y : (PiLp 2 fun _x : n => 𝕜) →ₗ[𝕜] (PiLp 2 fun _x : n => 𝕜), toEuclideanLin.symm (x * y) = (toEuclideanLin.symm x) * (toEuclideanLin.symm y) := λ x y => by @@ -121,7 +119,8 @@ theorem Matrix.dotProduct_eq_inner {n : Type _} [Fintype n] (x y : n → 𝕜) : rfl theorem Matrix.PosSemidef.invertible_iff_posDef {n : Type _} [Fintype n] [DecidableEq n] - {x : Matrix n n 𝕜} (hx : x.PosSemidef) : Function.Bijective (toLin' x) ↔ x.PosDef := + {x : Matrix n n 𝕜} (hx : x.PosSemidef) : + Function.Bijective (toLin' x) ↔ x.PosDef := by simp_rw [Matrix.PosDef, hx.1, true_and_iff] cases' (Matrix.posSemidef_iff x).mp hx with y hy @@ -261,8 +260,7 @@ theorem Matrix.posSemidef_iff_eq_rankOne [Fintype n] [DecidableEq n] {x : Matrix LinearMap.toMatrix' ((rankOne (v i) (v i) : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) := by - have : FiniteDimensional.finrank 𝕜 (EuclideanSpace 𝕜 n) = Fintype.card n := FiniteDimensional.finrank_pi _ - simp_rw [posSemidef_eq_linearMap_positive, LinearMap.isPositive_iff_eq_sum_rankOne this, + simp_rw [posSemidef_eq_linearMap_positive, LinearMap.isPositive_iff_eq_sum_rankOne, toEuclideanLin_eq_toLin, Matrix.toLin_piLp_eq_toLin', ← map_sum] constructor <;> rintro ⟨m, y, hy⟩ <;> refine' ⟨m, y, _⟩ · rw [← hy] @@ -272,18 +270,15 @@ theorem Matrix.posSemidef_iff_eq_rankOne [Fintype n] [DecidableEq n] {x : Matrix theorem Matrix.posSemidef_iff_eq_rankOne' [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → (n → 𝕜)), - x = - ∑ i : Fin m, - LinearMap.toMatrix' ((rankOne (v i) (v i) : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) : - EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) := + x = ∑ i : Fin m, + LinearMap.toMatrix' (rankOneLm (v i) (v i) : (EuclideanSpace 𝕜 n) →ₗ[𝕜] (EuclideanSpace 𝕜 n)) := Matrix.posSemidef_iff_eq_rankOne theorem Matrix.posSemidef_iff_eq_rankOne'' [Fintype n] [DecidableEq n] {x : Matrix n n 𝕜} : x.PosSemidef ↔ ∃ (m : Type) (hm : Fintype m) (v : m → (n → 𝕜)), x = ∑ i : m, - LinearMap.toMatrix' ((rankOne (v i) (v i) : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) : - EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) := + LinearMap.toMatrix' (rankOneLm (v i) (v i) : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) := by rw [Matrix.posSemidef_iff_eq_rankOne'] constructor @@ -299,8 +294,7 @@ by theorem rankOne.EuclideanSpace.toEuclideanLin_symm {𝕜 : Type _} [RCLike 𝕜] {n : Type _} [Fintype n] [DecidableEq n] (x y : EuclideanSpace 𝕜 n) : - toEuclideanLin.symm ((@rankOne 𝕜 (EuclideanSpace 𝕜 n) _ _ _ x y : - EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)) = + toEuclideanLin.symm (rankOne x y : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) = col (x : n → 𝕜) * (col (y : n → 𝕜))ᴴ := by simp_rw [← Matrix.ext_iff, toEuclideanLin_eq_toLin, toLin_symm, LinearMap.toMatrix_apply, @@ -314,15 +308,12 @@ theorem rankOne.EuclideanSpace.toEuclideanLin_symm {𝕜 : Type _} [RCLike 𝕜] theorem rankOne.EuclideanSpace.toMatrix' {𝕜 : Type _} [RCLike 𝕜] {n : Type _} [Fintype n] [DecidableEq n] (x y : EuclideanSpace 𝕜 n) : - LinearMap.toMatrix' (((@rankOne 𝕜 (EuclideanSpace 𝕜 n) _ _ _ x y : - EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)) - : (n → 𝕜) →ₗ[𝕜] (n → 𝕜)) = + LinearMap.toMatrix' ((rankOne x y).toLinearMap : (n → 𝕜) →ₗ[𝕜] (n → 𝕜)) = col (x : n → 𝕜) * (col (y : n → 𝕜))ᴴ := rankOne.EuclideanSpace.toEuclideanLin_symm _ _ theorem rankOne.Pi.toMatrix'' {𝕜 : Type _} [RCLike 𝕜] {n : Type _} [Fintype n] [DecidableEq n] (x y : n → 𝕜) : - LinearMap.toMatrix' (((@rankOne 𝕜 (EuclideanSpace 𝕜 n) _ _ _ x y : - EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)) + LinearMap.toMatrix' (((rankOneLm x y) : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) : (n → 𝕜) →ₗ[𝕜] (n → 𝕜)) = col (x : n → 𝕜) * (col (y : n → 𝕜))ᴴ := rankOne.EuclideanSpace.toEuclideanLin_symm _ _ @@ -380,11 +371,11 @@ def LinearMap.PositiveMap (T : (M₁ →ₗ[ℂ] M₁) →ₗ[ℂ] M₂ →ₗ[ ∀ x : M₁ →ₗ[ℂ] M₁, x.IsPositive → (T x).IsPositive /-- a $^*$-homomorphism from $L(M_1)$ to $L(M_2)$ is a positive map -/ -theorem LinearMap.PositiveMap.starHom {n₁ : ℕ} [FiniteDimensional ℂ M₁] [FiniteDimensional ℂ M₂] - (hn₁ : FiniteDimensional.finrank ℂ M₁ = n₁) (φ : StarAlgHom ℂ (M₁ →ₗ[ℂ] M₁) (M₂ →ₗ[ℂ] M₂)) : +theorem LinearMap.PositiveMap.starHom [FiniteDimensional ℂ M₁] [FiniteDimensional ℂ M₂] + (φ : StarAlgHom ℂ (M₁ →ₗ[ℂ] M₁) (M₂ →ₗ[ℂ] M₂)) : φ.toAlgHom.toLinearMap.PositiveMap := by intro x hx - rcases(LinearMap.isPositive_iff_exists_adjoint_hMul_self x hn₁).mp hx with ⟨w, rfl⟩ + rcases(LinearMap.isPositive_iff_exists_adjoint_hMul_self x).mp hx with ⟨w, rfl⟩ have : ∀ h, φ.toAlgHom.toLinearMap h = φ h := fun h => rfl simp_rw [LinearMap.IsPositive, LinearMap.IsSymmetric, this, _root_.map_mul, ← LinearMap.star_eq_adjoint, map_star, LinearMap.mul_apply, LinearMap.star_eq_adjoint, diff --git a/Monlib/LinearAlgebra/TensorFinite.lean b/Monlib/LinearAlgebra/TensorFinite.lean index cb3a803..b5f6efe 100644 --- a/Monlib/LinearAlgebra/TensorFinite.lean +++ b/Monlib/LinearAlgebra/TensorFinite.lean @@ -9,6 +9,7 @@ import Mathlib.Analysis.RCLike.Basic import Monlib.LinearAlgebra.IsReal import Monlib.LinearAlgebra.MyIps.OpUnop import Monlib.LinearAlgebra.MyIps.MulOp +import Monlib.LinearAlgebra.MyTensorProduct #align_import linear_algebra.tensor_finite diff --git a/Monlib/QuantumGraph/Example.lean b/Monlib/QuantumGraph/Example.lean index 81050e8..ea2886b 100644 --- a/Monlib/QuantumGraph/Example.lean +++ b/Monlib/QuantumGraph/Example.lean @@ -22,15 +22,18 @@ open scoped TensorProduct BigOperators Kronecker Matrix Functional variable {p : Type _} [Fintype p] [DecidableEq p] {n : p → Type _} [∀ i, Fintype (n i)] [∀ i, DecidableEq (n i)] + {p₂ : Type*} [Fintype p₂] [DecidableEq p₂] {n₂ : p₂ → Type*} [∀ i, Fintype (n₂ i)] + [∀ i, DecidableEq (n₂ i)] local notation "ℍ" => PiMat ℂ p n +local notation "ℍ₂" => PiMat ℂ p₂ n₂ -- local notation `⊗K` := matrix (n × n) (n × n) ℂ local notation "l(" x ")" => x →ₗ[ℂ] x -variable {φ : Π i : p, Module.Dual ℂ (Matrix (n i) (n i) ℂ)} +variable {φ : Π i : p, Module.Dual ℂ (Matrix (n i) (n i) ℂ)} {ψ : Π i, Module.Dual ℂ (Matrix (n₂ i) (n₂ i) ℂ)} -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" => LinearMap.mul' ℂ ℍ @@ -58,17 +61,21 @@ local notation "τ⁻¹" => local notation "id" => (1 : ℍ →ₗ[ℂ] ℍ) -noncomputable def Qam.completeGraph (E : Type _) [One E] [NormedAddCommGroup E] - [InnerProductSpace ℂ E] : E →ₗ[ℂ] E := - |(1 : E)⟩⟨(1 : E)| +noncomputable def Qam.completeGraph (E₁ E₂ : Type _) [One E₁] [One E₂] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] : + E₂ →ₗ[ℂ] E₁ := + |(1 : E₁)⟩⟨(1 : E₂)| -theorem Qam.completeGraph_eq {E : Type _} [One E] [NormedAddCommGroup E] [InnerProductSpace ℂ E] : - Qam.completeGraph E = |(1 : E)⟩⟨(1 : E)| := +theorem Qam.completeGraph_eq {E₁ E₂ : Type _} [One E₁] [One E₂] [NormedAddCommGroup E₁] + [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] : + Qam.completeGraph E₁ E₂ = |(1 : E₁)⟩⟨(1 : E₂)| := rfl -theorem Qam.completeGraph_eq' {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] : - Qam.completeGraph (Matrix p p ℂ) = - Algebra.linearMap ℂ (Matrix p p ℂ) ∘ₗ LinearMap.adjoint (Algebra.linearMap ℂ (Matrix p p ℂ)) := +theorem Qam.completeGraph_eq' {φ : Module.Dual ℂ (Matrix p p ℂ)} + {ψ : Module.Dual ℂ (Matrix p₂ p₂ ℂ)} + [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] : + Qam.completeGraph (Matrix p p ℂ) (Matrix p₂ p₂ ℂ) = + Algebra.linearMap ℂ (Matrix p p ℂ) ∘ₗ LinearMap.adjoint (Algebra.linearMap ℂ (Matrix p₂ p₂ ℂ)) := by rw [LinearMap.ext_iff] intro x @@ -77,10 +84,11 @@ theorem Qam.completeGraph_eq' {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ. Matrix.one_mul] simp only [Algebra.linearMap_apply, Algebra.algebraMap_eq_smul_one] -theorem Pi.Qam.completeGraph_eq' - [hφ : Π i, (φ i).IsFaithfulPosMap] : - Qam.completeGraph (PiMat ℂ p n) - = (Algebra.linearMap ℂ (PiMat ℂ p n)) ∘ₗ (LinearMap.adjoint (Algebra.linearMap ℂ (PiMat ℂ p n))) := +theorem Pi.Qam.completeGraph_eq' {φ : Π i, Module.Dual ℂ (Matrix (n i) (n i) ℂ)} + {ψ : Π i, Module.Dual ℂ (Matrix (n₂ i) (n₂ i) ℂ)} + [hφ : Π i, (φ i).IsFaithfulPosMap] [hψ : Π i, (ψ i).IsFaithfulPosMap] : + Qam.completeGraph (PiMat ℂ p n) (PiMat ℂ p₂ n₂) + = (Algebra.linearMap ℂ (PiMat ℂ p n)) ∘ₗ (LinearMap.adjoint (Algebra.linearMap ℂ (PiMat ℂ p₂ n₂))) := by rw [LinearMap.ext_iff] intro x @@ -88,39 +96,57 @@ theorem Pi.Qam.completeGraph_eq' Nontracial.Pi.unit_adjoint_eq, Module.Dual.pi.IsFaithfulPosMap.inner_eq, star_one, one_mul, Algebra.linearMap_apply, Algebra.algebraMap_eq_smul_one] -theorem Qam.Nontracial.CompleteGraph.qam {E : Type _} [NormedAddCommGroupOfRing E] - [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] : - schurIdempotent (Qam.completeGraph E) (Qam.completeGraph E) = Qam.completeGraph E := by - rw [Qam.completeGraph, schurIdempotent.apply_rankOne, one_mul] +theorem Qam.Nontracial.CompleteGraph.qam {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] + [FiniteDimensional ℂ E₁] [FiniteDimensional ℂ E₂] + [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] + [SMulCommClass ℂ E₁ E₁] [SMulCommClass ℂ E₂ E₂] : + schurIdempotent (Qam.completeGraph E₁ E₂) (Qam.completeGraph E₁ E₂) = Qam.completeGraph E₁ E₂ := by + simp_rw [Qam.completeGraph, schurIdempotent.apply_rankOne, one_mul] + +lemma Qam.Nontracial.CompleteGraph.adjoint_eq {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] + [FiniteDimensional ℂ E₁] [FiniteDimensional ℂ E₂] + [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] + [SMulCommClass ℂ E₁ E₁] [SMulCommClass ℂ E₂ E₂] : + LinearMap.adjoint (Qam.completeGraph E₁ E₂) = Qam.completeGraph E₂ E₁ := +rankOneLm_adjoint _ _ theorem Qam.Nontracial.CompleteGraph.isSelfAdjoint {E : Type _} [One E] [NormedAddCommGroup E] - [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : _root_.IsSelfAdjoint (Qam.completeGraph E) := by + [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : _root_.IsSelfAdjoint (Qam.completeGraph E E) := by simp_rw [_root_.IsSelfAdjoint, Qam.completeGraph, LinearMap.star_eq_adjoint, ← rankOneLm_eq_rankOne, rankOneLm_adjoint] theorem Qam.Nontracial.CompleteGraph.isReal {φ : Module.Dual ℂ (Matrix p p ℂ)} - [hφ : φ.IsFaithfulPosMap] : (Qam.completeGraph (Matrix p p ℂ)).IsReal := by - rw [Qam.completeGraph, LinearMap.isReal_iff, rankOne_real_apply, conjTranspose_one, + {ψ : Module.Dual ℂ (Matrix p₂ p₂ ℂ)} [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] : + (Qam.completeGraph (Matrix p p ℂ) (Matrix p₂ p₂ ℂ)).IsReal := by + simp_rw [Qam.completeGraph, LinearMap.isReal_iff, rankOne_real_apply, conjTranspose_one, _root_.map_one] -theorem Qam.Nontracial.CompleteGraph.is_symm {φ : Module.Dual ℂ (Matrix p p ℂ)} - [hφ : φ.IsFaithfulPosMap] : - LinearEquiv.symmMap ℂ (Matrix p p ℂ) _ (Qam.completeGraph (Matrix p p ℂ)) = - Qam.completeGraph (Matrix p p ℂ) := +theorem Qam.Nontracial.CompleteGraph.symm_eq {φ : Module.Dual ℂ (Matrix p p ℂ)} + {ψ : Module.Dual ℂ (Matrix p₂ p₂ ℂ)} [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] : + LinearEquiv.symmMap ℂ (Matrix p₂ p₂ ℂ) _ (Qam.completeGraph (Matrix p p ℂ) (Matrix p₂ p₂ ℂ)) = + Qam.completeGraph (Matrix p₂ p₂ ℂ) (Matrix p p ℂ) := by simp_rw [Qam.completeGraph, Qam.RankOne.symmetric_eq, conjTranspose_one, _root_.map_one] - -theorem Pi.Qam.Nontracial.CompleteGraph.isReal [hφ : ∀ i, (φ i).IsFaithfulPosMap] : - (Qam.completeGraph ℍ).IsReal := by - rw [Qam.completeGraph, ← rankOneLm_eq_rankOne, LinearMap.isReal_iff, Pi.rankOneLm_real_apply, +theorem Qam.Nontracial.CompleteGraph.is_symm + {φ : Module.Dual ℂ (Matrix p p ℂ)} [φ.IsFaithfulPosMap] : + LinearEquiv.symmMap ℂ (Matrix p p ℂ) _ (Qam.completeGraph (Matrix p p ℂ) (Matrix p p ℂ)) = + Qam.completeGraph (Matrix p p ℂ) (Matrix p p ℂ) := +Qam.Nontracial.CompleteGraph.symm_eq + +theorem Pi.Qam.Nontracial.CompleteGraph.isReal + [hφ : ∀ i, (φ i).IsFaithfulPosMap] [hψ : ∀ i, (ψ i).IsFaithfulPosMap] : + (Qam.completeGraph ℍ ℍ₂).IsReal := by + simp_rw [Qam.completeGraph, ← rankOneLm_eq_rankOne, LinearMap.isReal_iff, Pi.rankOneLm_real_apply, star_one, _root_.map_one] theorem Pi.Qam.Nontracial.CompleteGraph.is_symm [hφ : ∀ i, (φ i).IsFaithfulPosMap] : - LinearEquiv.symmMap ℂ ℍ _ (Qam.completeGraph ℍ) = Qam.completeGraph ℍ := by + LinearEquiv.symmMap ℂ ℍ _ (Qam.completeGraph ℍ ℍ) = Qam.completeGraph ℍ ℍ := by simp_rw [Qam.completeGraph, LinearEquiv.symmMap_rankOne_apply, star_one, _root_.map_one] theorem Qam.Nontracial.CompleteGraph.is_reflexive {E : Type _} [NormedAddCommGroupOfRing E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] : - schurIdempotent (Qam.completeGraph E) 1 = 1 := + schurIdempotent (Qam.completeGraph E E) 1 = 1 := by obtain ⟨α, β, hαβ⟩ := (1 : l(E)).exists_sum_rankOne nth_rw 1 [hαβ] @@ -330,23 +356,36 @@ theorem Pi.Qam.Lm.Nontracial.is_unreflexive_iff_reflexive_add_one [Nonempty p] inv_mul_cancel (Pi.Qam.Nontracial.delta_ne_zero hφ₂), one_smul, add_left_eq_self] rw [smul_eq_zero_iff_right (inv_ne_zero (Pi.Qam.Nontracial.delta_ne_zero hφ₂))] -theorem Qam.refl_idempotent_completeGraph_left {E : Type _} [NormedAddCommGroupOfRing E] - [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] - (x : l(E)) : schurIdempotent (Qam.completeGraph E) x = x := +theorem Qam.refl_idempotent_completeGraph_left {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] + [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] + [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] + [SMulCommClass ℂ E₂ E₂] + (x : E₂ →ₗ[ℂ] E₁) : schurIdempotent (Qam.completeGraph E₁ E₂) x = x := schurIdempotent_one_one_left _ -theorem Qam.refl_idempotent_completeGraph_right {E : Type _} [NormedAddCommGroupOfRing E] - [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] - (x : l(E)) : schurIdempotent x (Qam.completeGraph E) = x := +theorem Qam.refl_idempotent_completeGraph_right {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] + [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] + [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] + [SMulCommClass ℂ E₂ E₂] + (x : E₂ →ₗ[ℂ] E₁) : schurIdempotent x (Qam.completeGraph E₁ E₂) = x := schurIdempotent_one_one_right _ -noncomputable def Qam.complement' {E : Type _} [NormedAddCommGroupOfRing E] [InnerProductSpace ℂ E] - [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] (x : l(E)) : l(E) := - Qam.completeGraph E - x - -theorem Qam.Nontracial.Complement'.qam {E : Type _} [NormedAddCommGroupOfRing E] - [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] - (x : l(E)) : +noncomputable def Qam.complement' {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] + [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] + [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] + [SMulCommClass ℂ E₂ E₂] + (x : E₂ →ₗ[ℂ] E₁) : E₂ →ₗ[ℂ] E₁ := + Qam.completeGraph E₁ E₂ - x + +theorem Qam.Nontracial.Complement'.qam {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] + [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] + [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] + [SMulCommClass ℂ E₂ E₂] + (x : E₁ →ₗ[ℂ] E₂) : schurIdempotent x x = x ↔ schurIdempotent (Qam.complement' x) (Qam.complement' x) = Qam.complement' x := by @@ -357,22 +396,28 @@ theorem Qam.Nontracial.Complement'.qam {E : Type _} [NormedAddCommGroupOfRing E] simp only [sub_eq_zero, @eq_comm _ x] theorem Qam.Nontracial.Complement'.qam.isReal {φ : Module.Dual ℂ (Matrix p p ℂ)} - [hφ : φ.IsFaithfulPosMap] (x : l(Matrix p p ℂ)) : x.IsReal ↔ (Qam.complement' x).IsReal := + {ψ : Module.Dual ℂ (Matrix p₂ p₂ ℂ)} + [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] + (x : (Matrix p p ℂ) →ₗ[ℂ] (Matrix p₂ p₂ ℂ)) : x.IsReal ↔ (Qam.complement' x).IsReal := by simp only [Qam.complement', LinearMap.isReal_iff, LinearMap.real_sub, - (LinearMap.isReal_iff _).mp (@Qam.Nontracial.CompleteGraph.isReal p _ _ φ _)] + (LinearMap.isReal_iff _).mp (@Qam.Nontracial.CompleteGraph.isReal p₂ _ _ p _ _ ψ φ _ _)] simp only [sub_right_inj] theorem Pi.Qam.Nontracial.Complement'.Qam.isReal [hφ : ∀ i, (φ i).IsFaithfulPosMap] - (x : l(ℍ)) : x.IsReal ↔ (Qam.complement' x).IsReal := + [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + (x : ℍ →ₗ[ℂ] ℍ₂) : x.IsReal ↔ (Qam.complement' x).IsReal := by simp only [Qam.complement', LinearMap.isReal_iff, LinearMap.real_sub, - (LinearMap.isReal_iff _).mp (@Pi.Qam.Nontracial.CompleteGraph.isReal p _ n _ _ φ _)] + (LinearMap.isReal_iff _).mp (@Pi.Qam.Nontracial.CompleteGraph.isReal p₂ _ n₂ _ _ p _ _ n _ _ _ _ _ _)] simp only [sub_right_inj] -theorem Qam.complement'_complement' {E : Type _} [NormedAddCommGroupOfRing E] - [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] - (x : l(E)) : Qam.complement' (Qam.complement' x) = x := +theorem Qam.complement'_complement' {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] + [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] + [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] + [SMulCommClass ℂ E₂ E₂] + (x : E₁ →ₗ[ℂ] E₂) : Qam.complement' (Qam.complement' x) = x := sub_sub_cancel _ _ theorem Qam.Nontracial.Complement'.ir_reflexive {E : Type _} [NormedAddCommGroupOfRing E] @@ -493,12 +538,12 @@ theorem Pi.Qam.complement''_is_irreflexive_iff [Nonempty p] [∀ i, Nontrivial ( noncomputable def Pi.Qam.irreflexiveComplement [Nonempty p] [∀ i, Nontrivial (n i)] {δ : ℂ} (hφ : ∀ i, (φ i).IsFaithfulPosMap) (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) (x : l(ℍ)) : l(ℍ) := - Qam.completeGraph ℍ - Pi.Qam.trivialGraph hφ hφ₂ - x + Qam.completeGraph ℍ ℍ - Pi.Qam.trivialGraph hφ hφ₂ - x noncomputable def Pi.Qam.reflexiveComplement [Nonempty p] [∀ i, Nontrivial (n i)] {δ : ℂ} (hφ : ∀ i, (φ i).IsFaithfulPosMap) (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) (x : l(ℍ)) : l(ℍ) := - Qam.completeGraph ℍ + Pi.Qam.trivialGraph hφ hφ₂ - x + Qam.completeGraph ℍ ℍ + Pi.Qam.trivialGraph hφ hφ₂ - x theorem Qam.Nontracial.trivialGraph.isReal [Nonempty p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {δ : ℂ} (hφ₂ : φ.matrix⁻¹.trace = δ) : @@ -524,7 +569,7 @@ theorem Pi.Qam.irreflexiveComplement.isReal [Nonempty p] [∀ i, Nontrivial (n i [hφ : ∀ i, (φ i).IsFaithfulPosMap] (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} (hx : x.IsReal) : (Pi.Qam.irreflexiveComplement hφ hφ₂ x).IsReal := by rw [LinearMap.isReal_iff, Pi.Qam.irreflexiveComplement, LinearMap.real_sub, LinearMap.real_sub, - (LinearMap.isReal_iff (Qam.completeGraph ℍ)).mp Pi.Qam.Nontracial.CompleteGraph.isReal, + (LinearMap.isReal_iff (Qam.completeGraph ℍ ℍ)).mp Pi.Qam.Nontracial.CompleteGraph.isReal, (LinearMap.isReal_iff (Pi.Qam.trivialGraph hφ hφ₂)).mp (Pi.Qam.Nontracial.trivialGraph.isReal hφ₂), (LinearMap.isReal_iff x).mp hx] @@ -533,7 +578,7 @@ theorem Pi.Qam.reflexiveComplement.isReal [Nonempty p] [∀ i, Nontrivial (n i)] [hφ : ∀ i, (φ i).IsFaithfulPosMap] (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) {x : l(ℍ)} (hx : x.IsReal) : (Pi.Qam.reflexiveComplement hφ hφ₂ x).IsReal := by rw [LinearMap.isReal_iff, Pi.Qam.reflexiveComplement, LinearMap.real_sub, LinearMap.real_add, - (LinearMap.isReal_iff (Qam.completeGraph ℍ)).mp Pi.Qam.Nontracial.CompleteGraph.isReal, + (LinearMap.isReal_iff (Qam.completeGraph ℍ ℍ)).mp Pi.Qam.Nontracial.CompleteGraph.isReal, (LinearMap.isReal_iff (Pi.Qam.trivialGraph hφ hφ₂)).mp (Pi.Qam.Nontracial.trivialGraph.isReal hφ₂), (LinearMap.isReal_iff x).mp hx] @@ -551,18 +596,21 @@ theorem Pi.Qam.reflexiveComplement_reflexiveComplement [Nonempty p] [∀ i, Nont theorem Pi.Qam.trivialGraph_reflexiveComplement_eq_completeGraph [Nonempty p] [∀ i, Nontrivial (n i)] {δ : ℂ} [hφ : ∀ i, (φ i).IsFaithfulPosMap] (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) : - Pi.Qam.reflexiveComplement hφ hφ₂ (Pi.Qam.trivialGraph hφ hφ₂) = Qam.completeGraph ℍ := + Pi.Qam.reflexiveComplement hφ hφ₂ (Pi.Qam.trivialGraph hφ hφ₂) = Qam.completeGraph ℍ ℍ := by simp_rw [reflexiveComplement, add_sub_cancel_right] theorem Pi.Qam.completeGraph_reflexiveComplement_eq_trivialGraph [Nonempty p] [∀ i, Nontrivial (n i)] {δ : ℂ} [hφ : ∀ i, (φ i).IsFaithfulPosMap] (hφ₂ : ∀ i, (φ i).matrix⁻¹.trace = δ) : - Pi.Qam.reflexiveComplement hφ hφ₂ (Qam.completeGraph ℍ) = Pi.Qam.trivialGraph hφ hφ₂ := + Pi.Qam.reflexiveComplement hφ hφ₂ (Qam.completeGraph ℍ ℍ) = Pi.Qam.trivialGraph hφ hφ₂ := add_sub_cancel' _ _ -theorem Qam.complement'_eq {E : Type _} [NormedAddCommGroupOfRing E] [InnerProductSpace ℂ E] - [FiniteDimensional ℂ E] [IsScalarTower ℂ E E] [SMulCommClass ℂ E E] (a : l(E)) : - Qam.complement' a = Qam.completeGraph E - a := +theorem Qam.complement'_eq {E₁ E₂ : Type _} [NormedAddCommGroupOfRing E₁] + [NormedAddCommGroupOfRing E₂] + [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] + [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] + [SMulCommClass ℂ E₂ E₂] (a : E₂ →ₗ[ℂ] E₁) : + Qam.complement' a = Qam.completeGraph E₁ E₂ - a := rfl theorem Pi.Qam.irreflexiveComplement_is_irreflexive_qam_iff_irreflexive_qam [Nonempty p] diff --git a/Monlib/QuantumGraph/Iso.lean b/Monlib/QuantumGraph/Iso.lean index 096f135..d8db269 100644 --- a/Monlib/QuantumGraph/Iso.lean +++ b/Monlib/QuantumGraph/Iso.lean @@ -27,7 +27,7 @@ local notation "l(" x ")" => x →ₗ[ℂ] x variable {φ : Module.Dual ℂ (Matrix n n ℂ)} {ψ : Module.Dual ℂ (Matrix p p ℂ)} -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" => LinearMap.mul' ℂ (Matrix n n ℂ) diff --git a/Monlib/QuantumGraph/Mess.lean b/Monlib/QuantumGraph/Mess.lean index 09d8ecd..426a471 100644 --- a/Monlib/QuantumGraph/Mess.lean +++ b/Monlib/QuantumGraph/Mess.lean @@ -47,7 +47,7 @@ open scoped Matrix open Matrix -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" => LinearMap.mul' ℂ ℍ @@ -460,13 +460,14 @@ theorem grad_apply_of_real_Schur_idempotent [hφ : φ.IsFaithfulPosMap] {x : l( simp_rw [grad_apply, (LinearMap.isReal_iff _).mp hx1, ← LinearMap.comp_sub, ← LinearMap.comp_assoc, ← phiMap_mul, hx2] +-- open scoped FiniteDimensional theorem grad_of_real_Schur_idempotent_range [hφ : φ.IsFaithfulPosMap] {x : l(ℍ)} (hx1 : x.IsReal) (hx2 : Qam.reflIdempotent hφ x x = x) : LinearMap.range (grad hφ x) ≤ phiMap_of_real_Schur_idempotent.submodule hx1 hx2 := by + nth_rw 1 [← orthogonalProjection.range (phiMap_of_real_Schur_idempotent.submodule hx1 hx2)] rw [← grad_apply_of_real_Schur_idempotent hx1 hx2, ← phiMap_of_real_Schur_idempotent.orthogonal_projection_eq hx1 hx2] - nth_rw 2 [← orthogonalProjection.range (phiMap_of_real_Schur_idempotent.submodule hx1 hx2)] rw [LinearMap.range_le_iff_comap] -- rw [range_le_iff_comap], apply Submodule.ext @@ -897,7 +898,7 @@ theorem phi_map_left_inverse [hφ : φ.IsFaithfulPosMap] : phiInvMap hφ ∘ₗ phiInvMap, LinearMap.coe_mk, AddHom.coe_mk] simp_rw [LinearMap.comp_apply] simp_rw [← ιLinearEquiv_apply_eq, ← ιLinearEquiv_symm_apply_eq, LinearEquiv.symm_apply_apply] - have : (ιLinearEquiv hφ).symm 1 = Qam.completeGraph ℍ := + have : (ιLinearEquiv hφ).symm 1 = Qam.completeGraph ℍ ℍ := by simp_rw [ιLinearEquiv_symm_apply_eq, Algebra.TensorProduct.one_def, ιInvMap_apply, conjTranspose_one, _root_.map_one] diff --git a/Monlib/QuantumGraph/Nontracial.lean b/Monlib/QuantumGraph/Nontracial.lean index 00652af..72f13c7 100644 --- a/Monlib/QuantumGraph/Nontracial.lean +++ b/Monlib/QuantumGraph/Nontracial.lean @@ -28,6 +28,7 @@ variable {n p : Type _} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] open scoped TensorProduct BigOperators Kronecker local notation "ℍ" => Matrix n n ℂ +local notation "ℍ₂" => Matrix p p ℂ local notation "⊗K" => Matrix (n × n) (n × n) ℂ @@ -43,7 +44,7 @@ open scoped Matrix open Matrix -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" => LinearMap.mul' ℂ ℍ @@ -93,12 +94,13 @@ open TensorProduct theorem Finset.sum_fin_one {α : Type _} [AddCommMonoid α] (f : Fin 1 → α) : ∑ i, f i = f 0 := by simp only [Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton] -theorem rankOne_real_apply [hφ : φ.IsFaithfulPosMap] (a b : ℍ) : - (|a⟩⟨b| : ℍ →ₗ[ℂ] ℍ).real = |aᴴ⟩⟨hφ.sig (-1) bᴴ| := +theorem rankOne_real_apply [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] (a : ℍ) (b : ℍ₂) : + (|a⟩⟨b| : ℍ₂ →ₗ[ℂ] ℍ).real = |aᴴ⟩⟨hψ.sig (-1) bᴴ| := by have := - @Pi.rankOneLm_real_apply _ _ _ _ _ (fun _ : Fin 1 => φ) (fun _ => hφ) (fun _ : Fin 1 => a) - fun _ : Fin 1 => b + @Pi.rankOneLm_real_apply _ _ _ _ _ (fun _ : Fin 1 => φ) + _ _ _ _ _ _ (fun _ : Fin 1 => ψ) (fun _ => hφ) (fun _ => hψ) (fun _ : Fin 1 => a) + (fun _ : Fin 1 => b) simp only [LinearMap.ext_iff, Function.funext_iff, Fin.forall_fin_one, ← rankOneLm_eq_rankOne, rankOneLm_apply, LinearMap.real_apply] at this ⊢ simp only [Pi.star_apply, Pi.smul_apply, inner, @@ -106,12 +108,14 @@ theorem rankOne_real_apply [hφ : φ.IsFaithfulPosMap] (a b : ℍ) : intros x exact this (fun _ => x) -theorem Qam.RankOne.symmetric_eq [hφ : φ.IsFaithfulPosMap] (a b : ℍ) : - (LinearEquiv.symmMap ℂ ℍ ℍ) |a⟩⟨b| = |hφ.sig (-1) bᴴ⟩⟨aᴴ| := by +theorem Qam.RankOne.symmetric_eq [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] + (a : ℍ) (b : ℍ₂) : + (LinearEquiv.symmMap ℂ ℍ₂ ℍ) |a⟩⟨b| = |hψ.sig (-1) bᴴ⟩⟨aᴴ| := by simp_rw [LinearEquiv.symmMap_apply, rankOne_real_apply, ← rankOneLm_eq_rankOne, rankOneLm_adjoint] -theorem Qam.RankOne.symmetric'_eq [hφ : φ.IsFaithfulPosMap] (a b : ℍ) : - (LinearEquiv.symmMap ℂ ℍ ℍ).symm |a⟩⟨b| = |bᴴ⟩⟨hφ.sig (-1) aᴴ| := by +theorem Qam.RankOne.symmetric'_eq [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] + (a : ℍ) (b : ℍ₂) : + (LinearEquiv.symmMap ℂ ℍ ℍ₂).symm |a⟩⟨b| = |bᴴ⟩⟨hφ.sig (-1) aᴴ| := by simp_rw [LinearEquiv.symmMap_symm_apply, ← rankOneLm_eq_rankOne, rankOneLm_adjoint, rankOneLm_eq_rankOne, rankOne_real_apply] diff --git a/Monlib/QuantumGraph/QamA.lean b/Monlib/QuantumGraph/QamA.lean index a002587..1b0bcfb 100644 --- a/Monlib/QuantumGraph/QamA.lean +++ b/Monlib/QuantumGraph/QamA.lean @@ -41,7 +41,7 @@ open scoped Matrix open Matrix -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" => LinearMap.mul' ℂ ℍ diff --git a/Monlib/QuantumGraph/SchurIdempotent.lean b/Monlib/QuantumGraph/SchurIdempotent.lean index 3b12558..82256e7 100644 --- a/Monlib/QuantumGraph/SchurIdempotent.lean +++ b/Monlib/QuantumGraph/SchurIdempotent.lean @@ -24,10 +24,13 @@ import Monlib.LinearAlgebra.Nacgor variable {n : Type _} [Fintype n] [DecidableEq n] {s : n → Type _} [∀ i, Fintype (s i)] [∀ i, DecidableEq (s i)] + {n₂ : Type _} [Fintype n₂] [DecidableEq n₂] {s₂ : n₂ → Type _} [∀ i, Fintype (s₂ i)] + [∀ i, DecidableEq (s₂ i)] open scoped TensorProduct BigOperators Kronecker local notation "𝔹" => PiMat ℂ n s +local notation "𝔹₂" => PiMat ℂ n₂ s₂ local notation "l(" x ")" => x →ₗ[ℂ] x @@ -37,7 +40,7 @@ open scoped Matrix open Matrix -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" x => LinearMap.mul' ℂ x @@ -103,15 +106,19 @@ noncomputable def schurIdempotent {B C : Type _} [NormedAddCommGroupOfRing B] scoped[schurIdempotent] infix:100 " •ₛ " => schurIdempotent open scoped schurIdempotent -theorem schurIdempotent.apply_rankOne {B : Type _} [NormedAddCommGroupOfRing B] - [InnerProductSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [FiniteDimensional ℂ B] - (a b c d : B) : (↑|a⟩⟨b|) •ₛ (↑|c⟩⟨d|) = (|a * c⟩⟨b * d| : B →ₗ[ℂ] B) := +theorem schurIdempotent.apply_rankOne {B C : Type _} [NormedAddCommGroupOfRing B] + [NormedAddCommGroupOfRing C] [InnerProductSpace ℂ B] [InnerProductSpace ℂ C] + [SMulCommClass ℂ B B] [SMulCommClass ℂ C C] [IsScalarTower ℂ B B] [IsScalarTower ℂ C C] + [FiniteDimensional ℂ B] [FiniteDimensional ℂ C] + (a : B) (b : C) (c : B) (d : C) : (↑|a⟩⟨b|) •ₛ (↑|c⟩⟨d|) = (|a * c⟩⟨b * d| : C →ₗ[ℂ] B) := by - rw [schurIdempotent, LinearMap.ext_iff_inner_map] + rw [schurIdempotent, LinearMap.ext_iff] intro x + apply ext_inner_right ℂ + intro u simp only [ContinuousLinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk, rankOne_apply, LinearMap.comp_apply] - obtain ⟨α, β, h⟩ := TensorProduct.eq_span ((LinearMap.adjoint (LinearMap.mul' ℂ B)) x) + obtain ⟨α, β, h⟩ := TensorProduct.eq_span ((LinearMap.adjoint (LinearMap.mul' ℂ C)) x) rw [← h] simp_rw [map_sum, TensorProduct.map_tmul, ContinuousLinearMap.coe_coe, rankOne_apply, LinearMap.mul'_apply, smul_mul_smul, ← TensorProduct.inner_tmul, ← Finset.sum_smul, ← inner_sum, @@ -138,16 +145,20 @@ theorem schurIdempotent.apply_rankOne {B : Type _} [NormedAddCommGroupOfRing B] -- { simp only [equiv.apply_symm_apply, eq_self_iff_true, forall_true_iff], }, -- end, -- end -theorem schurIdempotent_one_one_right {B : Type _} [NormedAddCommGroupOfRing B] - [InnerProductSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [FiniteDimensional ℂ B] - (A : l(B)) : A •ₛ (|(1 : B)⟩⟨(1 : B)| : l(B)) = A := +theorem schurIdempotent_one_one_right {B C : Type _} [NormedAddCommGroupOfRing B] + [NormedAddCommGroupOfRing C] [InnerProductSpace ℂ B] [InnerProductSpace ℂ C] + [SMulCommClass ℂ B B] [SMulCommClass ℂ C C] [IsScalarTower ℂ B B] [IsScalarTower ℂ C C] + [FiniteDimensional ℂ B] [FiniteDimensional ℂ C] + (A : C →ₗ[ℂ] B) : A •ₛ (|(1 : B)⟩⟨(1 : C)| : C →ₗ[ℂ] B) = A := by obtain ⟨α, β, rfl⟩ := LinearMap.exists_sum_rankOne A simp_rw [map_sum, LinearMap.sum_apply, schurIdempotent.apply_rankOne, mul_one] -theorem schurIdempotent_one_one_left {B : Type _} [NormedAddCommGroupOfRing B] - [InnerProductSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [FiniteDimensional ℂ B] - (A : l(B)) : (|(1 : B)⟩⟨(1 : B)| : l(B)) •ₛ A = A := +theorem schurIdempotent_one_one_left {B C : Type _} [NormedAddCommGroupOfRing B] + [NormedAddCommGroupOfRing C] [InnerProductSpace ℂ B] [InnerProductSpace ℂ C] + [SMulCommClass ℂ B B] [SMulCommClass ℂ C C] [IsScalarTower ℂ B B] [IsScalarTower ℂ C C] + [FiniteDimensional ℂ B] [FiniteDimensional ℂ C] + (A : C →ₗ[ℂ] B) : (|(1 : B)⟩⟨(1 : C)| : C →ₗ[ℂ] B) •ₛ A = A := by obtain ⟨α, β, rfl⟩ := LinearMap.exists_sum_rankOne A simp_rw [map_sum, schurIdempotent.apply_rankOne, one_mul] @@ -211,8 +222,10 @@ theorem schurIdempotent_real -- [star_module ℂ B] -- {ψ : module.dual ℂ B} (hψ : ∀ a b, ⟪a, b⟫_ℂ = ψ (star a * b)) {ψ : ∀ i, Module.Dual ℂ (Matrix (s i) (s i) ℂ)} - [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (x y : l(𝔹)) : - LinearMap.real (x •ₛ y : l(𝔹)) = (LinearMap.real y) •ₛ (LinearMap.real x) := + {φ : ∀ i, Module.Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} + [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + [hφ : ∀ i, (φ i).IsFaithfulPosMap] (x y : 𝔹 →ₗ[ℂ] 𝔹₂) : + LinearMap.real (x •ₛ y : 𝔹 →ₗ[ℂ] 𝔹₂) = (LinearMap.real y) •ₛ (LinearMap.real x) := by obtain ⟨α, β, rfl⟩ := x.exists_sum_rankOne obtain ⟨γ, ζ, rfl⟩ := y.exists_sum_rankOne diff --git a/Monlib/QuantumGraph/Symm.lean b/Monlib/QuantumGraph/Symm.lean index 42650ae..5a793b6 100644 --- a/Monlib/QuantumGraph/Symm.lean +++ b/Monlib/QuantumGraph/Symm.lean @@ -34,10 +34,13 @@ open scoped TensorProduct Kronecker Matrix Functional variable {n : Type _} [Fintype n] [DecidableEq n] {s : n → Type _} [∀ i, Fintype (s i)] [∀ i, DecidableEq (s i)] {ψ : ∀ i, Module.Dual ℂ (Matrix (s i) (s i) ℂ)} + {n₂ : Type _} [Fintype n₂] [DecidableEq n₂] {s₂ : n₂ → Type _} [∀ i, Fintype (s₂ i)] + [∀ i, DecidableEq (s₂ i)] {φ : ∀ i, Module.Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} local notation "𝔹" => PiMat ℂ n s +local notation "𝔹₂" => PiMat ℂ n₂ s₂ -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" x => LinearMap.mul' ℂ x @@ -64,20 +67,22 @@ local notation "τ⁻¹" x => local notation "id" x => (1 : x →ₗ[ℂ] x) -theorem LinearEquiv.symmMap_rankOne_apply [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (a b : 𝔹) : - LinearEquiv.symmMap _ _ _ (|a⟩⟨b| : 𝔹 →ₗ[ℂ] 𝔹) = - |Module.Dual.pi.IsFaithfulPosMap.sig hψ (-1) (star b)⟩⟨star a| := - by - rw [LinearEquiv.symmMap_apply, ← rankOneLm_eq_rankOne, Pi.rankOneLm_real_apply, rankOneLm_adjoint] - rfl - -theorem LinearEquiv.symmMap_symm_rankOne_apply [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (a b : 𝔹) : - (LinearEquiv.symmMap _ _ _).symm (|a⟩⟨b| : 𝔹 →ₗ[ℂ] 𝔹) = +theorem LinearEquiv.symmMap_rankOne_apply [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + [hφ : ∀ i, (φ i).IsFaithfulPosMap] + (a : 𝔹) (b : 𝔹₂) : + LinearEquiv.symmMap _ _ _ (|a⟩⟨b| : 𝔹₂ →ₗ[ℂ] 𝔹) = + |Module.Dual.pi.IsFaithfulPosMap.sig hφ (-1) (star b)⟩⟨star a| := +by + rw [LinearEquiv.symmMap_apply, ← rankOneLm_eq_rankOne, Pi.rankOneLm_real_apply, + rankOneLm_adjoint] + +theorem LinearEquiv.symmMap_symm_rankOne_apply [hψ : ∀ i, (ψ i).IsFaithfulPosMap] + [hφ : ∀ i, (φ i).IsFaithfulPosMap] (a : 𝔹) (b : 𝔹₂) : + (LinearEquiv.symmMap _ _ _).symm (|a⟩⟨b| : 𝔹₂ →ₗ[ℂ] 𝔹) = |star b⟩⟨Module.Dual.pi.IsFaithfulPosMap.sig hψ (-1) (star a)| := - by +by rw [LinearEquiv.symmMap_symm_apply, ← rankOneLm_eq_rankOne, rankOneLm_adjoint, Pi.rankOneLm_real_apply] - rfl open scoped BigOperators diff --git a/Monlib/QuantumGraph/ToProjections.lean b/Monlib/QuantumGraph/ToProjections.lean index d6bc316..49debee 100644 --- a/Monlib/QuantumGraph/ToProjections.lean +++ b/Monlib/QuantumGraph/ToProjections.lean @@ -45,7 +45,7 @@ open scoped Matrix open Matrix -local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y +local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y local notation "m" => LinearMap.mul' ℂ ℍ @@ -186,7 +186,7 @@ private theorem matrix.stdBasisMatrix.transpose' {R n p : Type _} [DecidableEq n -- tidy, }, -- } -set_option maxHeartbeats 300000 in +set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 0 in theorem rankOne_toMatrix_transpose_psi_symm [hφ : φ.IsFaithfulPosMap] (x y : ℍ) : @@ -244,21 +244,23 @@ private theorem is_idempotent_elem_to_clm {𝕜 E : Type _} [RCLike 𝕜] [Norme IsIdempotentElem p ↔ IsIdempotentElem (toContinuousLinearMap p) := by simp_rw [IsIdempotentElem, lm_to_clm_comp, Function.Injective.eq_iff (LinearEquiv.injective _)] +open scoped FiniteDimensional open LinearMap in private theorem is_self_adjoint_to_clm {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] [FiniteDimensional 𝕜 E] {p : E →ₗ[𝕜] E} : + [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {p : E →ₗ[𝕜] E} : IsSelfAdjoint p ↔ IsSelfAdjoint (toContinuousLinearMap p) := by simp_rw [_root_.IsSelfAdjoint, ContinuousLinearMap.star_eq_adjoint, ← LinearMap.adjoint_toContinuousLinearMap, Function.Injective.eq_iff (LinearEquiv.injective _), LinearMap.star_eq_adjoint] open LinearMap in +set_option synthInstance.maxHeartbeats 300000 in theorem orthogonal_projection_iff_lm {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] - [InnerProductSpace 𝕜 E] [CompleteSpace E] [FiniteDimensional 𝕜 E] {p : E →ₗ[𝕜] E} : + [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {p : E →ₗ[𝕜] E} : (∃ U : Submodule 𝕜 E, (orthogonalProjection' U : E →ₗ[𝕜] E) = p) ↔ IsSelfAdjoint p ∧ IsIdempotentElem p := by - have := @orthogonal_projection_iff 𝕜 E _ _ _ _ _ (toContinuousLinearMap p) + have := @orthogonal_projection_iff 𝕜 E _ _ _ _ (toContinuousLinearMap p) simp_rw [is_idempotent_elem_to_clm, is_self_adjoint_to_clm] at this ⊢ rw [← this] constructor @@ -271,11 +273,11 @@ theorem orthogonal_projection_iff_lm {𝕜 E : Type _} [RCLike 𝕜] [NormedAddC rfl theorem Matrix.conj_eq_transpose_conjTranspose {R n₁ n₂ : Type _} [Star R] (A : Matrix n₁ n₂ R) : - Aᴴᵀ = Aᵀᴴ := + Aᴴᵀ = (Aᵀ)ᴴ := rfl theorem Matrix.conj_eq_conjTranspose_transpose {R n₁ n₂ : Type _} [Star R] (A : Matrix n₁ n₂ R) : - Aᴴᵀ = Aᴴᵀ := + Aᴴᵀ = (Aᴴ)ᵀ := rfl set_option synthInstance.maxHeartbeats 50000 in @@ -482,13 +484,13 @@ theorem RealQam.edges_eq [hφ : φ.IsFaithfulPosMap] {A : l(ℍ)} (hA : RealQam simp_rw [trace_sum, ← Matrix.mul_assoc, this, Finset.sum_const, Finset.card_fin, Nat.smul_one_eq_coe] -theorem completeGraphRealQam [hφ : φ.IsFaithfulPosMap] : RealQam hφ (Qam.completeGraph ℍ) := +theorem completeGraphRealQam [hφ : φ.IsFaithfulPosMap] : RealQam hφ (Qam.completeGraph ℍ ℍ) := ⟨Qam.Nontracial.CompleteGraph.qam, Qam.Nontracial.CompleteGraph.isReal⟩ theorem Qam.completeGraph_edges [hφ : φ.IsFaithfulPosMap] : (@completeGraphRealQam p _ _ φ hφ).edges = FiniteDimensional.finrank ℂ (⊤ : Submodule ℂ ℍ) := by - have this : (RealQam.edges completeGraphRealQam : ℂ) = (Qam.completeGraph ℍ φ.matrix⁻¹).trace := RealQam.edges_eq _ + have this : (RealQam.edges completeGraphRealQam : ℂ) = (Qam.completeGraph ℍ ℍ φ.matrix⁻¹).trace := RealQam.edges_eq _ haveI ig := hφ.matrixIsPosDef.invertible simp_rw [Qam.completeGraph, ContinuousLinearMap.coe_coe, rankOne_apply, Module.Dual.IsFaithfulPosMap.inner_eq', conjTranspose_one, Matrix.mul_one, @@ -580,6 +582,7 @@ theorem RealQam.edges_eq_dim_iff [hφ : φ.IsFaithfulPosMap] {A : l(ℍ)} (hA : rw [← this'', AlgEquiv.toLinearMap_apply, MulEquivClass.map_eq_one_iff] at this' exact this' +set_option synthInstance.maxHeartbeats 300000 in private theorem orthogonal_projection_of_dim_one {𝕜 E : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {U : Submodule 𝕜 E} (hU : FiniteDimensional.finrank 𝕜 U = 1) : diff --git a/Monlib/RepTheory/AutMat.lean b/Monlib/RepTheory/AutMat.lean index ad6c89c..b9b9747 100644 --- a/Monlib/RepTheory/AutMat.lean +++ b/Monlib/RepTheory/AutMat.lean @@ -417,6 +417,7 @@ theorem aut_mat_inner_trace_preserving [DecidableEq n] (f : (M n) ≃ₐ[𝕜] M (f x).trace = x.trace := by obtain ⟨T, rfl⟩ := aut_mat_inner' f rw [Algebra.autInner_apply, trace_mul_comm, Matrix.invOf_mul_self_assoc] +alias AlgEquiv.apply_matrix_trace := aut_mat_inner_trace_preserving /-- if a matrix commutes with all matrices, then it is equal to a scalar multiplied by the identity -/ @@ -851,34 +852,56 @@ by simp [FiniteDimensional.finrank_matrix, ← pow_two] at this exact this.symm -def perm_perm_aux {R ι : Type*} [CommSemiring R] [Fintype ι] [DecidableEq ι] {n : ι → Type*} - [Π i, Fintype (n i)] [Π i, DecidableEq (n i)] (σ : Equiv.Perm ι) (x : PiMat R ι n) (i : ι) : - PiMat R ι n := -λ j => if (i = σ.symm j) then (x j) else 0 -@[simps] -def _root_.Pi.perm_of_perm {R ι : Type*} [CommSemiring R] [Fintype ι] [DecidableEq ι] {n : ι → Type*} - [Π i, Fintype (n i)] [Π i, DecidableEq (n i)] (σ : Equiv.Perm ι) : - PiMat R ι n ≃ₐ[R] PiMat R ι n := -{ toFun := λ x => ∑ i, perm_perm_aux σ x i - invFun := λ x => ∑ i, perm_perm_aux σ.symm x i - left_inv := λ x => by - ext1 i - simp only [Finset.sum_apply, perm_perm_aux, Finset.sum_ite_eq', Finset.mem_univ, if_true] - right_inv := λ x => by - ext1 i - simp only [Finset.sum_apply, perm_perm_aux, Finset.sum_ite_eq', Finset.mem_univ, if_true] - map_add' := λ x y => by - ext1 i - simp only [Finset.sum_apply, perm_perm_aux, Pi.add_apply] - simp only [Finset.sum_add_distrib, ite_add_zero] - map_mul' := λ x y => by - ext1 i - simp only [Finset.sum_apply, perm_perm_aux, Pi.mul_apply] - simp only [Finset.sum_mul, Finset.mul_sum, ite_mul, zero_mul, mul_ite, mul_zero, - Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] - commutes' := λ r => by - ext1 i - simp only [Finset.sum_apply, perm_perm_aux, Pi.smul_apply, Algebra.algebraMap_eq_smul_one] - simp only [Pi.one_apply, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] } +-- def perm_perm_aux {R ι : Type*} [CommSemiring R] [Fintype ι] [DecidableEq ι] {n : ι → Type*} +-- (σ : Equiv.Perm ι) +-- -- (hσ : ∀ i, n (σ i) = n i) +-- (i : ι) : +-- Type u_3 := +-- n (σ i) +-- have hσ' : ∀ i, n (σ.symm i) = n i := λ j => by + -- rw [← hσ, Equiv.apply_symm_apply] + +-- @[simps] +-- def _root_.Pi.perm_of_perm {R ι : Type*} [CommSemiring R] [Fintype ι] [DecidableEq ι] {n : ι → Type*} +-- [Π i, Fintype (n i)] [Π i, DecidableEq (n i)] (σ : Equiv.Perm ι) : +-- -- haveI : Π i, Fintype ((n ∘ σ) i) := λ i => by +-- -- simp [Function.comp_apply] +-- -- infer_instance +-- -- haveI : Π i, DecidableEq ((n ∘ σ) i) := λ i => by infer_instance +-- -- -- haveI : Semiring (PiMat R ι (n ∘ ⇑σ)) := by +-- -- -- infer_instance +-- -- -- haveI : Π i, Semiring (Matrix ((n ∘ ⇑σ) i) ((n ∘ σ) i) R) := by infer_instance +-- -- haveI : Π i, Algebra R (Matrix ((n ∘ ⇑σ) i) ((n ∘ σ) i) R) := by +-- -- intro i +-- -- infer_instance +-- -- haveI : Algebra R (PiMat R ι (n ∘ ⇑σ)) := Pi.algebra _ _ +-- -- -- (hσ : ∀ i, n (σ i) = n i) : +-- PiMat R ι n ≃ₐ[R] σ (PiMat R ι n) := +-- -- have hσ' : ∀ i, n (σ.symm i) = n i := λ j => by +-- -- rw [← hσ, Equiv.apply_symm_apply] +-- { toFun := λ x => ∑ i, perm_perm_aux σ x i +-- invFun := λ x => ∑ i, perm_perm_aux σ.symm x i +-- left_inv := λ x => by +-- ext1 i +-- simp only [Finset.sum_apply, perm_perm_aux, Finset.sum_ite_eq', Finset.mem_univ, if_true] +-- -- simp only [Equiv.symm_symm_apply, eq_mpr_eq_cast, cast_cast] +-- -- simp_all [hσ, hσ', Equiv.symm_apply_apply, cast_eq_iff_heq] + +-- right_inv := λ x => by +-- ext1 i +-- simp only [Finset.sum_apply, perm_perm_aux, Finset.sum_ite_eq', Finset.mem_univ, if_true] +-- map_add' := λ x y => by +-- ext1 i +-- simp only [Finset.sum_apply, perm_perm_aux, Pi.add_apply] +-- simp only [Finset.sum_add_distrib, ite_add_zero] +-- map_mul' := λ x y => by +-- ext1 i +-- simp only [Finset.sum_apply, perm_perm_aux, Pi.mul_apply] +-- simp only [Finset.sum_mul, Finset.mul_sum, ite_mul, zero_mul, mul_ite, mul_zero, +-- Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] +-- commutes' := λ r => by +-- ext1 i +-- simp only [Finset.sum_apply, perm_perm_aux, Pi.smul_apply, Algebra.algebraMap_eq_smul_one] +-- simp only [Pi.one_apply, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] } end Matrix