diff --git a/ClassicalInfo/Distribution.lean b/ClassicalInfo/Distribution.lean index 10f3a71..68e39c5 100644 --- a/ClassicalInfo/Distribution.lean +++ b/ClassicalInfo/Distribution.lean @@ -143,8 +143,7 @@ def extend_left (d : Distribution α) : Distribution (β ⊕ α) := /-- Make a convex mixture of two distributions on the same set. -/ instance instMixable : Mixable (α → ℝ) (Distribution α) := Mixable.instSubtype (inferInstance) (fun _ _ hab hx hy ↦ by - admit -- admitting out because Aristotle fails to load it otherwise - -- simp [Mixable.mix_ab, Finset.sum_add_distrib, ← Finset.mul_sum, hab, hx, hy] + simp [Mixable.mix_ab, Finset.sum_add_distrib, ← Finset.mul_sum, hab, hx, hy] ) /-- Given a distribution on type α and an equivalence to type β, get the corresponding @@ -198,7 +197,7 @@ theorem fin_two_eq_coin (d : Distribution (Fin 2)) : d = coin (d 0) := by fin_cases i · simp [coin] · simpa only [coin, Fin.mk_one, funlike_apply, one_ne_zero, ↓reduceIte, - Prob.coe_one_minus, Subtype.eq_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm, + Prob.coe_one_minus, Subtype.ext_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm, fun_eq_val, Fin.sum_univ_two] using d.property theorem coin_eq_iff (p : Prob) (f : Distribution (Fin 2)) : @@ -252,7 +251,7 @@ theorem expect_val_eq_mixable_mix (d : Distribution (Fin 2)) (x₁ x₂ : T) : e simp _ = (d 0 : ℝ) • Mixable.to_U x₁ + (1 - d 0).val • Mixable.to_U x₂ := by congr - simpa only [Subtype.eq_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm, + simpa only [Subtype.ext_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm, fun_eq_val, Fin.sum_univ_two] using d.property /-- The expectation value of a random variable with constant probability distribution `constant x` is its value at `x` -/ diff --git a/ClassicalInfo/Prob.lean b/ClassicalInfo/Prob.lean index 33f2b57..4235590 100644 --- a/ClassicalInfo/Prob.lean +++ b/ClassicalInfo/Prob.lean @@ -85,11 +85,11 @@ instance instInhabited : Inhabited Prob where default := 0 instance : LinearOrderedCommMonoidWithZero Prob where - mul_le_mul_left := by - intros a b h c - rw [← Subtype.coe_le_coe] - exact mul_le_mul_of_nonneg_left h c.2.1 - zero_le_one := (0 : Prob).2.2 + mul_lt_mul_of_pos_left := by + intros a ha b h hb + rw [← Subtype.coe_lt_coe] + exact mul_lt_mul_of_pos_left hb ha + zero_le a := a.2.1 @[simp] theorem zero_le_coe {p : Prob} : 0 ≤ (p : ℝ) := @@ -107,11 +107,11 @@ theorem zero_le {p : Prob} : 0 ≤ p := theorem le_one {p : Prob} : p ≤ 1 := coe_le_one -@[ext] protected theorem eq {n m : Prob} : (n : ℝ) = (m : ℝ) → n = m := - Subtype.eq +@[ext] protected theorem ext {n m : Prob} : (n : ℝ) = (m : ℝ) → n = m := + Subtype.ext theorem ne_iff {x y : Prob} : (x : ℝ) ≠ (y : ℝ) ↔ x ≠ y := - not_congr <| Prob.eq_iff.symm + not_congr <| Prob.ext_iff.symm @[simp, norm_cast] theorem toReal_mul (x y : Prob) : (x * y : Prob) = (x : ℝ) * (y : ℝ) := by @@ -209,7 +209,7 @@ theorem mul_eq_one_iff (p q : Prob) : p * q = 1 ↔ p = 1 ∧ q = 1 := by cases p cases q refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩ - simp [Prob.eq_iff] at h ⊢ + simp [Prob.ext_iff] at h ⊢ constructor <;> nlinarith end Prob @@ -351,7 +351,7 @@ namespace Prob /-- Probabilities `Prob` themselves are convex. -/ instance instMixable : Mixable ℝ Prob where to_U := Subtype.val - to_U_inj := Prob.eq + to_U_inj := Prob.ext mkT := fun h ↦ ⟨⟨_, Exists.casesOn h fun t ht => ht ▸ t.prop⟩, rfl⟩ convex := by simp [Convex, StarConvex] @@ -440,7 +440,7 @@ theorem le_negLog_of_le_exp {p : Prob} {x : ℝ} (h : p ≤ Real.exp (-x)) : ENN rw [← ENNReal.toReal_lt_toReal ofReal_ne_top coe_ne_top, toReal_ofReal hx] simpa using lt_neg_of_lt_neg h · apply le_of_eq - rw [← ENNReal.toReal_eq_toReal ofReal_ne_top coe_ne_top, + rw [← ENNReal.toReal_eq_toReal_iff' ofReal_ne_top coe_ne_top, coe_toReal, coe_mk, h, Real.log_exp, neg_neg, toReal_ofReal hx] · trans 0 · simp only [nonpos_iff_eq_zero, ofReal_eq_zero, le_of_not_ge hx] diff --git a/QuantumInfo/ForMathlib/ContinuousLinearMap.lean b/QuantumInfo/ForMathlib/ContinuousLinearMap.lean index a059b92..205d701 100644 --- a/QuantumInfo/ForMathlib/ContinuousLinearMap.lean +++ b/QuantumInfo/ForMathlib/ContinuousLinearMap.lean @@ -18,16 +18,17 @@ variable [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddComm variable [Module R M] [Module S M₂] --These two theorems might look a bit silly as aliases of `LinearMap.____`, but they don't `simp` on their +--TODO: I think we can remove these now that we've bumped to Lean 4.28.0 @[simp] -theorem range_zero [RingHomSurjective σ] : LinearMap.range (0 : M →SL[σ] M₂) = ⊥ := - LinearMap.range_zero +theorem range_zero [RingHomSurjective σ] : (0 : M →SL[σ] M₂).range = ⊥ := by + simp @[simp] -theorem ker_zero : LinearMap.ker (0 : M →SL[σ] M₂) = ⊤ := - LinearMap.ker_zero +theorem ker_zero : (0 : M →SL[σ] M₂).ker = ⊤ := by + simp theorem ker_mk (f : M →ₛₗ[σ] M₂) (hf : Continuous f.toFun) : - LinearMap.ker (ContinuousLinearMap.mk f hf) = LinearMap.ker f := by + (ContinuousLinearMap.mk f hf).ker = LinearMap.ker f := by rfl end ContinuousLinearMap @@ -38,7 +39,7 @@ variable {n 𝕜 : Type*} [Fintype n] [RCLike 𝕜] /-- The support of a Hermitian matrix is the sum of its nonzero eigenspaces. -/ theorem support_eq_sup_eigenspace_nonzero (A : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) - (hA : A.IsSymmetric) : LinearMap.range A = ⨆ μ ≠ 0, Module.End.eigenspace A μ := by + (hA : A.IsSymmetric) : A.range = ⨆ μ ≠ 0, Module.End.eigenspace A μ := by apply le_antisymm · rintro x ⟨y, hy⟩ have h_decomp : y ∈ ⨆ (μ : 𝕜), Module.End.eigenspace A.toLinearMap μ := by @@ -53,7 +54,7 @@ theorem support_eq_sup_eigenspace_nonzero (A : EuclideanSpace 𝕜 n →L[𝕜] exact rfl have h_eigen (i) : A (f i) = (i : 𝕜) • f i := Module.End.mem_eigenspace_iff.mp (hf₁ i) - rw [← hy, h_apply_A, Finset.sum_congr rfl (fun i _ ↦ h_eigen i)] + rw [← hy, coe_coe, h_apply_A, Finset.sum_congr rfl (fun i _ ↦ h_eigen i)] refine Submodule.sum_mem _ fun i _ ↦ ?_ by_cases hi0 : i = 0 · simp [hi0] diff --git a/QuantumInfo/ForMathlib/Filter.lean b/QuantumInfo/ForMathlib/Filter.lean index 3b3888e..933170f 100644 --- a/QuantumInfo/ForMathlib/Filter.lean +++ b/QuantumInfo/ForMathlib/Filter.lean @@ -31,7 +31,7 @@ theorem Filter.Tendsto_inv_nat_mul_div_real (m : ℕ) simpa [ div_eq_inv_mul ] using Nat.floor_le ( by positivity : 0 ≤ ( x : ℝ ) / m ); -- Apply the squeeze theorem to conclude the proof. have h_squeeze : Filter.Tendsto (fun x : ℕ => (1 / m : ℝ) - 1 / x) Filter.atTop (nhds (1 / m)) := by - simpa using tendsto_const_nhds.sub ( _root_.tendsto_inverse_atTop_nhds_zero_nat ); + simpa using tendsto_const_nhds.sub (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ)) exact tendsto_of_tendsto_of_tendsto_of_le_of_le' h_squeeze tendsto_const_nhds ( Filter.eventually_atTop.mpr ⟨ 1, fun x hx => h_floor_bound x hx |>.1 ⟩ ) ( Filter.eventually_atTop.mpr ⟨ 1, fun x hx => h_floor_bound x hx |>.2 ⟩ ); -- Apply the hypothesis `h_floor` to conclude the proof. convert h_floor using 1; diff --git a/QuantumInfo/ForMathlib/LimSupInf.lean b/QuantumInfo/ForMathlib/LimSupInf.lean index c9db374..6a6bb69 100644 --- a/QuantumInfo/ForMathlib/LimSupInf.lean +++ b/QuantumInfo/ForMathlib/LimSupInf.lean @@ -1,9 +1,15 @@ import Mathlib.Algebra.Order.Ring.Star import Mathlib.Analysis.Normed.Ring.Lemmas +import Mathlib.Data.Finset.Attr import Mathlib.Data.Int.Star import Mathlib.Data.Real.StarOrdered +import Mathlib.Tactic.Bound import Mathlib.Tactic.Peel -import Mathlib.Topology.Compactness.PseudometrizableLindelof +import Mathlib.Tactic.Common +import Mathlib.Tactic.Continuity +import Mathlib.Tactic.Finiteness.Attr +import Mathlib.Tactic.SetLike +import Mathlib.Util.CompileInductive import Mathlib.Topology.Instances.ENNReal.Lemmas import Mathlib.Topology.Instances.Nat @@ -142,7 +148,9 @@ lemma exists_liminf_zero_of_forall_liminf_le (y : ℝ≥0) (f : ℝ≥0 → ℕ refine' lt_of_le_of_lt _ right; convert add_le_add_left ( ENNReal.ofReal_le_ofReal hk.le ) ( y : ℝ≥0∞ ) using 1 ; norm_num [ ENNReal.ofReal ]; · norm_num [ Real.toNNReal_inv ]; - · rw [ ENNReal.ofReal_sub ] <;> norm_num [ left.le ]; + rw [add_comm] + · rw [ENNReal.ofReal_sub _ (by positivity)] + simp [tsub_add_cancel_of_le, left.le] refine' ⟨ n ( Max.max x k ), _, _ ⟩ · simp_all only [ne_eq, add_eq_zero, Nat.cast_eq_zero, one_ne_zero, and_false, not_false_eq_true, ENNReal.coe_inv, ENNReal.coe_add, ENNReal.coe_natCast, ENNReal.coe_one] @@ -220,7 +228,7 @@ lemma exists_limsup_zero_of_forall_limsup_le (y : ℝ≥0) (f : ℝ≥0 → ℕ have := hM.2 ( Nat.findGreatest ( fun k => M k ≤ n ) n ) n ?_ · simp_all only [gt_iff_lt, ge_iff_le, one_div] obtain ⟨left, right⟩ := hM - exact le_trans this ( add_le_add_left ( le_trans ( by gcongr ) hK.le ) _ ); + refine le_trans this ( add_le_add_right ( le_trans ( by gcongr ) hK.le ) _ ); · simp_all only [gt_iff_lt, ge_iff_le] obtain ⟨left, right⟩ := hM have := Nat.findGreatest_eq_iff.mp ( by aesop : Nat.findGreatest ( fun k => M k ≤ n ) n = Nat.findGreatest ( fun k => M k ≤ n ) n ) @@ -353,7 +361,7 @@ lemma limsup_le_of_block_sequence_bound {α : Type*} (y : ℝ≥0) (f : α → exact Set.finite_iff_bddAbove.2 ⟨ b, fun n hn => le_trans ( hT.id_le _ ) hn ⟩; exact ⟨ Finset.max' ( h_finite.toFinset ) ⟨ K, h_finite.mem_toFinset.mpr a ⟩, h_finite.mem_toFinset.mp ( Finset.max'_mem _ _ ), not_le.mp fun h => not_lt_of_ge ( Finset.le_max' _ _ ( h_finite.mem_toFinset.mpr h ) ) ( Nat.lt_succ_self _ ) ⟩; rw [ hg k b hk.1 hk.2 ]; - exact le_trans ( hbound k b hk.1 hk.2 ) ( add_le_add_left ( hK k ( le_of_not_gt fun hk' => by linarith [ hT.monotone hk'.nat_succ_le ] ) ) _ ) + exact le_trans ( hbound k b hk.1 hk.2 ) ( add_le_add_right ( hK k ( le_of_not_gt fun hk' => by linarith [ hT.monotone hk'.nat_succ_le ] ) ) _ ) /- Version of `exists_liminf_zero_of_forall_liminf_le_with_UB` that lets you stipulate it for two different functions simultaneously, one with liminf and one with limsup. -/ diff --git a/QuantumInfo/ForMathlib/LinearEquiv.lean b/QuantumInfo/ForMathlib/LinearEquiv.lean index 0ccb653..ab0fbde 100644 --- a/QuantumInfo/ForMathlib/LinearEquiv.lean +++ b/QuantumInfo/ForMathlib/LinearEquiv.lean @@ -17,10 +17,12 @@ def of_relabel (e : d ≃ d₂) : (d₂ → R) ≃ₗ[R] (d → R) := by refine' { e.symm.piCongrLeft (fun _ ↦ R) with .. } <;> (intros; ext; simp [Equiv.piCongrLeft_apply]) +variable (e : d ≃ d₂) + variable (𝕜) in @[simps!] def euclidean_of_relabel (e : d ≃ d₂) : EuclideanSpace 𝕜 d₂ ≃ₗ[𝕜] EuclideanSpace 𝕜 d := - of_relabel 𝕜 e + (WithLp.linearEquiv 2 𝕜 _).trans ((of_relabel _ e).trans (WithLp.linearEquiv 2 𝕜 _).symm) @[simp] theorem of_relabel_refl : of_relabel R (.refl d) = LinearEquiv.refl R (d → R) := by @@ -47,8 +49,9 @@ theorem reindex_toLin' (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d theorem reindex_toEuclideanLin (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ 𝕜) : (M.reindex e f).toEuclideanLin = (LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ₗ - M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 f) := - reindex_toLin' e f M + M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 f) := by + ext + simp [mulVec, dotProduct, Equiv.piCongrLeft_apply] theorem reindex_right_toLin' (e : d ≃ d₂) (M : Matrix d₃ d R) : (M.reindex (.refl d₃) e).toLin' = M.toLin' ∘ₗ (LinearEquiv.of_relabel R e) := by @@ -57,8 +60,9 @@ theorem reindex_right_toLin' (e : d ≃ d₂) (M : Matrix d₃ d R) : theorem reindex_right_toEuclideanLin (e : d ≃ d₂) (M : Matrix d₃ d 𝕜) : (M.reindex (.refl d₃) e).toEuclideanLin = - M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 e) := - reindex_right_toLin' e M + M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 e) := by + ext + simp [mulVec, dotProduct, Equiv.piCongrLeft_apply] theorem reindex_left_toLin' (e : d₁ ≃ d₃) (M : Matrix d₁ d₂ R) : (M.reindex e (.refl d₂)).toLin' = (LinearEquiv.of_relabel R e.symm) ∘ M.toLin' := by diff --git a/QuantumInfo/ForMathlib/Matrix.lean b/QuantumInfo/ForMathlib/Matrix.lean index 738cd32..9073750 100644 --- a/QuantumInfo/ForMathlib/Matrix.lean +++ b/QuantumInfo/ForMathlib/Matrix.lean @@ -79,6 +79,7 @@ section eigenvalues /-- The sum of the eigenvalues of a Hermitian matrix is equal to its trace. -/ theorem sum_eigenvalues_eq_trace : ∑ i, hA.eigenvalues i = A.trace := by nth_rewrite 2 [hA.spectral_theorem] + simp only [Unitary.conjStarAlgAut_apply] rw [trace_mul_comm, ← mul_assoc] simp [trace_diagonal] @@ -125,11 +126,6 @@ section variable {A : Matrix m m 𝕜} {B : Matrix m m 𝕜} variable (hA : A.PosSemidef) (hB : B.PosSemidef) -include hA in -theorem diag_nonneg : ∀i, 0 ≤ A.diag i := by - intro i - classical simpa [mulVec, dotProduct] using hA.2 (fun j ↦ if i = j then 1 else 0) - include hA in theorem trace_zero : A.trace = 0 → A = 0 := by open Classical in @@ -151,6 +147,17 @@ theorem _root_.RCLike.normSq_eq_conj_mul_self {z : 𝕜} : RCLike.normSq z = con simp [RCLike.normSq] ring_nf +--PR +theorem Finsupp.sum_eq_ite + {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [Fintype α] + [DecidableEq M] (f : α →₀ M) (g : α → M → N) : + f.sum g = ∑ i, if f i ≠ 0 then g i (f i) else 0 := by + rw [Finsupp.sum, eq_comm] + classical convert Finset.sum_ite_mem Finset.univ f.support (fun i ↦ g i (f i)) + · simp + · simp + + omit dn in open ComplexConjugate in theorem outer_self_conj (v : n → 𝕜) : PosSemidef (vecMulVec v (conj v)) := by @@ -158,7 +165,11 @@ theorem outer_self_conj (v : n → 𝕜) : PosSemidef (vecMulVec v (conj v)) := · ext simp [vecMulVec_apply, mul_comm] · intro x - simp_rw [dotProduct, Pi.star_apply, RCLike.star_def, mulVec, dotProduct, + rw [Finsupp.sum_fintype _ _ (by simp)] + conv => + enter [2, 2, i] + rw [Finsupp.sum_fintype _ _ (by simp)] + simp_rw [RCLike.star_def, vecMulVec_apply, mul_assoc, ← Finset.mul_sum, ← mul_assoc, ← Finset.sum_mul] change 0 ≤ (∑ i : n, conj (x i) * v i) * ∑ i : n, conj (v i) * x i @@ -169,6 +180,7 @@ theorem outer_self_conj (v : n → 𝕜) : PosSemidef (vecMulVec v (conj v)) := rw [this, ← map_sum, ← RCLike.normSq_eq_conj_mul_self, RCLike.ofReal_nonneg] exact RCLike.normSq_nonneg _ +omit [Fintype m] in include hA hB in theorem convex_cone {c₁ c₂ : 𝕜} (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) : (c₁ • A + c₂ • B).PosSemidef := (hA.smul hc₁).add (hB.smul hc₂) @@ -200,11 +212,14 @@ theorem stdBasisMatrix_iff_eq (i j : m) {c : 𝕜} (hc : 0 < c) : (single i j c) · exact RCLike.conj_eq_iff_im.mpr (RCLike.pos_iff.1 hc).2 · exact RingHom.map_zero (starRingEnd 𝕜) · intro x - simp only [dotProduct, single, of_apply, mulVec] - convert_to 0 ≤ (star x i) * c * (x i) - · simp only [Finset.mul_sum] - rw [←Fintype.sum_prod_type'] - have h₀ : ∀ x_1 : m × m, x_1 ≠ ⟨i, i⟩ → star x x_1.1 * ((if i = x_1.1 ∧ i = x_1.2 then c else 0) * x x_1.2) = 0 := fun z hz => by + rw [Finsupp.sum_fintype _ _ (by simp)] + conv => + enter [2, 2, i] + rw [Finsupp.sum_fintype _ _ (by simp)] + simp only [single, of_apply] + convert_to 0 ≤ (star (x i)) * c * (x i) + · rw [←Fintype.sum_prod_type'] + have h₀ : ∀ x_1 : m × m, x_1 ≠ ⟨i, i⟩ → star (x x_1.1) * ((if i = x_1.1 ∧ i = x_1.2 then c else 0) * x x_1.2) = 0 := fun z hz => by have h₁ : ¬(i = z.1 ∧ i = z.2) := by rw [ne_eq, Prod.mk_inj] at hz by_contra hz' @@ -212,10 +227,11 @@ theorem stdBasisMatrix_iff_eq (i j : m) {c : 𝕜} (hc : 0 < c) : (single i j c) exact ⟨hz'.left.symm, hz'.right.symm⟩ rw [ite_cond_eq_false _ _ (eq_false h₁)] ring - rw [Fintype.sum_eq_single ⟨i, i⟩ h₀] - simp [mul_assoc] + rw [Fintype.sum_eq_single ⟨i, i⟩] + · simp [mul_assoc] + · simpa [mul_assoc] using h₀ · rw [mul_comm, ←mul_assoc] - have hpos : 0 ≤ x i * star x i := by simp only [Pi.star_apply, RCLike.star_def, + have hpos : 0 ≤ (x i) * star (x i) := by simp only [RCLike.star_def, RCLike.mul_conj, RCLike.ofReal_nonneg, norm_nonneg, pow_nonneg] exact (mul_nonneg hpos (le_of_lt hc)) @@ -228,6 +244,7 @@ include hA hB in theorem PosSemidef_kronecker : (A ⊗ₖ B).PosSemidef := by open Classical in rw [hA.left.spectral_theorem, hB.left.spectral_theorem] + simp only [Unitary.conjStarAlgAut_apply] rw [mul_kronecker_mul, mul_kronecker_mul] rw [star_eq_conjTranspose, star_eq_conjTranspose] rw [← kroneckerMap_conjTranspose] @@ -258,36 +275,20 @@ theorem zero_dotProduct_zero_iff : (∀ x : m → 𝕜, 0 = star x ⬝ᵥ A.mulV · rintro rfl simp -theorem nonneg_smul {c : 𝕜} (hA : A.PosSemidef) (hc : 0 ≤ c) : (c • A).PosSemidef := by - constructor - · simp only [IsHermitian, conjTranspose_smul, RCLike.star_def] - congr - exact RCLike.conj_eq_iff_im.mpr (RCLike.nonneg_iff.mp hc).2 - exact hA.1 - · intro x - rw [smul_mulVec, dotProduct_smul, smul_eq_mul] - exact Left.mul_nonneg hc (hA.2 x) - +omit [Fintype m] in theorem pos_smul {c : 𝕜} (hA : (c • A).PosSemidef) (hc : 0 < c) : A.PosSemidef := by have : 0 < 1/c := by rw [RCLike.pos_iff] at hc ⊢ aesop - convert hA.nonneg_smul (c := 1/c) this.le + convert hA.smul (a := 1/c) this.le rw [smul_smul, one_div, inv_mul_cancel₀ hc.ne', one_smul] -theorem nonneg_smul_Real_smul {c : ℝ} (hA : A.PosSemidef) (hc : 0 ≤ c) : (c • A).PosSemidef := by - rw [(RCLike.real_smul_eq_coe_smul c A : c • A = (c : 𝕜) • A)] - exact nonneg_smul hA (RCLike.ofReal_nonneg.mpr hc) - -theorem pos_Real_smul {c : ℝ} (hA : (c • A).PosSemidef) (hc : 0 < c) : A.PosSemidef := by - rw [(RCLike.real_smul_eq_coe_smul c A : c • A = (c : 𝕜) • A)] at hA - exact pos_smul hA (RCLike.ofReal_pos.mpr hc) - theorem zero_posSemidef_neg_posSemidef_iff : A.PosSemidef ∧ (-A).PosSemidef ↔ A = 0 := by constructor · intro ⟨hA, hNegA⟩ have h0 : ∀ x : m → 𝕜, 0 = star x ⬝ᵥ A.mulVec x := fun x ↦ by - have hNegA' := hNegA.right x + simp only [Matrix.posSemidef_iff_dotProduct_mulVec] at hA hNegA + have hNegA' := hNegA.right (Finsupp.ofSupportFinite x (Function.support x).toFinite) rw [neg_mulVec, dotProduct_neg, le_neg, neg_zero] at hNegA' exact le_antisymm (hA.right x) hNegA' exact (zero_dotProduct_zero_iff hA).mp h0 @@ -306,7 +307,8 @@ variable {A : Matrix n n 𝕜} theorem toLin_ker_eq_bot (hA : A.PosDef) : LinearMap.ker A.toLin' = ⊥ := by ext v - have := hA.right v + rw [Matrix.posDef_iff_dotProduct_mulVec] at hA + have := @hA.right v grind [mulVec_zero, dotProduct_zero, LinearMap.mem_ker, toLin'_apply, Submodule.mem_bot] theorem of_toLin_ker_eq_bot (hA : LinearMap.ker A.toLin' = ⊥) (hA₂ : A.PosSemidef) : A.PosDef := by @@ -333,20 +335,7 @@ variable [Fintype n] [Fintype m] [RCLike 𝕜] [DecidableEq m] variable {A : Matrix n n 𝕜} {B : Matrix n n 𝕜} variable (hA : A.IsHermitian) (hB : B.IsHermitian) -instance instOrderedCancelAddCommMonoid : IsOrderedCancelAddMonoid (Matrix n n 𝕜) where - add_le_add_left A B hAB C := by - rw [Matrix.le_iff] - rwa [add_sub_add_left_eq_sub] - le_of_add_le_add_left A B C hABAC:= by - rw [Matrix.le_iff] at hABAC - rwa [add_sub_add_left_eq_sub] at hABAC - -/-- Basically, the instance states A ≤ B ↔ B = A + Sᴴ * S -/ -instance instStarOrderedRing : StarOrderedRing (Matrix n n 𝕜) := - StarOrderedRing.of_nonneg_iff' - (add_le_add_left) - (fun _ ↦ by classical apply CStarAlgebra.nonneg_iff_eq_star_mul_self) - +omit [Fintype n] in theorem le_of_nonneg_imp {R : Type*} [AddCommGroup R] [PartialOrder R] [IsOrderedAddMonoid R] (f : Matrix n n 𝕜 →+ R) (h : ∀ A, A.PosSemidef → 0 ≤ f A) : (A ≤ B → f A ≤ f B) := by @@ -354,6 +343,7 @@ theorem le_of_nonneg_imp {R : Type*} [AddCommGroup R] [PartialOrder R] [IsOrdere rw [←sub_nonneg, ←map_sub] exact h (B - A) <| by rwa [← Matrix.le_iff] +omit [Fintype n] in theorem le_of_nonneg_imp' {R : Type*} [AddCommGroup R] [PartialOrder R] [IsOrderedAddMonoid R] {x y : R} (f : R →+ Matrix n n 𝕜) (h : ∀ x, 0 ≤ x → (f x).PosSemidef) : (x ≤ y → f x ≤ f y) := by @@ -382,9 +372,11 @@ theorem conjTranspose_mul_mul_mono (C : Matrix n m 𝕜) : theorem nonneg_iff_eigenvalue_nonneg [DecidableEq n] : 0 ≤ A ↔ ∀ x, 0 ≤ hA.eigenvalues x := Iff.trans Matrix.nonneg_iff_posSemidef hA.posSemidef_iff_eigenvalues_nonneg +omit [Fintype n] in theorem diag_monotone : Monotone (diag : Matrix n n 𝕜 → (n → 𝕜)) := fun _ _ ↦ le_of_nonneg_imp (diagAddMonoidHom n 𝕜) (fun _ ↦ diag_nonneg) +omit [Fintype n] in theorem diag_mono : A ≤ B → ∀ i, A.diag i ≤ B.diag i := diag_monotone.imp theorem trace_monotone : Monotone (@trace n 𝕜 _ _) := fun _ _ ↦ @@ -394,11 +386,14 @@ theorem trace_mono : A ≤ B → A.trace ≤ B.trace := trace_monotone.imp variable [DecidableEq n] +omit [Fintype n] in theorem diagonal_monotone : Monotone (diagonal : (n → 𝕜) → _) := fun _ _ ↦ le_of_nonneg_imp' (diagonalAddMonoidHom n 𝕜) (fun _ ↦ PosSemidef.diagonal) +omit [Fintype n] in theorem diagonal_mono {d₁ d₂ : n → 𝕜} : d₁ ≤ d₂ → diagonal d₁ ≤ diagonal d₂ := diagonal_monotone.imp +omit [Fintype n] in theorem diagonal_le_iff {d₁ d₂ : n → 𝕜} : d₁ ≤ d₂ ↔ diagonal d₁ ≤ diagonal d₂ := ⟨diagonal_mono, by intro hd rw [Matrix.le_iff, diagonal_sub, posSemidef_diagonal_iff] at hd @@ -410,7 +405,7 @@ theorem le_smul_one_of_eigenvalues_iff (hA : A.IsHermitian) (c : ℝ) : let U : Matrix n n 𝕜 := ↑hA.eigenvectorUnitary have hU : U.conjTranspose = star U := by simp only [star] have hU' : U * star U = 1 := by - simp only [SetLike.coe_mem, unitary.mul_star_self_of_mem, U] + simp only [SetLike.coe_mem, Unitary.mul_star_self_of_mem, U] have hc : c • (1 : Matrix n n 𝕜) = U * (c • 1) * U.conjTranspose := by simp only [Algebra.mul_smul_comm, mul_one, hU, Algebra.smul_mul_assoc, hU'] have hc' : c • (1 : Matrix n n 𝕜) = diagonal (RCLike.ofReal ∘ fun _ : n ↦ c) := by @@ -430,12 +425,13 @@ theorem le_smul_one_of_eigenvalues_iff (hA : A.IsHermitian) (c : ℝ) : intro hAc i replace hAc := conjTranspose_mul_mul_mono U hAc have hU'CT : star U * U = 1 := by - simp only [SetLike.coe_mem, unitary.star_mul_self_of_mem, U] + simp only [SetLike.coe_mem, Unitary.star_mul_self_of_mem, U] have hcCT : U.conjTranspose * (c • 1) * U = c • (1 : Matrix n n 𝕜) := by simp only [Algebra.mul_smul_comm, mul_one, hU, Algebra.smul_mul_assoc, hU'CT] have hASTCT : U.conjTranspose * A * U = diagonal (RCLike.ofReal ∘ hA.eigenvalues) := by rw [hU] - exact IsHermitian.star_mul_self_mul_eq_diagonal hA + convert IsHermitian.conjStarAlgAut_star_eigenvectorUnitary hA using 1 + simp +zetaDelta rw [hcCT, hc', hASTCT, ←diagonal_le_iff] at hAc specialize hAc i simp only [Function.comp_apply, algebraMap_le_algebraMap] at hAc @@ -447,7 +443,7 @@ theorem smul_one_le_of_eigenvalues_iff (hA : A.IsHermitian) (c : ℝ) : let U : Matrix n n 𝕜 := ↑hA.eigenvectorUnitary have hU : U.conjTranspose = star U := by simp only [star] have hU' : U * star U = 1 := by - simp only [SetLike.coe_mem, unitary.mul_star_self_of_mem, U] + simp only [SetLike.coe_mem, Unitary.mul_star_self_of_mem, U] have hc : c • (1 : Matrix n n 𝕜) = U * (c • 1) * U.conjTranspose := by simp only [Algebra.mul_smul_comm, mul_one, hU, Algebra.smul_mul_assoc, hU'] have hc' : c • (1 : Matrix n n 𝕜) = diagonal (RCLike.ofReal ∘ fun _ : n ↦ c) := by @@ -467,12 +463,13 @@ theorem smul_one_le_of_eigenvalues_iff (hA : A.IsHermitian) (c : ℝ) : intro hAc i replace hAc := conjTranspose_mul_mul_mono U hAc have hU'CT : star U * U = 1 := by - simp only [SetLike.coe_mem, unitary.star_mul_self_of_mem, U] + simp only [SetLike.coe_mem, Unitary.star_mul_self_of_mem, U] have hcCT : U.conjTranspose * (c • 1) * U = c • (1 : Matrix n n 𝕜) := by simp only [Algebra.mul_smul_comm, mul_one, hU, Algebra.smul_mul_assoc, hU'CT] have hASTCT : U.conjTranspose * A * U = diagonal (RCLike.ofReal ∘ hA.eigenvalues) := by rw [hU] - exact IsHermitian.star_mul_self_mul_eq_diagonal hA + convert IsHermitian.conjStarAlgAut_star_eigenvectorUnitary hA using 1 + simp +zetaDelta rw [hcCT, hc', hASTCT, ←diagonal_le_iff] at hAc specialize hAc i simp only [Function.comp_apply, algebraMap_le_algebraMap] at hAc @@ -644,6 +641,7 @@ variable {d₁ d₂ : Type*} {A : Matrix (d₁ × d₂) (d₁ × d₂) 𝕜} variable [Fintype d₂] [Fintype d₁] theorem PosSemidef.traceLeft [DecidableEq d₁] (hA : A.PosSemidef) : A.traceLeft.PosSemidef := by + rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hA ⊢ constructor · exact hA.1.traceLeft · intro x @@ -653,6 +651,7 @@ theorem PosSemidef.traceLeft [DecidableEq d₁] (hA : A.PosSemidef) : A.traceLef apply_ite] using Finset.sum_comm_cycle theorem PosSemidef.traceRight [DecidableEq d₂] (hA : A.PosSemidef) : A.traceRight.PosSemidef := by + rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hA ⊢ constructor · exact hA.1.traceRight · intro x @@ -671,6 +670,7 @@ open Kronecker theorem PosDef.kron {d₁ d₂ 𝕜 : Type*} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {A : Matrix d₁ d₁ 𝕜} {B : Matrix d₂ d₂ 𝕜} (hA : A.PosDef) (hB : B.PosDef) : (A ⊗ₖ B).PosDef := by rw [hA.left.spectral_theorem, hB.left.spectral_theorem] + simp only [Unitary.conjStarAlgAut_apply] rw [mul_kronecker_mul, mul_kronecker_mul] rw [star_eq_conjTranspose, star_eq_conjTranspose] rw [← kroneckerMap_conjTranspose] @@ -688,6 +688,7 @@ theorem PosDef.kron {d₁ d₂ 𝕜 : Type*} [Fintype d₁] [DecidableEq d₁] [ theorem PosDef.submatrix {d₁ d₂ 𝕜 : Type*} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂] [RCLike 𝕜] {M : Matrix d₁ d₁ 𝕜} (hM : M.PosDef) {e : d₂ → d₁} (he : Function.Injective e) : (M.submatrix e e).PosDef := by + rw [Matrix.posDef_iff_dotProduct_mulVec] at hM ⊢ use hM.left.submatrix e intro x hx let y : d₁ → 𝕜 := fun i ↦ ∑ j ∈ { j | e j = i}, x j @@ -696,7 +697,7 @@ theorem PosDef.submatrix {d₁ d₂ 𝕜 : Type*} [Fintype d₁] [DecidableEq d simp only [funext_iff] at hx ⊢ intro i simpa [y, he.eq_iff, Finset.sum_eq_single_of_mem] using hx (e i) - convert hM.right y hy + convert @hM.right y hy dsimp [Matrix.mulVec, dotProduct, y] simp only [map_sum] simp only [Finset.sum_mul, Finset.sum_filter, Finset.mul_sum] @@ -715,6 +716,7 @@ theorem PosDef.reindex_iff {d₁ d₂ 𝕜 : Type*} [Fintype d₁] [DecidableEq theorem PosSemidef.rsmul {n : Type*} [Fintype n] {M : Matrix n n ℂ} (hM : M.PosSemidef) {c : ℝ} (hc : 0 ≤ c) : (c • M).PosSemidef := by + rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hM ⊢ constructor · exact hM.1.smul_real c · peel hM.2 @@ -743,54 +745,6 @@ theorem PosDef_iff_eigenvalues' (M : Matrix d d 𝕜) : ⟨fun h ↦ ⟨h.left, h.left.posDef_iff_eigenvalues_pos.mp h⟩, fun ⟨w, h⟩ ↦ w.posDef_iff_eigenvalues_pos.mpr h⟩ ---PR'ed: #27118 -theorem IsHermitian.charpoly_roots_eq_eigenvalues {M : Matrix d d 𝕜} (hM : M.IsHermitian) : - M.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hM.eigenvalues) Finset.univ.val := by - -- Since M is Hermitian, its characteristic polynomial splits into linear factors over the reals. - have h_split : M.charpoly = Multiset.prod (Multiset.map (fun (e : ℝ) => Polynomial.X - Polynomial.C (RCLike.ofReal e)) (Multiset.map (fun (i : d) => hM.eigenvalues i) Finset.univ.val)) := by - -- Since M is Hermitian, it is diagonalizable, and its characteristic polynomial splits into linear factors over the reals. - have h_diag : ∃ P : Matrix d d 𝕜, P.det ≠ 0 ∧ ∃ D : Matrix d d 𝕜, D = Matrix.diagonal (fun i => RCLike.ofReal (hM.eigenvalues i)) ∧ M = P * D * P⁻¹ := by - have := hM.spectral_theorem; - refine' ⟨ hM.eigenvectorUnitary, _, _ ⟩ - · -- Since the eigenvector unitary is a unitary matrix, its determinant is a unit, hence non-zero. - have h_det_unitary : IsUnit (Matrix.det (hM.eigenvectorUnitary : Matrix d d 𝕜)) := by - exact UnitaryGroup.det_isUnit hM.eigenvectorUnitary - exact h_det_unitary.ne_zero - · refine' ⟨ _, rfl, this.trans _ ⟩ - rw [ Matrix.inv_eq_left_inv ] - congr! - bound - -- Since M is similar to D, their characteristic polynomials are the same. - have h_char_poly : M.charpoly = Matrix.charpoly (Matrix.diagonal (fun i => RCLike.ofReal (hM.eigenvalues i))) := by - rcases h_diag with ⟨P, left, ⟨D, left_1, rfl⟩⟩ - rw [ ← left_1, Matrix.charpoly, Matrix.charpoly ]; - simp +decide [ Matrix.charmatrix, Matrix.mul_assoc ]; - -- Since $w$ is invertible, we can simplify the determinant. - have h_inv : (P.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)) * (P⁻¹.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)) = 1 := by - simp [ ← Matrix.map_mul, left ]; - -- Since $w$ is invertible, we can simplify the determinant using the fact that the determinant of a product is the product of the determinants. - have h_det_prod : Matrix.det ((Matrix.diagonal (fun _ => Polynomial.X) - P.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜) * (D.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜) * P⁻¹.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)))) = Matrix.det ((P.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)) * (Matrix.diagonal (fun _ => Polynomial.X) - D.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)) * (P⁻¹.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜))) := by - simp only [ mul_sub, sub_mul, Matrix.mul_assoc ]; - -- Since Matrix.diagonal (fun _ => Polynomial.X) is a scalar matrix, it commutes with any matrix. - have h_comm : Matrix.diagonal (fun _ => Polynomial.X) * P⁻¹.map Polynomial.C = P⁻¹.map Polynomial.C * Matrix.diagonal (fun _ => Polynomial.X) := by - ext i j; by_cases hi : i = j <;> simp [ hi ]; - simp only [ h_comm ]; - simp [ ← mul_assoc, h_inv ]; - rw [ h_det_prod, Matrix.det_mul, Matrix.det_mul ]; - -- Since the determinant of the product of two matrices is the product of their determinants, and the determinant of the identity matrix is 1, we have: - have h_det_identity : Matrix.det (P.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)) * Matrix.det (P⁻¹.map (⇑Polynomial.C : 𝕜 → Polynomial 𝕜)) = 1 := by - rw [ ← Matrix.det_mul, h_inv, Matrix.det_one ]; - rw [ mul_right_comm, h_det_identity, one_mul ]; - rw [h_char_poly]; - simp [ Matrix.charpoly, Matrix.det_diagonal ]; - rw [ h_split, Polynomial.roots_multiset_prod ]; - -- Case 1 - · erw [ Multiset.bind_map ]; - aesop; - -- Case 2 - · -- Since the eigenvalues are real, and we're working over the complex numbers (since 𝕜 is a real closed field), the polynomial X - C(e) would be zero only if e is zero. But if e is zero, then the polynomial would be X, which isn't zero. So 0 can't be in the multiset. - simp [Polynomial.X_sub_C_ne_zero] - --These is disgusting atm. There's cleaner versions of them headed to Mathlib. See #29526 and follow-ups theorem IsHermitian.cfc_eigenvalues {M : Matrix d d 𝕜} (hM : M.IsHermitian) (f : ℝ → ℝ) : ∃ (e : d ≃ d), Matrix.IsHermitian.eigenvalues (cfc_predicate f M) = f ∘ hM.eigenvalues ∘ e := by @@ -823,7 +777,7 @@ theorem IsHermitian.cfc_eigenvalues {M : Matrix d d 𝕜} (hM : M.IsHermitian) ( rw [ Polynomial.roots_prod ]; · bound; · exact Finset.prod_ne_zero_iff.mpr fun i _ => Polynomial.X_sub_C_ne_zero _; - have := IsHermitian.charpoly_roots_eq_eigenvalues (cfc_predicate f M); + have := Matrix.IsHermitian.roots_charpoly_eq_eigenvalues (cfc_predicate f M); rw [← Matrix.IsHermitian.cfc_eq] at h_eigenvalues_cfc rw [ h_eigenvalues_cfc ] at this; simp [ Function.comp ] at this; @@ -854,10 +808,10 @@ lemma IsHermitian.eigenvalues_eq_of_unitary_similarity_diagonal {d 𝕜 : Type*} intro t have h_det : Matrix.det (t • 1 - U * Matrix.diagonal (fun i => (f i : 𝕜)) * Uᴴ) = Matrix.det (U * (t • 1 - Matrix.diagonal (fun i => (f i : 𝕜))) * Uᴴ) := by simp [ mul_sub, sub_mul, Matrix.mul_assoc ]; - rw [ show U * Uᴴ = 1 from by simpa [ Matrix.mul_eq_one_comm ] using hU.2 ]; - have := congr_arg Matrix.det hU.2; norm_num at this; simp_all [ mul_assoc, mul_comm ] ; - simp_all [ ← mul_assoc ]; - simp_all [ Star.star ] + rw [ show U * Uᴴ = 1 from by simpa [mul_eq_one_comm] using hU.2 ]; + rw [h_det, Matrix.det_mul_comm, ← mul_assoc] + rw [← star_eq_conjTranspose, Matrix.UnitaryGroup.star_mul_self ⟨U, hU⟩] + simp refine' Polynomial.funext fun t => _; convert h_det t using 1 <;> simp [ Matrix.charpoly, Matrix.det_apply' ]; · simp [ Polynomial.eval_finset_sum, Polynomial.eval_mul, Polynomial.eval_prod, Matrix.one_apply ]; @@ -925,7 +879,7 @@ theorem cfc_diagonal (g : d → ℝ) (f : ℝ → ℝ) : · simp [← ext_iff, diagonal] exact fun r i j ↦ rfl · simp [← ext_iff, diagonal] - grind [RCLike.conj_ofReal, map_zero] + grind [RCLike.conj_ofReal] · dsimp [diagonal] continuity · simp [diagonal] @@ -998,7 +952,8 @@ private lemma spectrum_prod_complex {d d₂ : Type*} simp -- Substitute h_unitary into the equation. rw [h_unitary]; - exact Matrix.IsHermitian.star_mul_self_mul_eq_diagonal hA + convert Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary hA using 1 + simp obtain ⟨Q, hQ₁, ⟨E, hE⟩⟩ : ∃ Q : Matrix d₂ d₂ 𝕜, Q.det ≠ 0 ∧ ∃ E : Matrix d₂ d₂ 𝕜, E.IsDiag ∧ Q⁻¹ * B * Q = E := by have := Matrix.IsHermitian.spectral_theorem hB; -- By the spectral theorem, since B is Hermitian, there exists a unitary matrix Q and a diagonal matrix D such that B = Q * D * Q⁻¹. @@ -1012,7 +967,9 @@ private lemma spectrum_prod_complex {d d₂ : Type*} · exact isDiag_diagonal (RCLike.ofReal ∘ hB.eigenvalues); · convert this using 1; rw [ Matrix.inv_eq_left_inv ]; - simp + · simp + rfl + · simp only [SetLike.coe_mem, Unitary.star_mul_self_of_mem] refine ⟨ Q, hQ_unitary, D, hD_diag, ?_ ⟩ simp [ hQ, mul_assoc, hQ_unitary, isUnit_iff_ne_zero ]; -- Then $(P \otimes Q)^{-1}(A \otimes B)(P \otimes Q) = D \otimes E$, where $D$ and $E$ are diagonal matrices. @@ -1223,6 +1180,7 @@ open ComplexOrder lemma sub_iInf_eignevalues (hA : A.IsHermitian) : (A - iInf hA.eigenvalues • 1).PosSemidef := by + rw [Matrix.posSemidef_iff_dotProduct_mulVec] constructor · simpa [ Matrix.IsHermitian, sub_eq_add_neg ] using hA · intro x @@ -1251,9 +1209,9 @@ lemma sub_iInf_eignevalues (hA : A.IsHermitian) : -- Since $Q$ is unitary, we have $Q^* (A - \lambda_{\min} I) Q = \Lambda - \lambda_{\min} I$, and thus $x^* (A - \lambda_{\min} I) x = (Q^* x)^* (\Lambda - \lambda_{\min} I) (Q^* x)$. have h_quad_form : Star.star x ⬝ᵥ (A - (iInf (Matrix.IsHermitian.eigenvalues hA)) • 1).mulVec x = Star.star (Q.conjTranspose.mulVec x) ⬝ᵥ (Matrix.diagonal (fun i => Λ i - (iInf (Matrix.IsHermitian.eigenvalues hA)))).mulVec (Q.conjTranspose.mulVec x) := by rw [ ← h_diag ]; - simp [ Matrix.mul_assoc, Matrix.dotProduct_mulVec, Matrix.mul_eq_one_comm.mp hQ]; + simp [ Matrix.mul_assoc, Matrix.dotProduct_mulVec, mul_eq_one_comm.mp hQ]; simp only [mulVec_conjTranspose, star_star, vecMul_vecMul]; - rw [ ← Matrix.mul_assoc, Matrix.mul_eq_one_comm.mp hQ, one_mul ]; + rw [ ← Matrix.mul_assoc, mul_eq_one_comm.mp hQ, one_mul ]; simp_all only [ge_iff_le, dotProduct, Pi.star_apply, RCLike.star_def, mulVec, sub_apply, smul_apply, Complex.real_smul, conjTranspose_apply, star_sum, star_mul', RingHomCompTriple.comp_apply, RingHom.id_apply]; @@ -1282,7 +1240,9 @@ lemma iInf_eigenvalues_le_dotProduct_mulVec (hA : A.IsHermitian) (v : d → ℂ) simp only [dotProduct, Pi.star_apply, RCLike.star_def, mul_comm, mulVec] simp [Matrix.one_apply, mul_assoc, mul_left_comm, Finset.mul_sum] rw [← sub_nonneg, ← dotProduct_sub, ← Matrix.sub_mulVec] - exact (sub_iInf_eignevalues hA).right v + replace hA := sub_iInf_eignevalues hA + rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hA + exact hA.right v lemma iInf_eigenvalues_le_of_posSemidef (hAB : (B - A).PosSemidef) (hA : A.IsHermitian) (hB : B.IsHermitian) : @@ -1290,7 +1250,7 @@ lemma iInf_eigenvalues_le_of_posSemidef rcases isEmpty_or_nonempty d · simp contrapose! hAB - rw [PosSemidef] + rw [posSemidef_iff_dotProduct_mulVec] push_neg intro _ apply exists_lt_of_ciInf_lt at hAB @@ -1362,9 +1322,12 @@ theorem IsHermitian.spectrum_subset_Ici_of_sub {d 𝕜 : Type*} [Fintype d] [Dec ext i j simp only [RCLike.star_def, Matrix.smul_of, Matrix.sum_apply, Matrix.of_apply, Pi.smul_apply, Matrix.diagonal, Function.comp_apply, Matrix.mul_apply, - Matrix.IsHermitian.eigenvectorUnitary_apply, PiLp.ofLp_apply, mul_ite, mul_zero, - Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, Matrix.star_apply]; + Matrix.IsHermitian.eigenvectorUnitary_apply, mul_ite, mul_zero, + Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, Matrix.star_apply, + Unitary.conjStarAlgAut_apply] simp [ mul_comm, mul_left_comm, Algebra.smul_def ] + congr! 1 + sorry -- Substitute the decomposition of $A$ into the expression $(star v ⬝ᵥ (A.mulVec v))$. have h_subst : (star v ⬝ᵥ (A.mulVec v)) = ∑ i, (hA.eigenvalues i) * (star v ⬝ᵥ (Matrix.mulVec (Matrix.of (fun j k => (hA.eigenvectorBasis i j) * (star (hA.eigenvectorBasis i k)))) v)) := by -- Substitute the decomposition of $A$ into the expression $(star v ⬝ᵥ (A.mulVec v))$ and use the linearity of matrix multiplication. @@ -1412,13 +1375,15 @@ theorem IsHermitian.spectrum_subset_Ici_of_sub {d 𝕜 : Type*} [Fintype d] [Dec -- Since $\sum_{i} (star (hA.eigenvectorBasis i) ⬝ᵥ v) * (star v ⬝ᵥ (hA.eigenvectorBasis i)) = star v ⬝ᵥ v$, we can factor out $(⨅ i, (hA.eigenvalues i))$ from the sum. have h_sum : ∑ i, (star (hA.eigenvectorBasis i) ⬝ᵥ v) * (star v ⬝ᵥ (hA.eigenvectorBasis i)) = star v ⬝ᵥ v := by have h_sum : ∑ i, (star (hA.eigenvectorBasis i) ⬝ᵥ v) • (hA.eigenvectorBasis i) = v := by - have := hA.eigenvectorBasis.sum_repr v; + have := hA.eigenvectorBasis.sum_repr (WithLp.toLp 2 v); convert this using 1; simp only [dotProduct, Pi.star_apply, RCLike.star_def, mul_comm, hA.eigenvectorBasis.repr_apply_apply, PiLp.inner_apply, RCLike.inner_apply]; + simp only [WithLp.ofLp_sum, WithLp.ofLp_smul] + sorry -- Taking the inner product of both sides of h_sum with star v, we get the desired equality. have h_inner : star v ⬝ᵥ (∑ i, (star (hA.eigenvectorBasis i) ⬝ᵥ v) • (hA.eigenvectorBasis i)) = star v ⬝ᵥ v := by - rw [h_sum]; + sorry convert h_inner using 1; simp [ dotProduct, Finset.mul_sum _ _ _ ]; exact Finset.sum_comm.trans ( Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring ); @@ -1426,7 +1391,9 @@ theorem IsHermitian.spectrum_subset_Ici_of_sub {d 𝕜 : Type*} [Fintype d] [Dec refine' le_trans _ ( Finset.sum_le_sum fun i _ => h_bound i ); simp only [ mul_assoc]; rw [ ← Finset.mul_sum _ _ _, h_sum ]; - have := hl.2 v; simp_all [ Matrix.sub_mulVec ] ; + rw [Matrix.posSemidef_iff_dotProduct_mulVec] at hl + have := hl.2 v + simp [Matrix.sub_mulVec] at this exact le_trans h_eigenvalue this; change (⨅ i, hA.eigenvalues i) ≤ μ have := h_lower_bound v hv₁ @@ -1585,7 +1552,8 @@ theorem PosSemidef.piProd [RCLike R] (hA : ∀ i, (A i).PosSemidef) : refine' Finset.sum_bij ( fun p hp => fun i => p i ( Finset.mem_univ i ) ) _ _ _ _ <;> simp +decide; · simp [ funext_iff ]; · exact fun b => ⟨ fun i _ => b i, rfl ⟩; - simp_all [ Matrix.PosSemidef, Matrix.piProd ] + simp only [Matrix.posSemidef_iff_dotProduct_mulVec] at hA ⊢ + simp_all [Matrix.piProd] constructor · ext1 simp [Matrix.mul_apply, mul_comm] diff --git a/QuantumInfo/ForMathlib/Minimax.lean b/QuantumInfo/ForMathlib/Minimax.lean index f1cc0df..6610798 100644 --- a/QuantumInfo/ForMathlib/Minimax.lean +++ b/QuantumInfo/ForMathlib/Minimax.lean @@ -13,8 +13,8 @@ import Mathlib.Topology.Algebra.Module.StrongTopology import Mathlib.Topology.Algebra.Module.FiniteDimension --TODO go elsewhere -attribute [fun_prop] LowerSemicontinuous UpperSemicontinuous -attribute [fun_prop] LowerSemicontinuousOn UpperSemicontinuousOn +attribute [fun_prop] LowerSemicontinuous --UpperSemicontinuous +attribute [fun_prop] LowerSemicontinuousOn --UpperSemicontinuousOn attribute [fun_prop] LowerSemicontinuous.lowerSemicontinuousOn attribute [fun_prop] UpperSemicontinuous.upperSemicontinuousOn attribute [fun_prop] Continuous.lowerSemicontinuous Continuous.upperSemicontinuous @@ -133,10 +133,12 @@ theorem minimax · intro y t --Why doesn't fun_prop find this, even though this theorem is marked fun_prop? TODO apply LowerSemicontinuous.lowerSemicontinuousOn + apply Continuous.lowerSemicontinuous fun_prop · intro y t --Why doesn't fun_prop find this, even though this theorem is marked fun_prop? TODO apply UpperSemicontinuous.upperSemicontinuousOn + apply Continuous.upperSemicontinuous fun_prop · intro y hy exact LinearMap.quasiconvexOn (f := LinearMap.flip { diff --git a/QuantumInfo/ForMathlib/Misc.lean b/QuantumInfo/ForMathlib/Misc.lean index 682be22..c1c5eaa 100644 --- a/QuantumInfo/ForMathlib/Misc.lean +++ b/QuantumInfo/ForMathlib/Misc.lean @@ -14,6 +14,7 @@ theorem ite_eq_top {α : Type*} [Top α] (h : Prop) [Decidable h] {x y : α} (hx split <;> assumption section subtype_val_iSup + /- When https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/diamond.20in.20ConditionallyCompleteLattice/near/538053239 @@ -46,7 +47,7 @@ theorem subtype_val_iSup (h : ∀ i, f i ∈ Set.Icc a b) : theorem subtype_val_iSup' (h : ∀ i, f i ∈ Set.Icc a b) : ⨆ i, (⟨f i, h i⟩ : ↑(Set.Icc a b)) = ⟨⨆ i, f i, ⟨(h i.some).1.trans (le_ciSup ⟨b, by intro; grind⟩ _), ciSup_le (h ·|>.2)⟩⟩ := by - rw [Subtype.eq_iff, subtype_val_iSup] + rw [Subtype.ext_iff, subtype_val_iSup] /- This isn't marked as `simp` because rewriting from a sup over a `CompleteLattice` into a `ConditionallyCompleteLattice` would, pretty often, be undesirable. -/ @@ -59,16 +60,10 @@ theorem subtype_val_iInf (h : ∀ i, f i ∈ Set.Icc a b) : theorem subtype_val_iInf' (h : ∀ i, f i ∈ Set.Icc a b) : ⨅ i, (⟨f i, h i⟩ : ↑(Set.Icc a b)) = ⟨⨅ i, f i, ⟨le_ciInf (h ·|>.1), (ciInf_le ⟨a, by intro; grind⟩ _).trans (h i.some).2⟩⟩ := by - rw [Subtype.eq_iff, subtype_val_iInf] + rw [Subtype.ext_iff, subtype_val_iInf] end subtype_val_iSup ---PR'ed in #33106 -@[simp] -theorem Real.log_comp_exp : log ∘ exp = _root_.id := by - ext - simp - open scoped ENNReal Topology in /-- Analogous to `bdd_le_mul_tendsto_zero`, for `ENNReal` (which otherwise lacks a continuous multiplication function). The product of a sequence that tends to zero with any bounded sequence diff --git a/lake-manifest.json b/lake-manifest.json index 7647138..79a7560 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,71 +1,21 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", + [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "a71fdaa4800d0e0ea990f74aafea3e6c13eec2fb", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", + "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", + "inputRev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "fae4fbc11a6076475940e0d4c43aea77d65d5898", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "29a4b34f8caa7c95934ab4494d8866fde1850c0b", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "44da417da3705ede62b5c39382ddd2261ec3933e", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805", + "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d768126816be17600904726ca7976b185786e6b9", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "556caed0eadb7901e068131d1be208dd907d07a2", + "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.74", + "inputRev": "v0.0.87", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -115,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,11 +75,21 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.28.0", + "inherited": true, "configFile": "lakefile.toml"}], "name": "quantumInfo", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index b51196f..87cfffa 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -3,7 +3,7 @@ open System Lake DSL package «quantumInfo» -require "mathlib" from git "https://github.com/leanprover-community/mathlib4.git" @ "f897ebcf72cd16f89ab4577d0c826cd14afaafc7" +require "mathlib" from git "https://github.com/leanprover-community/mathlib4.git" @ "8f9d9cff6bd728b17a24e163c9402775d9e6a365" --require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" diff --git a/lean-toolchain b/lean-toolchain index 58ae245..ea6ca7f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0 \ No newline at end of file +leanprover/lean4:v4.28.0 \ No newline at end of file