From 6b644aa074ea2f9da2105d09fae6ed5143014c12 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 15 Jun 2025 14:58:02 +0000 Subject: [PATCH 01/86] added lemmas --- Mathlib/LinearAlgebra/Projection.lean | 137 ++++++++++++++++++++++++++ 1 file changed, 137 insertions(+) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 6e97c137d33692..cab936c41c1c66 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -424,6 +424,48 @@ theorem eq_conj_prod_map' {f : E →ₗ[R] E} (h : IsProj p f) : · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero, coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero] +theorem isIdempotentElem {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] + {T : V →ₗ[R] V} {U : Submodule R V} (h : IsProj U T) : + IsIdempotentElem T := +by ext; exact h.2 _ (h.1 _) + +protected theorem range + {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] {T : V →ₗ[R] V} {U : Submodule R V} + (h : IsProj U T) : + range T = U := +by + ext x + refine ⟨fun ⟨y, hy⟩ => ?_, fun hx => ⟨x, h.map_id x hx⟩⟩ + rw [← hy] + exact h.map_mem y + +protected theorem top (S M : Type*) [Semiring S] [AddCommMonoid M] [Module S M] : + IsProj (⊤ : Submodule S M) (id (R := S)) := +⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ + +theorem _root_.LinearMap.subtype_top_comp_codRestrict_top_eq_id + {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] : + (Submodule.subtype ⊤).comp (IsProj.top S M).codRestrict = LinearMap.id := +rfl + +theorem subtype_comp_codRestrict {S M : Type*} [Semiring S] [AddCommMonoid M] + [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : + (Submodule.subtype U).comp hf.codRestrict = f := +rfl + +theorem submodule_eq_top_iff {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] + {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : + U = (⊤ : Submodule S M) ↔ (Submodule.subtype _).comp hf.codRestrict = LinearMap.id := +by + rw [subtype_comp_codRestrict] + constructor <;> rintro rfl + · ext + simp only [id_coe, id_eq, hf.2 _ mem_top] + · refine eq_top_iff'.mpr ?mpr.a + intro x + rw [← id_apply (R := S) x] + exact hf.map_mem x + end IsProj end LinearMap @@ -444,3 +486,98 @@ theorem IsProj.eq_conj_prodMap {f : E →ₗ[R] E} (h : IsProj p f) : end LinearMap end CommRing + +section +variable {R E M : Type*} [Semiring R] [AddCommGroup E] [Module R E] + [AddCommMonoid M] [Module R M] + +open Submodule LinearMap + +/-- Given an idempotent linear operator `p`, we have + `x ∈ range p` if and only if `p(x) = x` for all `x`. -/ +theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : + x ∈ range p ↔ p x = x := by + simp_rw [mem_range] + refine ⟨fun ⟨y, hy⟩ => ?_, fun h => ⟨x, h⟩⟩ + rw [← hy, ← Module.End.mul_apply, hp.eq] + +/-- Given an idempotent linear operator `q`, + we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ +theorem IsIdempotentElem.comp_idempotent_iff + {q : M →ₗ[R] M} (hq : IsIdempotentElem q) + {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : + q.comp p = p ↔ range p ≤ range q := +by + simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, + SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] + +/-- If `p,q` are idempotent operators and `p ∘ q = p = q ∘ p`, + then `q - p` is an idempotent operator. -/ +theorem LinearMap.isIdempotentElem_sub_of + {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) + (hq : IsIdempotentElem q) + (hpq : p.comp q = p) (hqp : q.comp p = p) : + IsIdempotentElem (q - p) := by + simp_rw [IsIdempotentElem, Module.End.mul_eq_comp, sub_comp, comp_sub, hpq, hqp, + ← Module.End.mul_eq_comp, hp.eq, hq.eq, sub_self, sub_zero] + +/-- If `p,q` are idempotent operators and `q - p` is also an idempotent + operator, then `p ∘ q = p = q ∘ p`. -/ +theorem LinearMap.commutes_of_isIdempotentElem_sub + [SMulCommClass R R E] [NoZeroSMulDivisors R E] [NeZero (2 : R)] + {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) + (hqp : IsIdempotentElem (q - p)) : p.comp q = p ∧ q.comp p = p := +by + simp_rw [IsIdempotentElem, Module.End.mul_eq_comp, comp_sub, sub_comp, ← Module.End.mul_eq_comp, + hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp + have h' : ((2 : R) • p : E →ₗ[R] E) = q.comp p + p.comp q := + by + simp_rw [two_smul] + nth_rw 2 [← hqp] + simp_rw [Module.End.mul_eq_comp, add_sub_cancel, add_comm] + have H : ((2 : R) • p).comp q = q.comp (p.comp q) + p.comp q := by + simp_rw [h', add_comp, comp_assoc, ← Module.End.mul_eq_comp, hq.eq] + simp_rw [add_comm, two_smul, add_comp, add_right_inj] at H + have H' : q.comp ((2 : R) • p) = q.comp p + q.comp (p.comp q) := by + simp_rw [h', comp_add, ← comp_assoc, ← Module.End.mul_eq_comp, hq.eq] + simp_rw [two_smul, comp_add, add_right_inj] at H' + have H'' : q.comp p = p.comp q := by + simp_rw [H'] + exact H.symm + rw [← H'', and_self_iff, ← smul_right_inj (two_ne_zero' R), h', ← H'', two_smul] + +/-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, + in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ +theorem IsIdempotentElem.isCompl_range_ker + {T : E →ₗ[R] E} (h : IsIdempotentElem T) : + IsCompl (range T) (ker T) := +by + symm + constructor + · rw [disjoint_iff] + ext x + simp only [mem_bot, mem_inf, mem_ker, mem_range] + constructor + · intro h' + rcases h'.2 with ⟨y, hy⟩ + rw [← hy, ← IsIdempotentElem.eq h, Module.End.mul_apply, hy] + exact h'.1 + · intro h' + rw [h', map_zero] + simp only [true_and] + use x + simp only [h', map_zero, eq_self_iff_true] + · suffices ∀ x : E, ∃ v : ker T, ∃ w : range T, x = v + w + by + rw [codisjoint_iff] + ext x + rcases this x with ⟨v, w, hvw⟩ + simp only [mem_top, iff_true, hvw] + apply add_mem_sup (SetLike.coe_mem v) (SetLike.coe_mem w) + intro x + use ⟨x - T x, ?_⟩, ⟨T x, ?_⟩ + · simp only [Submodule.coe_mk, sub_add_cancel] + · rw [mem_ker, map_sub, ← Module.End.mul_apply, IsIdempotentElem.eq h, sub_self] + · rw [mem_range]; simp only [exists_apply_eq_apply] + +end From ad04c9b5f97bf55840baea82f66a897eac8b5001 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 15 Jun 2025 21:58:31 +0000 Subject: [PATCH 02/86] fixes --- Mathlib/LinearAlgebra/Projection.lean | 55 +++++++++++---------------- 1 file changed, 22 insertions(+), 33 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index cab936c41c1c66..363fdb8b578511 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -497,14 +497,12 @@ open Submodule LinearMap `x ∈ range p` if and only if `p(x) = x` for all `x`. -/ theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : x ∈ range p ↔ p x = x := by - simp_rw [mem_range] refine ⟨fun ⟨y, hy⟩ => ?_, fun h => ⟨x, h⟩⟩ rw [← hy, ← Module.End.mul_apply, hp.eq] /-- Given an idempotent linear operator `q`, we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ -theorem IsIdempotentElem.comp_idempotent_iff - {q : M →ₗ[R] M} (hq : IsIdempotentElem q) +theorem IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : q.comp p = p ↔ range p ≤ range q := by @@ -513,43 +511,39 @@ by /-- If `p,q` are idempotent operators and `p ∘ q = p = q ∘ p`, then `q - p` is an idempotent operator. -/ -theorem LinearMap.isIdempotentElem_sub_of - {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) - (hq : IsIdempotentElem q) - (hpq : p.comp q = p) (hqp : q.comp p = p) : +theorem LinearMap.isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) + (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : IsIdempotentElem (q - p) := by simp_rw [IsIdempotentElem, Module.End.mul_eq_comp, sub_comp, comp_sub, hpq, hqp, ← Module.End.mul_eq_comp, hp.eq, hq.eq, sub_self, sub_zero] /-- If `p,q` are idempotent operators and `q - p` is also an idempotent operator, then `p ∘ q = p = q ∘ p`. -/ -theorem LinearMap.commutes_of_isIdempotentElem_sub - [SMulCommClass R R E] [NoZeroSMulDivisors R E] [NeZero (2 : R)] - {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) - (hqp : IsIdempotentElem (q - p)) : p.comp q = p ∧ q.comp p = p := +theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E →ₗ[R] E} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : + p.comp q = p ∧ q.comp p = p := by simp_rw [IsIdempotentElem, Module.End.mul_eq_comp, comp_sub, sub_comp, ← Module.End.mul_eq_comp, hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp - have h' : ((2 : R) • p : E →ₗ[R] E) = q.comp p + p.comp q := + have h' : ((2 : ℕ) • p : E →ₗ[R] E) = q.comp p + p.comp q := by simp_rw [two_smul] nth_rw 2 [← hqp] simp_rw [Module.End.mul_eq_comp, add_sub_cancel, add_comm] - have H : ((2 : R) • p).comp q = q.comp (p.comp q) + p.comp q := by + have H : ((2 : ℕ) • p).comp q = q.comp (p.comp q) + p.comp q := by simp_rw [h', add_comp, comp_assoc, ← Module.End.mul_eq_comp, hq.eq] simp_rw [add_comm, two_smul, add_comp, add_right_inj] at H - have H' : q.comp ((2 : R) • p) = q.comp p + q.comp (p.comp q) := by + have H' : q.comp ((2 : ℕ) • p) = q.comp p + q.comp (p.comp q) := by simp_rw [h', comp_add, ← comp_assoc, ← Module.End.mul_eq_comp, hq.eq] simp_rw [two_smul, comp_add, add_right_inj] at H' have H'' : q.comp p = p.comp q := by simp_rw [H'] exact H.symm - rw [← H'', and_self_iff, ← smul_right_inj (two_ne_zero' R), h', ← H'', two_smul] + rw [← H'', and_self_iff, ← smul_right_inj (two_ne_zero), h', ← H'', two_smul] /-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ -theorem IsIdempotentElem.isCompl_range_ker - {T : E →ₗ[R] E} (h : IsIdempotentElem T) : +theorem IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : IsCompl (range T) (ker T) := by symm @@ -557,27 +551,22 @@ by · rw [disjoint_iff] ext x simp only [mem_bot, mem_inf, mem_ker, mem_range] - constructor - · intro h' - rcases h'.2 with ⟨y, hy⟩ - rw [← hy, ← IsIdempotentElem.eq h, Module.End.mul_apply, hy] + constructor <;> intro h' + · rcases h'.2 with ⟨y, rfl⟩ + rw [← IsIdempotentElem.eq h, Module.End.mul_apply] exact h'.1 - · intro h' - rw [h', map_zero] - simp only [true_and] + · rw [h', map_zero, eq_self_iff_true, true_and] use x simp only [h', map_zero, eq_self_iff_true] - · suffices ∀ x : E, ∃ v : ker T, ∃ w : range T, x = v + w - by + · suffices ∀ x : E, ∃ v : ker T, ∃ w : range T, x = v + w by rw [codisjoint_iff] ext x - rcases this x with ⟨v, w, hvw⟩ - simp only [mem_top, iff_true, hvw] - apply add_mem_sup (SetLike.coe_mem v) (SetLike.coe_mem w) - intro x - use ⟨x - T x, ?_⟩, ⟨T x, ?_⟩ - · simp only [Submodule.coe_mk, sub_add_cancel] + rcases this x with ⟨v, w, rfl⟩ + simp only [mem_top, iff_true] + exact add_mem_sup (SetLike.coe_mem v) (SetLike.coe_mem w) + refine fun x => ⟨⟨x - T x, ?_⟩, ⟨T x, ?_⟩, ?_⟩ · rw [mem_ker, map_sub, ← Module.End.mul_apply, IsIdempotentElem.eq h, sub_self] - · rw [mem_range]; simp only [exists_apply_eq_apply] + · simp only [mem_range, exists_apply_eq_apply] + · simp only [Submodule.coe_mk, sub_add_cancel] end From c1c066a0a8276633e62f2b42cb3a75c13c65f03b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 16 Jun 2025 15:11:48 +0000 Subject: [PATCH 03/86] generalizing results --- Mathlib/Algebra/Ring/Idempotent.lean | 37 +++++++++++++++++++++++++++ Mathlib/LinearAlgebra/Projection.lean | 25 ++++-------------- 2 files changed, 42 insertions(+), 20 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 2197f748aed0fe..861368d8633a1c 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -7,6 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Idempotent import Mathlib.Algebra.Ring.Defs import Mathlib.Order.Notation import Mathlib.Tactic.Convert +import Mathlib.Algebra.Group.Torsion /-! # Idempotent elements of a ring @@ -76,3 +77,39 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : end CommRing end IsIdempotentElem + +lemma isIdempotentElem_sub_of {H : Type*} [NonAssocRing H] {p q : H} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) + (hpq : p * q = p) (hqp : q * p = p) : + IsIdempotentElem (q - p) := +by simp_rw [IsIdempotentElem, sub_mul, mul_sub, hpq, hqp, hp.eq, hq.eq, sub_self, sub_zero] + +lemma commutes_of_isIdempotentElem_sub + {H : Type*} [Ring H] [IsAddTorsionFree H] {p q : H} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : + p * q = p ∧ q * p = p := +by + simp_rw [IsIdempotentElem, mul_sub, sub_mul, + hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp + have h' : ((2 : ℕ) • p : H) = q * p + p * q := by + simp_rw [two_nsmul] + calc p + p = p + (p * q + q * p - p) := by rw [hqp] + _ = q * p + p * q := by simp_rw [add_sub_cancel, add_comm] + have H : ((2 : ℕ) • p) * q = q * (p * q) + p * q := by + simp_rw [h', add_mul, mul_assoc, hq.eq] + simp_rw [add_comm, two_nsmul, add_mul, add_right_inj] at H + have H' : q * ((2 : ℕ) • p) = q * p + q * (p * q) := by + simp_rw [h', mul_add, ← mul_assoc, hq.eq] + simp_rw [two_nsmul, mul_add, add_right_inj] at H' + have H'' : q * p = p * q := by + simp_rw [H'] + exact H.symm + rw [← H'', and_self_iff] + rw [← H'', ← two_nsmul, nsmul_right_inj (Nat.zero_ne_add_one 1).symm] at h' + exact h'.symm + +theorem isIdempotentElem_sub_iff {H : Type*} [Ring H] [IsAddTorsionFree H] {p q : H} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : + IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := +⟨commutes_of_isIdempotentElem_sub hp hq, + fun ⟨h1, h2⟩ => isIdempotentElem_sub_of hp hq h1 h2⟩ diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 363fdb8b578511..f82548eeee92e4 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -5,6 +5,7 @@ Authors: Yury Kudryashov -/ import Mathlib.LinearAlgebra.Quotient.Basic import Mathlib.LinearAlgebra.Prod +import Mathlib.Algebra.Ring.Idempotent /-! # Projection to a subspace @@ -514,32 +515,16 @@ by theorem LinearMap.isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : IsIdempotentElem (q - p) := by - simp_rw [IsIdempotentElem, Module.End.mul_eq_comp, sub_comp, comp_sub, hpq, hqp, - ← Module.End.mul_eq_comp, hp.eq, hq.eq, sub_self, sub_zero] + exact _root_.isIdempotentElem_sub_of hp hq hpq hqp /-- If `p,q` are idempotent operators and `q - p` is also an idempotent operator, then `p ∘ q = p = q ∘ p`. -/ theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : p.comp q = p ∧ q.comp p = p := -by - simp_rw [IsIdempotentElem, Module.End.mul_eq_comp, comp_sub, sub_comp, ← Module.End.mul_eq_comp, - hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp - have h' : ((2 : ℕ) • p : E →ₗ[R] E) = q.comp p + p.comp q := - by - simp_rw [two_smul] - nth_rw 2 [← hqp] - simp_rw [Module.End.mul_eq_comp, add_sub_cancel, add_comm] - have H : ((2 : ℕ) • p).comp q = q.comp (p.comp q) + p.comp q := by - simp_rw [h', add_comp, comp_assoc, ← Module.End.mul_eq_comp, hq.eq] - simp_rw [add_comm, two_smul, add_comp, add_right_inj] at H - have H' : q.comp ((2 : ℕ) • p) = q.comp p + q.comp (p.comp q) := by - simp_rw [h', comp_add, ← comp_assoc, ← Module.End.mul_eq_comp, hq.eq] - simp_rw [two_smul, comp_add, add_right_inj] at H' - have H'' : q.comp p = p.comp q := by - simp_rw [H'] - exact H.symm - rw [← H'', and_self_iff, ← smul_right_inj (two_ne_zero), h', ← H'', two_smul] + letI : IsAddTorsionFree (E →ₗ[R] E) := + noZeroSMulDivisors_nat_iff_isAddTorsionFree.mp instNoZeroSMulDivisors + _root_.commutes_of_isIdempotentElem_sub hp hq hqp /-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ From d4fb18b46731737b73ec60fabb6c12fd90969493 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Wed, 18 Jun 2025 20:43:47 +0000 Subject: [PATCH 04/86] fixing styles --- Mathlib/Algebra/Ring/Idempotent.lean | 29 ++++++++---------- Mathlib/LinearAlgebra/Projection.lean | 44 +++++++++++---------------- 2 files changed, 30 insertions(+), 43 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 861368d8633a1c..61bd1113cd3355 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -76,22 +76,20 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b) := add_sub_mul_of_commute (.all ..) hp hq end CommRing + +lemma sub_of [NonAssocRing R] {p q : R} (hp : IsIdempotentElem p) + (hq : IsIdempotentElem q) (hpq : p * q = p) (hqp : q * p = p) : IsIdempotentElem (q - p) := by + simp_rw [IsIdempotentElem, sub_mul, mul_sub, hpq, hqp, hp.eq, hq.eq, sub_self, sub_zero] + end IsIdempotentElem -lemma isIdempotentElem_sub_of {H : Type*} [NonAssocRing H] {p q : H} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) - (hpq : p * q = p) (hqp : q * p = p) : - IsIdempotentElem (q - p) := -by simp_rw [IsIdempotentElem, sub_mul, mul_sub, hpq, hqp, hp.eq, hq.eq, sub_self, sub_zero] - -lemma commutes_of_isIdempotentElem_sub - {H : Type*} [Ring H] [IsAddTorsionFree H] {p q : H} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : - p * q = p ∧ q * p = p := -by + +lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : + p * q = p ∧ q * p = p := by simp_rw [IsIdempotentElem, mul_sub, sub_mul, hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp - have h' : ((2 : ℕ) • p : H) = q * p + p * q := by + have h' : (2 : ℕ) • p = q * p + p * q := by simp_rw [two_nsmul] calc p + p = p + (p * q + q * p - p) := by rw [hqp] _ = q * p + p * q := by simp_rw [add_sub_cancel, add_comm] @@ -108,8 +106,7 @@ by rw [← H'', ← two_nsmul, nsmul_right_inj (Nat.zero_ne_add_one 1).symm] at h' exact h'.symm -theorem isIdempotentElem_sub_iff {H : Type*} [Ring H] [IsAddTorsionFree H] {p q : H} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : +theorem isIdempotentElem_sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := -⟨commutes_of_isIdempotentElem_sub hp hq, - fun ⟨h1, h2⟩ => isIdempotentElem_sub_of hp hq h1 h2⟩ + ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub_of hq h1 h2⟩ diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index f82548eeee92e4..85188bdff20551 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -426,38 +426,31 @@ theorem eq_conj_prod_map' {f : E →ₗ[R] E} (h : IsProj p f) : coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero] theorem isIdempotentElem {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] - {T : V →ₗ[R] V} {U : Submodule R V} (h : IsProj U T) : - IsIdempotentElem T := -by ext; exact h.2 _ (h.1 _) + {T : V →ₗ[R] V} {U : Submodule R V} (h : IsProj U T) : IsIdempotentElem T := by + ext; exact h.2 _ (h.1 _) protected theorem range - {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] {T : V →ₗ[R] V} {U : Submodule R V} - (h : IsProj U T) : - range T = U := -by + {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] {T : V →ₗ[R] V} {U : Submodule R V} + (h : IsProj U T) : range T = U := by ext x refine ⟨fun ⟨y, hy⟩ => ?_, fun hx => ⟨x, h.map_id x hx⟩⟩ rw [← hy] exact h.map_mem y protected theorem top (S M : Type*) [Semiring S] [AddCommMonoid M] [Module S M] : - IsProj (⊤ : Submodule S M) (id (R := S)) := -⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ + IsProj (⊤ : Submodule S M) (id (R := S)) := ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ theorem _root_.LinearMap.subtype_top_comp_codRestrict_top_eq_id - {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] : - (Submodule.subtype ⊤).comp (IsProj.top S M).codRestrict = LinearMap.id := -rfl + {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] : + (Submodule.subtype ⊤).comp (IsProj.top S M).codRestrict = LinearMap.id := rfl theorem subtype_comp_codRestrict {S M : Type*} [Semiring S] [AddCommMonoid M] - [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : - (Submodule.subtype U).comp hf.codRestrict = f := -rfl + [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : + (Submodule.subtype U).comp hf.codRestrict = f := rfl theorem submodule_eq_top_iff {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] - {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : - U = (⊤ : Submodule S M) ↔ (Submodule.subtype _).comp hf.codRestrict = LinearMap.id := -by + {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : + U = (⊤ : Submodule S M) ↔ (Submodule.subtype _).comp hf.codRestrict = LinearMap.id := by rw [subtype_comp_codRestrict] constructor <;> rintro rfl · ext @@ -504,23 +497,21 @@ theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentEle /-- Given an idempotent linear operator `q`, we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ theorem IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) - {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : - q.comp p = p ↔ range p ≤ range q := -by + {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : + q.comp p = p ↔ range p ≤ range q := by simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] /-- If `p,q` are idempotent operators and `p ∘ q = p = q ∘ p`, then `q - p` is an idempotent operator. -/ theorem LinearMap.isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) - (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : - IsIdempotentElem (q - p) := by - exact _root_.isIdempotentElem_sub_of hp hq hpq hqp + (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : + IsIdempotentElem (q - p) := hp.sub_of hq hpq hqp /-- If `p,q` are idempotent operators and `q - p` is also an idempotent operator, then `p ∘ q = p = q ∘ p`. -/ theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E →ₗ[R] E} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : p.comp q = p ∧ q.comp p = p := letI : IsAddTorsionFree (E →ₗ[R] E) := noZeroSMulDivisors_nat_iff_isAddTorsionFree.mp instNoZeroSMulDivisors @@ -529,8 +520,7 @@ theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p /-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ theorem IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : - IsCompl (range T) (ker T) := -by + IsCompl (range T) (ker T) := by symm constructor · rw [disjoint_iff] From 8dd253dc332b022afa8703cb04d37754b75ba0a3 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Wed, 18 Jun 2025 21:43:56 +0000 Subject: [PATCH 05/86] moved results --- Mathlib/Algebra/Ring/Idempotent.lean | 5 ++--- Mathlib/LinearAlgebra/Projection.lean | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 61bd1113cd3355..b1adcb76e0892d 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -81,9 +81,6 @@ lemma sub_of [NonAssocRing R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpq : p * q = p) (hqp : q * p = p) : IsIdempotentElem (q - p) := by simp_rw [IsIdempotentElem, sub_mul, mul_sub, hpq, hqp, hp.eq, hq.eq, sub_self, sub_zero] -end IsIdempotentElem - - lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : p * q = p ∧ q * p = p := by @@ -110,3 +107,5 @@ theorem isIdempotentElem_sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub_of hq h1 h2⟩ + +end IsIdempotentElem diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 85188bdff20551..0645df3b586141 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -515,7 +515,7 @@ theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p p.comp q = p ∧ q.comp p = p := letI : IsAddTorsionFree (E →ₗ[R] E) := noZeroSMulDivisors_nat_iff_isAddTorsionFree.mp instNoZeroSMulDivisors - _root_.commutes_of_isIdempotentElem_sub hp hq hqp + hp.commutes_of_isIdempotentElem_sub hq hqp /-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ From b5e62f203bf02d481d770254521b0589f5facba9 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Thu, 19 Jun 2025 10:23:35 +0000 Subject: [PATCH 06/86] Update Mathlib/Algebra/Ring/Idempotent.lean Co-authored-by: Thomas Browning --- Mathlib/Algebra/Ring/Idempotent.lean | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index b1adcb76e0892d..4750def346ae04 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -86,22 +86,14 @@ lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} p * q = p ∧ q * p = p := by simp_rw [IsIdempotentElem, mul_sub, sub_mul, hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp - have h' : (2 : ℕ) • p = q * p + p * q := by - simp_rw [two_nsmul] - calc p + p = p + (p * q + q * p - p) := by rw [hqp] - _ = q * p + p * q := by simp_rw [add_sub_cancel, add_comm] - have H : ((2 : ℕ) • p) * q = q * (p * q) + p * q := by - simp_rw [h', add_mul, mul_assoc, hq.eq] - simp_rw [add_comm, two_nsmul, add_mul, add_right_inj] at H - have H' : q * ((2 : ℕ) • p) = q * p + q * (p * q) := by - simp_rw [h', mul_add, ← mul_assoc, hq.eq] - simp_rw [two_nsmul, mul_add, add_right_inj] at H' - have H'' : q * p = p * q := by - simp_rw [H'] - exact H.symm - rw [← H'', and_self_iff] - rw [← H'', ← two_nsmul, nsmul_right_inj (Nat.zero_ne_add_one 1).symm] at h' - exact h'.symm + have hpq : p * q = q * p := by + have h1 := congr_arg (q * ·) hqp + have h2 := congr_arg (· * q) hqp + simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1 + simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2 + exact h2.symm.trans h1 + rw [hpq, sub_eq_iff_eq_add, ← two_nsmul, ← two_nsmul, nsmul_right_inj (by simp)] at hqp + rw [hpq, hqp, and_self] theorem isIdempotentElem_sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : From 457590e93a6b44b215c580f1a937d50ae03dd3a9 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 19 Jun 2025 10:33:34 +0000 Subject: [PATCH 07/86] update --- Mathlib/LinearAlgebra/Projection.lean | 27 +++++++++------------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 0645df3b586141..1667e9a0f8cf92 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -388,6 +388,9 @@ theorem isProj_iff_isIdempotentElem (f : M →ₗ[S] M) : @[deprecated (since := "2025-01-12")] alias isProj_iff_idempotent := isProj_iff_isIdempotentElem +theorem isIdempotentElem + {T : M →ₗ[S] M} {U : Submodule S M} (h : IsProj U T) : IsIdempotentElem T := + T.isProj_iff_isIdempotentElem.mp ⟨U, h⟩ namespace IsProj variable {p m} @@ -425,33 +428,21 @@ theorem eq_conj_prod_map' {f : E →ₗ[R] E} (h : IsProj p f) : · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero, coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero] -theorem isIdempotentElem {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] - {T : V →ₗ[R] V} {U : Submodule R V} (h : IsProj U T) : IsIdempotentElem T := by - ext; exact h.2 _ (h.1 _) - -protected theorem range - {R V : Type*} [Semiring R] [AddCommMonoid V] [Module R V] {T : V →ₗ[R] V} {U : Submodule R V} +protected theorem range {T : M →ₗ[S] M} {U : Submodule S M} (h : IsProj U T) : range T = U := by ext x - refine ⟨fun ⟨y, hy⟩ => ?_, fun hx => ⟨x, h.map_id x hx⟩⟩ - rw [← hy] - exact h.map_mem y + exact ⟨fun ⟨y, hy⟩ => hy ▸ h.map_mem y, fun hx => ⟨x, h.map_id x hx⟩⟩ protected theorem top (S M : Type*) [Semiring S] [AddCommMonoid M] [Module S M] : IsProj (⊤ : Submodule S M) (id (R := S)) := ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ -theorem _root_.LinearMap.subtype_top_comp_codRestrict_top_eq_id - {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] : - (Submodule.subtype ⊤).comp (IsProj.top S M).codRestrict = LinearMap.id := rfl - theorem subtype_comp_codRestrict {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : (Submodule.subtype U).comp hf.codRestrict = f := rfl theorem submodule_eq_top_iff {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : - U = (⊤ : Submodule S M) ↔ (Submodule.subtype _).comp hf.codRestrict = LinearMap.id := by - rw [subtype_comp_codRestrict] + U = (⊤ : Submodule S M) ↔ f = LinearMap.id := by constructor <;> rintro rfl · ext simp only [id_coe, id_eq, hf.2 _ mem_top] @@ -489,14 +480,14 @@ open Submodule LinearMap /-- Given an idempotent linear operator `p`, we have `x ∈ range p` if and only if `p(x) = x` for all `x`. -/ -theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : +theorem LinearMap.IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : x ∈ range p ↔ p x = x := by refine ⟨fun ⟨y, hy⟩ => ?_, fun h => ⟨x, h⟩⟩ rw [← hy, ← Module.End.mul_apply, hp.eq] /-- Given an idempotent linear operator `q`, we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ -theorem IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) +theorem LinearMap.IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : q.comp p = p ↔ range p ≤ range q := by simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, @@ -519,7 +510,7 @@ theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p /-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ -theorem IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : +theorem LinearMap.IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : IsCompl (range T) (ker T) := by symm constructor From f3285f5336e86cb0555fb077ed4ac0f487523ea8 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 19 Jun 2025 10:36:28 +0000 Subject: [PATCH 08/86] removed variables --- Mathlib/LinearAlgebra/Projection.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 1667e9a0f8cf92..7b4f8152e92537 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -436,12 +436,10 @@ protected theorem range {T : M →ₗ[S] M} {U : Submodule S M} protected theorem top (S M : Type*) [Semiring S] [AddCommMonoid M] [Module S M] : IsProj (⊤ : Submodule S M) (id (R := S)) := ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ -theorem subtype_comp_codRestrict {S M : Type*} [Semiring S] [AddCommMonoid M] - [Module S M] {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : +theorem subtype_comp_codRestrict {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : (Submodule.subtype U).comp hf.codRestrict = f := rfl -theorem submodule_eq_top_iff {S M : Type*} [Semiring S] [AddCommMonoid M] [Module S M] - {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : +theorem submodule_eq_top_iff {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : U = (⊤ : Submodule S M) ↔ f = LinearMap.id := by constructor <;> rintro rfl · ext From f46a4c169f2397f3c25bf0b4c37ffdd1939f8aeb Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 19 Jun 2025 12:43:19 +0000 Subject: [PATCH 09/86] namespace --- Mathlib/LinearAlgebra/Projection.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 7b4f8152e92537..aea0416692b358 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -470,7 +470,7 @@ end LinearMap end CommRing -section +namespace LinearMap variable {R E M : Type*} [Semiring R] [AddCommGroup E] [Module R E] [AddCommMonoid M] [Module R M] @@ -478,14 +478,14 @@ open Submodule LinearMap /-- Given an idempotent linear operator `p`, we have `x ∈ range p` if and only if `p(x) = x` for all `x`. -/ -theorem LinearMap.IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : +theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : x ∈ range p ↔ p x = x := by refine ⟨fun ⟨y, hy⟩ => ?_, fun h => ⟨x, h⟩⟩ rw [← hy, ← Module.End.mul_apply, hp.eq] /-- Given an idempotent linear operator `q`, we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ -theorem LinearMap.IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) +theorem IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : q.comp p = p ↔ range p ≤ range q := by simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, @@ -493,13 +493,13 @@ theorem LinearMap.IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : /-- If `p,q` are idempotent operators and `p ∘ q = p = q ∘ p`, then `q - p` is an idempotent operator. -/ -theorem LinearMap.isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) +theorem isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : IsIdempotentElem (q - p) := hp.sub_of hq hpq hqp /-- If `p,q` are idempotent operators and `q - p` is also an idempotent operator, then `p ∘ q = p = q ∘ p`. -/ -theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E →ₗ[R] E} +theorem commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : p.comp q = p ∧ q.comp p = p := letI : IsAddTorsionFree (E →ₗ[R] E) := @@ -508,7 +508,7 @@ theorem LinearMap.commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p /-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ -theorem LinearMap.IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : +theorem IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : IsCompl (range T) (ker T) := by symm constructor @@ -533,4 +533,4 @@ theorem LinearMap.IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : Is · simp only [mem_range, exists_apply_eq_apply] · simp only [Submodule.coe_mk, sub_add_cancel] -end +end LinearMap From 7730bf4cb89e0e132103142ac765a144e7b09e04 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 20 Jun 2025 17:19:16 +0000 Subject: [PATCH 10/86] added suggestions --- Mathlib/Algebra/Ring/Idempotent.lean | 6 +++--- Mathlib/LinearAlgebra/Projection.lean | 9 +++------ 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 4750def346ae04..0472ef3b9b5c8f 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -77,7 +77,7 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : end CommRing -lemma sub_of [NonAssocRing R] {p q : R} (hp : IsIdempotentElem p) +lemma sub_of_mul_eq [NonAssocRing R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpq : p * q = p) (hqp : q * p = p) : IsIdempotentElem (q - p) := by simp_rw [IsIdempotentElem, sub_mul, mul_sub, hpq, hqp, hp.eq, hq.eq, sub_self, sub_zero] @@ -95,9 +95,9 @@ lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} rw [hpq, sub_eq_iff_eq_add, ← two_nsmul, ← two_nsmul, nsmul_right_inj (by simp)] at hqp rw [hpq, hqp, and_self] -theorem isIdempotentElem_sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} +theorem sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := - ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub_of hq h1 h2⟩ + ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub_of_mul_eq hq h1 h2⟩ end IsIdempotentElem diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index aea0416692b358..0938ed0b8ce868 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -444,10 +444,7 @@ theorem submodule_eq_top_iff {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsPro constructor <;> rintro rfl · ext simp only [id_coe, id_eq, hf.2 _ mem_top] - · refine eq_top_iff'.mpr ?mpr.a - intro x - rw [← id_apply (R := S) x] - exact hf.map_mem x + · rw [← hf.range, range_id] end IsProj @@ -485,7 +482,7 @@ theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentEle /-- Given an idempotent linear operator `q`, we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ -theorem IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) +theorem IsIdempotentElem.comp_eq_right_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : q.comp p = p ↔ range p ≤ range q := by simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, @@ -495,7 +492,7 @@ theorem IsIdempotentElem.comp_idempotent_iff {q : M →ₗ[R] M} (hq : IsIdempot then `q - p` is an idempotent operator. -/ theorem isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : - IsIdempotentElem (q - p) := hp.sub_of hq hpq hqp + IsIdempotentElem (q - p) := hp.sub_of_mul_eq hq hpq hqp /-- If `p,q` are idempotent operators and `q - p` is also an idempotent operator, then `p ∘ q = p = q ∘ p`. -/ From 808e8394e1d8f947d87d04a568dc2e15b7a32d16 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Wed, 25 Jun 2025 17:11:39 +0000 Subject: [PATCH 11/86] Update Projection.lean --- Mathlib/LinearAlgebra/Projection.lean | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 0938ed0b8ce868..7a579a511af5ce 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -503,31 +503,4 @@ theorem commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E → noZeroSMulDivisors_nat_iff_isAddTorsionFree.mp instNoZeroSMulDivisors hp.commutes_of_isIdempotentElem_sub hq hqp -/-- Given any idempotent operator `T`, then `IsCompl T.range T.ker`, - in other words, there exists unique `v ∈ range(T)` and `w ∈ ker(T)` such that `x = v + w`. -/ -theorem IsIdempotentElem.isCompl_range_ker {T : E →ₗ[R] E} (h : IsIdempotentElem T) : - IsCompl (range T) (ker T) := by - symm - constructor - · rw [disjoint_iff] - ext x - simp only [mem_bot, mem_inf, mem_ker, mem_range] - constructor <;> intro h' - · rcases h'.2 with ⟨y, rfl⟩ - rw [← IsIdempotentElem.eq h, Module.End.mul_apply] - exact h'.1 - · rw [h', map_zero, eq_self_iff_true, true_and] - use x - simp only [h', map_zero, eq_self_iff_true] - · suffices ∀ x : E, ∃ v : ker T, ∃ w : range T, x = v + w by - rw [codisjoint_iff] - ext x - rcases this x with ⟨v, w, rfl⟩ - simp only [mem_top, iff_true] - exact add_mem_sup (SetLike.coe_mem v) (SetLike.coe_mem w) - refine fun x => ⟨⟨x - T x, ?_⟩, ⟨T x, ?_⟩, ?_⟩ - · rw [mem_ker, map_sub, ← Module.End.mul_apply, IsIdempotentElem.eq h, sub_self] - · simp only [mem_range, exists_apply_eq_apply] - · simp only [Submodule.coe_mk, sub_add_cancel] - end LinearMap From fe3e04498e83bae9f224582c4167c749b6792960 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Mon, 30 Jun 2025 18:53:23 +0000 Subject: [PATCH 12/86] Update Projection.lean --- Mathlib/LinearAlgebra/Projection.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 10f921a27c6940..e02dc9c9c9e616 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -390,6 +390,7 @@ theorem isProj_iff_isIdempotentElem (f : M →ₗ[S] M) : theorem isIdempotentElem {T : M →ₗ[S] M} {U : Submodule S M} (h : IsProj U T) : IsIdempotentElem T := T.isProj_iff_isIdempotentElem.mp ⟨U, h⟩ + namespace IsProj variable {p m} From 23f11aab8cf9c21a26f8237005dea85218e4f4c6 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 30 Jun 2025 22:09:25 +0000 Subject: [PATCH 13/86] update --- Mathlib/LinearAlgebra/Projection.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index e02dc9c9c9e616..bfd274913fd426 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -433,8 +433,9 @@ protected theorem range {T : M →ₗ[S] M} {U : Submodule S M} ext x exact ⟨fun ⟨y, hy⟩ => hy ▸ h.map_mem y, fun hx => ⟨x, h.map_id x hx⟩⟩ -protected theorem top (S M : Type*) [Semiring S] [AddCommMonoid M] [Module S M] : - IsProj (⊤ : Submodule S M) (id (R := S)) := ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ +variable (S M) in +protected theorem top : IsProj (⊤ : Submodule S M) (id (R := S)) := + ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ theorem subtype_comp_codRestrict {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : (Submodule.subtype U).comp hf.codRestrict = f := rfl From 80bd03c35540cf56eecc265f55a2c970cf0dd15b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 30 Jun 2025 22:14:10 +0000 Subject: [PATCH 14/86] added LinearMap.IsProj.bot --- Mathlib/LinearAlgebra/Projection.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index bfd274913fd426..a5ae0f63c284d4 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -433,6 +433,10 @@ protected theorem range {T : M →ₗ[S] M} {U : Submodule S M} ext x exact ⟨fun ⟨y, hy⟩ => hy ▸ h.map_mem y, fun hx => ⟨x, h.map_id x hx⟩⟩ +variable (S M) in +protected theorem bot : IsProj (⊥ : Submodule S M) (0 : M →ₗ[S] M) := + ⟨congrFun rfl, by simp only [mem_bot, zero_apply, forall_eq]⟩ + variable (S M) in protected theorem top : IsProj (⊤ : Submodule S M) (id (R := S)) := ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ From 0c7a20f3009f0a70a5b0c0300f3574ec784781aa Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sat, 5 Jul 2025 14:33:55 +0000 Subject: [PATCH 15/86] star projection sub --- Mathlib/Algebra/Ring/Idempotent.lean | 9 +++++---- Mathlib/Algebra/Star/StarProjection.lean | 18 ++++++++++++++++++ Mathlib/LinearAlgebra/Projection.lean | 4 ++-- 3 files changed, 25 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index c684ea761f60cf..d028c08500223e 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -85,9 +85,10 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : end CommRing -lemma sub_of_mul_eq [NonAssocRing R] {p q : R} (hp : IsIdempotentElem p) - (hq : IsIdempotentElem q) (hpq : p * q = p) (hqp : q * p = p) : IsIdempotentElem (q - p) := by - simp_rw [IsIdempotentElem, sub_mul, mul_sub, hpq, hqp, hp.eq, hq.eq, sub_self, sub_zero] +/-- `b - a` is idempotent when `a * b = a` and `b * a = a` -/ +lemma sub [NonAssocRing R] {a b : R} (ha : IsIdempotentElem a) + (hb : IsIdempotentElem b) (hab : a * b = a) (hba : b * a = a) : IsIdempotentElem (b - a) := by + simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero] lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : @@ -106,7 +107,7 @@ lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} theorem sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := - ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub_of_mul_eq hq h1 h2⟩ + ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩ /-- `a + b` is idempotent when `a` and `b` anti-commute. -/ theorem add [NonUnitalNonAssocSemiring R] diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index b1c043d5e736f3..ee0e5b36efa190 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -89,6 +89,24 @@ theorem mul [NonUnitalSemiring R] [StarRing R] isSelfAdjoint := (IsSelfAdjoint.commute_iff hp.isSelfAdjoint hq.isSelfAdjoint).mp hpq isIdempotentElem := hp.isIdempotentElem.mul_of_commute hpq hq.isIdempotentElem +/-- `q - p` is a star projection if `p * q = p` -/ +theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] + (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) : + IsStarProjection (q - p) where + isSelfAdjoint := hq.isSelfAdjoint.sub hp.isSelfAdjoint + isIdempotentElem := hp.isIdempotentElem.sub + hq.isIdempotentElem hpq + (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))) + +/-- `q - p` is a star projection if `q * p = p` -/ +theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] + (hp : IsStarProjection p) (hq : IsStarProjection q) (hqp : q * p = p) : + IsStarProjection (q - p) where + isSelfAdjoint := hq.isSelfAdjoint.sub hp.isSelfAdjoint + isIdempotentElem := hp.isIdempotentElem.sub + hq.isIdempotentElem + (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) hqp + theorem add_sub_mul_of_commute [Ring R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (p + q - p * q) where diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index a5ae0f63c284d4..37d9d96b91d6b5 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -495,9 +495,9 @@ theorem IsIdempotentElem.comp_eq_right_iff {q : M →ₗ[R] M} (hq : IsIdempoten /-- If `p,q` are idempotent operators and `p ∘ q = p = q ∘ p`, then `q - p` is an idempotent operator. -/ -theorem isIdempotentElem_sub_of {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) +theorem isIdempotentElem_sub {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : - IsIdempotentElem (q - p) := hp.sub_of_mul_eq hq hpq hqp + IsIdempotentElem (q - p) := hp.sub hq hpq hqp /-- If `p,q` are idempotent operators and `q - p` is also an idempotent operator, then `p ∘ q = p = q ∘ p`. -/ From 80895b427f61dd10597820029a3371ecb2c66d34 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sat, 5 Jul 2025 14:39:42 +0000 Subject: [PATCH 16/86] remove useless lemmas --- Mathlib/LinearAlgebra/Projection.lean | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 37d9d96b91d6b5..bfced18d70ca7a 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -493,19 +493,4 @@ theorem IsIdempotentElem.comp_eq_right_iff {q : M →ₗ[R] M} (hq : IsIdempoten simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] -/-- If `p,q` are idempotent operators and `p ∘ q = p = q ∘ p`, - then `q - p` is an idempotent operator. -/ -theorem isIdempotentElem_sub {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) - (hq : IsIdempotentElem q) (hpq : p.comp q = p) (hqp : q.comp p = p) : - IsIdempotentElem (q - p) := hp.sub hq hpq hqp - -/-- If `p,q` are idempotent operators and `q - p` is also an idempotent - operator, then `p ∘ q = p = q ∘ p`. -/ -theorem commutes_of_isIdempotentElem_sub [NoZeroSMulDivisors ℕ E] {p q : E →ₗ[R] E} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : - p.comp q = p ∧ q.comp p = p := - letI : IsAddTorsionFree (E →ₗ[R] E) := - noZeroSMulDivisors_nat_iff_isAddTorsionFree.mp instNoZeroSMulDivisors - hp.commutes_of_isIdempotentElem_sub hq hqp - end LinearMap From 01e09ea66c51ef8994259cdb6c6239727de2a75f Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sat, 5 Jul 2025 14:43:14 +0000 Subject: [PATCH 17/86] golf --- Mathlib/Algebra/Star/StarProjection.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index ee0e5b36efa190..19a121851033fb 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -101,11 +101,8 @@ theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] /-- `q - p` is a star projection if `q * p = p` -/ theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hqp : q * p = p) : - IsStarProjection (q - p) where - isSelfAdjoint := hq.isSelfAdjoint.sub hp.isSelfAdjoint - isIdempotentElem := hp.isIdempotentElem.sub - hq.isIdempotentElem - (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) hqp + IsStarProjection (q - p) := hp.sub_of_mul_eq_left hq + (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) theorem add_sub_mul_of_commute [Ring R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) : From 5e17e24d37690e5898cec4fdd39df93c61cd1d7e Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sat, 5 Jul 2025 14:46:55 +0000 Subject: [PATCH 18/86] doc --- Mathlib/Algebra/Star/StarProjection.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index 19a121851033fb..92b97eae3eba83 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -89,7 +89,7 @@ theorem mul [NonUnitalSemiring R] [StarRing R] isSelfAdjoint := (IsSelfAdjoint.commute_iff hp.isSelfAdjoint hq.isSelfAdjoint).mp hpq isIdempotentElem := hp.isIdempotentElem.mul_of_commute hpq hq.isIdempotentElem -/-- `q - p` is a star projection if `p * q = p` -/ +/-- `q - p` is a star projection if `p * q = p` for star projections `p,q`. -/ theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) : IsStarProjection (q - p) where @@ -98,7 +98,7 @@ theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] hq.isIdempotentElem hpq (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))) -/-- `q - p` is a star projection if `q * p = p` -/ +/-- `q - p` is a star projection if `q * p = p` for star projections `p,q`. -/ theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hqp : q * p = p) : IsStarProjection (q - p) := hp.sub_of_mul_eq_left hq From 08b389098eaaf84f6f5814446f31b04ec42578f8 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Sat, 5 Jul 2025 15:07:34 +0000 Subject: [PATCH 19/86] Update Projection.lean --- Mathlib/LinearAlgebra/Projection.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index bfced18d70ca7a..50d5019d7e694f 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -5,7 +5,6 @@ Authors: Yury Kudryashov -/ import Mathlib.LinearAlgebra.Quotient.Basic import Mathlib.LinearAlgebra.Prod -import Mathlib.Algebra.Ring.Idempotent /-! # Projection to a subspace From 9920520457fedb56da0fcc9388376c053fd25c7b Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Sat, 5 Jul 2025 16:32:14 +0000 Subject: [PATCH 20/86] Update Projection.lean --- Mathlib/LinearAlgebra/Projection.lean | 50 --------------------------- 1 file changed, 50 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index 50d5019d7e694f..f92c3a80effc4c 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -386,10 +386,6 @@ theorem isProj_iff_isIdempotentElem (f : M →ₗ[S] M) : @[deprecated (since := "2025-01-12")] alias isProj_iff_idempotent := isProj_iff_isIdempotentElem -theorem isIdempotentElem - {T : M →ₗ[S] M} {U : Submodule S M} (h : IsProj U T) : IsIdempotentElem T := - T.isProj_iff_isIdempotentElem.mp ⟨U, h⟩ - namespace IsProj variable {p m} @@ -427,29 +423,6 @@ theorem eq_conj_prod_map' {f : E →ₗ[R] E} (h : IsProj p f) : · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero, coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero] -protected theorem range {T : M →ₗ[S] M} {U : Submodule S M} - (h : IsProj U T) : range T = U := by - ext x - exact ⟨fun ⟨y, hy⟩ => hy ▸ h.map_mem y, fun hx => ⟨x, h.map_id x hx⟩⟩ - -variable (S M) in -protected theorem bot : IsProj (⊥ : Submodule S M) (0 : M →ₗ[S] M) := - ⟨congrFun rfl, by simp only [mem_bot, zero_apply, forall_eq]⟩ - -variable (S M) in -protected theorem top : IsProj (⊤ : Submodule S M) (id (R := S)) := - ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩ - -theorem subtype_comp_codRestrict {U : Submodule S M} {f : M →ₗ[S] M} (hf : IsProj U f) : - (Submodule.subtype U).comp hf.codRestrict = f := rfl - -theorem submodule_eq_top_iff {f : M →ₗ[S] M} {U : Submodule S M} (hf : IsProj U f) : - U = (⊤ : Submodule S M) ↔ f = LinearMap.id := by - constructor <;> rintro rfl - · ext - simp only [id_coe, id_eq, hf.2 _ mem_top] - · rw [← hf.range, range_id] - end IsProj end LinearMap @@ -470,26 +443,3 @@ theorem IsProj.eq_conj_prodMap {f : E →ₗ[R] E} (h : IsProj p f) : end LinearMap end CommRing - -namespace LinearMap -variable {R E M : Type*} [Semiring R] [AddCommGroup E] [Module R E] - [AddCommMonoid M] [Module R M] - -open Submodule LinearMap - -/-- Given an idempotent linear operator `p`, we have - `x ∈ range p` if and only if `p(x) = x` for all `x`. -/ -theorem IsIdempotentElem.mem_range_iff {p : M →ₗ[R] M} (hp : IsIdempotentElem p) {x : M} : - x ∈ range p ↔ p x = x := by - refine ⟨fun ⟨y, hy⟩ => ?_, fun h => ⟨x, h⟩⟩ - rw [← hy, ← Module.End.mul_apply, hp.eq] - -/-- Given an idempotent linear operator `q`, - we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/ -theorem IsIdempotentElem.comp_eq_right_iff {q : M →ₗ[R] M} (hq : IsIdempotentElem q) - {E₂ : Type*} [AddCommMonoid E₂] [Module R E₂] (p : E₂ →ₗ[R] M) : - q.comp p = p ↔ range p ≤ range q := by - simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, - SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff] - -end LinearMap From 2dd9dac6deac42dc6be3ea8f3750e7a97ea4d1b6 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Sat, 5 Jul 2025 16:37:09 +0000 Subject: [PATCH 21/86] Update Idempotent.lean --- Mathlib/Algebra/Ring/Idempotent.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index d028c08500223e..af70d6dab28196 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -85,7 +85,7 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : end CommRing -/-- `b - a` is idempotent when `a * b = a` and `b * a = a` -/ +/-- `b - a` is idempotent when `a * b = a` and `b * a = a`. -/ lemma sub [NonAssocRing R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (hab : a * b = a) (hba : b * a = a) : IsIdempotentElem (b - a) := by simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero] From bbf2c7d944b972a14d8b0d7381e316505a7f48a2 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 7 Jul 2025 15:20:21 +0000 Subject: [PATCH 22/86] added p le q when pq eq p --- Mathlib/Algebra/Order/Star/Basic.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index ee684da125f806..744a8264fc5ea8 100644 --- a/Mathlib/Algebra/Order/Star/Basic.lean +++ b/Mathlib/Algebra/Order/Star/Basic.lean @@ -405,7 +405,16 @@ theorem one_sub_nonneg (hp : IsStarProjection p) : 0 ≤ 1 - p := hp.one_sub.non theorem le_one (hp : IsStarProjection p) : p ≤ 1 := sub_nonneg.mp hp.one_sub_nonneg +/-- For a star projection `p`, we have `0 ≤ p ≤ 1`. -/ theorem mem_Icc (hp : IsStarProjection p) : p ∈ Set.Icc (0 : R) 1 := by simp only [Set.mem_Icc, hp.nonneg, hp.le_one, and_self] +/-- A star projection `p` is less than or equal to a star projection `q` when `p * q = p`. -/ +theorem le_of_mul_eq_left {q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) + (hpq : p * q = p) : p ≤ q := sub_nonneg.mp (hp.sub_of_mul_eq_left hq hpq).nonneg + +/-- A star projection `p` is less than or equal to a star projection `q` when `q * p = p`. -/ +theorem le_of_mul_eq_right {q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) + (hpq : q * p = p) : p ≤ q := sub_nonneg.mp (hp.sub_of_mul_eq_right hq hpq).nonneg + end IsStarProjection From 366ccdac7ba9802e193bcbbcdfad3400201dcb23 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Mon, 14 Jul 2025 17:48:29 +0000 Subject: [PATCH 23/86] Update StarProjection.lean --- Mathlib/Algebra/Star/StarProjection.lean | 26 ++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index 92b97eae3eba83..c0ac58b0f140cd 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -89,7 +89,7 @@ theorem mul [NonUnitalSemiring R] [StarRing R] isSelfAdjoint := (IsSelfAdjoint.commute_iff hp.isSelfAdjoint hq.isSelfAdjoint).mp hpq isIdempotentElem := hp.isIdempotentElem.mul_of_commute hpq hq.isIdempotentElem -/-- `q - p` is a star projection if `p * q = p` for star projections `p,q`. -/ +/-- `q - p` is a star projection when `p * q = p`. -/ theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) : IsStarProjection (q - p) where @@ -98,12 +98,34 @@ theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] hq.isIdempotentElem hpq (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))) -/-- `q - p` is a star projection if `q * p = p` for star projections `p,q`. -/ +/-- `q - p` is a star projection when `q * p = p`. -/ theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hqp : q * p = p) : IsStarProjection (q - p) := hp.sub_of_mul_eq_left hq (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) +/-- `q - p` is a star projection iff `p * q = p`. -/ +theorem IsStarProjection.sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] + {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : + IsStarProjection (q - p) ↔ p * q = p := by + rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem] + simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true] + nth_rw 3 [← hp.isSelfAdjoint] + nth_rw 2 [← hq.isSelfAdjoint] + rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm] + simp_rw [and_self] + +/-- `q - p` is a star projection iff `q * p = p`. -/ +theorem IsStarProjection.sub_iff_mul_eq_right [Ring R] [StarRing R] [IsAddTorsionFree R] + {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : + IsStarProjection (q - p) ↔ q * p = p := by + rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem] + simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true] + nth_rw 1 [← hp.isSelfAdjoint] + nth_rw 1 [← hq.isSelfAdjoint] + rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm] + simp_rw [and_self] + theorem add_sub_mul_of_commute [Ring R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (p + q - p * q) where From 226f700284a392dc8ee053c20b9ad678f45de371 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 14 Jul 2025 18:43:05 +0000 Subject: [PATCH 24/86] fix --- Mathlib/Algebra/Star/StarProjection.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index c0ac58b0f140cd..33dd80fbb9a2a0 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -104,7 +104,7 @@ theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] IsStarProjection (q - p) := hp.sub_of_mul_eq_left hq (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) -/-- `q - p` is a star projection iff `p * q = p`. -/ +/-- `q - p` is a star projection iff `p * q = p`. -/ theorem IsStarProjection.sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ p * q = p := by From b9340369eadfbac212ea2ab8370b42131505ecea Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 14 Jul 2025 18:49:08 +0000 Subject: [PATCH 25/86] fix --- Mathlib/Algebra/Star/StarProjection.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index 33dd80fbb9a2a0..aa6cf5d30363ae 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -105,7 +105,7 @@ theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) /-- `q - p` is a star projection iff `p * q = p`. -/ -theorem IsStarProjection.sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] +theorem sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ p * q = p := by rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem] @@ -116,7 +116,7 @@ theorem IsStarProjection.sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsion simp_rw [and_self] /-- `q - p` is a star projection iff `q * p = p`. -/ -theorem IsStarProjection.sub_iff_mul_eq_right [Ring R] [StarRing R] [IsAddTorsionFree R] +theorem sub_iff_mul_eq_right [Ring R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ q * p = p := by rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem] From 480399f97f6270d2d92ccee2754267fd5ccd7d70 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 14 Jul 2025 19:28:43 +0000 Subject: [PATCH 26/86] starProjection_le_starProjection_iff --- .../Analysis/InnerProductSpace/Positive.lean | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index e2042a32c05a79..ac9fbc189b1771 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -235,6 +235,36 @@ theorem IsIdempotentElem.isPositive_iff_isSelfAdjoint {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : p.IsPositive ↔ IsSelfAdjoint p := ⟨fun h => h.isSelfAdjoint, fun h => IsPositive.of_isStarProjection ⟨hp, h⟩⟩ +/-- For star projection operators `p,q` in a complex-Hilbert space, +we have `p ≤ q` iff `p ∘ q = p`. -/ +theorem IsStarProjection.le_iff_comp_eq_self [InnerProductSpace ℂ E] {p q : E →L[ℂ] E} + (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ p ∘L q = p := by + refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ + IsPositive.of_isStarProjection (hp.sub_of_mul_eq_left hq hpq)⟩ + rw [← sub_eq_zero, ← coe_inj, coe_zero, ← inner_map_self_eq_zero] + intro x + specialize h2 ((1 - q) x) + simp [reApplyInnerSelf_apply] at h2 + simp_rw [← ContinuousLinearMap.mul_apply, hq.1.eq, sub_self, zero_sub, mul_apply, + ← map_sub, inner_neg_left, Complex.neg_re, le_neg, neg_zero] at h2 + rw [← hp.1.eq, ContinuousLinearMap.mul_apply, ← adjoint_inner_right, + isSelfAdjoint_iff'.mp hp.2, ← RCLike.re_eq_complex_re, re_inner_self_nonpos] at h2 + simp [sub_eq_zero] at h2 + simp [h2] + +/-- In a complex-Hilbert space, `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ +theorem starProjection_le_starProjection_iff [InnerProductSpace ℂ E] + (U V : Submodule ℂ E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : + U.starProjection ≤ V.starProjection ↔ U ≤ V := by + rw [IsStarProjection.le_iff_comp_eq_self (isStarProjection_starProjection _) + (isStarProjection_starProjection _), ← star_inj, + (isStarProjection_starProjection _).isSelfAdjoint, star_eq_adjoint, adjoint_comp] + simp_rw [← star_eq_adjoint, (isStarProjection_starProjection _).isSelfAdjoint.star_eq] + rw [← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] + · have : ∀ p : E →L[ℂ] E, LinearMap.range p.toLinearMap = LinearMap.range p := fun p => rfl + simp_rw [this, Submodule.range_starProjection] + · exact congr(LinearMapClass.linearMap $((isStarProjection_starProjection V).isIdempotentElem.eq)) + end ContinuousLinearMap namespace LinearMap From 0ae9522068c2f2faf43688f767782b8e2a0ae03e Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 28 Jul 2025 20:13:10 +0000 Subject: [PATCH 27/86] generalize --- .../Analysis/InnerProductSpace/Positive.lean | 81 ++++++++++++++----- 1 file changed, 62 insertions(+), 19 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index b00e95e506c4f1..cbfc01933b122f 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -385,33 +385,76 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : tfae_have 2 ↔ 4 := hp.isSelfAdjoint_iff_orthogonal_range tfae_finish -/-- For star projection operators `p,q` in a complex-Hilbert space, -we have `p ≤ q` iff `p ∘ q = p`. -/ -theorem IsStarProjection.le_iff_comp_eq_self [InnerProductSpace ℂ E] {p q : E →L[ℂ] E} +--move to `Projection` +theorem IsStarProjection.norm_apply_le {T : E →L[𝕜] E} (hT : IsStarProjection T) (v : E) : + ‖T v‖ ≤ ‖v‖ := by + obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT + exact hht ▸ Submodule.norm_starProjection_apply_le _ _ + +open RCLike +--move to `Projection` +theorem IsStarProjection.reApplyInnerSelf_eq {T : E →L[𝕜] E} (hT : IsStarProjection T) (v : E) : + T.reApplyInnerSelf v = ‖T v‖ ^ 2 := by + obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT + calc T.reApplyInnerSelf v = re (inner 𝕜 (T v) v) := rfl + _ = re (inner 𝕜 (T v) (T v)) + re (inner 𝕜 (T v) ((1 - T) v)) := by + simp [← map_add, ← inner_add_right] + _ = re (inner 𝕜 (T v) (T v)) + 0 := ?_ + _ = ‖T v‖ ^ 2 := by simp; exact inner_self_eq_norm_sq _ + congr + rw [hht, ← Submodule.starProjection_orthogonal', + Submodule.inner_starProjection_left_eq_right, + (Submodule.starProjection_apply_eq_zero_iff _).mpr (by simp)] + simp + +open ContinuousLinearMap +-- move to `Projection` +theorem IsStarProjection.apply_norm_eq_iff {T : E →L[𝕜] E} (hT : IsStarProjection T) {v : E} : + ‖T v‖ = ‖v‖ ↔ v ∈ LinearMap.range T := by + refine ⟨fun h => ?_, fun h => congr(‖$((LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mp h)‖)⟩ + have := calc 0 = ‖v‖ ^ 2 - ‖T v‖ ^ 2 := by simp [h] + _ = ‖T v + (1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by simp + _ = ‖T v‖ ^ 2 + ‖(1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by + congr + rw [norm_add_sq (𝕜 := 𝕜), ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] + simp [← mul_apply, hT.isIdempotentElem.eq] + _ = ‖(1 - T) v‖ ^ 2 := by simp + rw [eq_comm, sq_eq_zero_iff, norm_eq_zero, sub_apply, one_apply, sub_eq_zero, eq_comm] at this + exact (LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mpr this + +/-- For star projection operators `p,q`, we have `p ≤ q` iff `p ∘ q = p`. -/ +theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ p ∘L q = p := by refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ IsPositive.of_isStarProjection (hp.sub_of_mul_eq_left hq hpq)⟩ - rw [← sub_eq_zero, ← coe_inj, coe_zero, ← inner_map_self_eq_zero] - intro x - specialize h2 ((1 - q) x) - simp [reApplyInnerSelf_apply] at h2 - simp_rw [← ContinuousLinearMap.mul_apply, hq.1.eq, sub_self, zero_sub, mul_apply, - ← map_sub, inner_neg_left, Complex.neg_re, le_neg, neg_zero] at h2 - rw [← hp.1.eq, ContinuousLinearMap.mul_apply, ← adjoint_inner_right, - isSelfAdjoint_iff'.mp hp.2, ← RCLike.re_eq_complex_re, re_inner_self_nonpos] at h2 - simp [sub_eq_zero] at h2 - simp [h2] - -/-- In a complex-Hilbert space, `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ -theorem starProjection_le_starProjection_iff [InnerProductSpace ℂ E] - (U V : Submodule ℂ E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : + rw [← star_inj] + simp_rw [star_eq_adjoint, adjoint_comp, hp.isSelfAdjoint.adjoint_eq, hq.isSelfAdjoint.adjoint_eq] + have : q.comp p = p ↔ LinearMap.range p ≤ LinearMap.range q := by + simpa [coe_comp, ← coe_inj] using LinearMap.IsIdempotentElem.comp_eq_right_iff + congr(LinearMapClass.linearMap $hq.isIdempotentElem.eq) p.toLinearMap + rw [this] + intro a ha + specialize h2 a + have {T : E →L[𝕜] E} (hT : IsStarProjection T) : a ∈ LinearMap.range T ↔ T a = a := + (LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)) + simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, + ← reApplyInnerSelf_apply, hq.reApplyInnerSelf_eq, hp.reApplyInnerSelf_eq, (this hp).mp ha, + sub_nonneg, sq_le_sq, abs_norm] at h2 + exact hq.apply_norm_eq_iff.mp (le_antisymm (hq.norm_apply_le a) h2) + +/-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ +theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) + [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection ≤ V.starProjection ↔ U ≤ V := by - rw [IsStarProjection.le_iff_comp_eq_self (isStarProjection_starProjection _) + rw [IsStarProjection.le_iff_comp_eq_left (isStarProjection_starProjection _) (isStarProjection_starProjection _), ← star_inj, (isStarProjection_starProjection _).isSelfAdjoint, star_eq_adjoint, adjoint_comp] simp_rw [← star_eq_adjoint, (isStarProjection_starProjection _).isSelfAdjoint.star_eq] rw [← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] - · have : ∀ p : E →L[ℂ] E, LinearMap.range p.toLinearMap = LinearMap.range p := fun p => rfl + · have {p : E →L[𝕜] E} : LinearMap.range p.toLinearMap = LinearMap.range p := rfl simp_rw [this, Submodule.range_starProjection] · exact congr(LinearMapClass.linearMap $((isStarProjection_starProjection V).isIdempotentElem.eq)) From 96e458708cb162b867c5f403f5b8b6d663300e94 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 28 Jul 2025 20:40:56 +0000 Subject: [PATCH 28/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index cbfc01933b122f..9f77ed6e3c59db 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -449,13 +449,13 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection ≤ V.starProjection ↔ U ≤ V := by - rw [IsStarProjection.le_iff_comp_eq_left (isStarProjection_starProjection _) - (isStarProjection_starProjection _), ← star_inj, - (isStarProjection_starProjection _).isSelfAdjoint, star_eq_adjoint, adjoint_comp] - simp_rw [← star_eq_adjoint, (isStarProjection_starProjection _).isSelfAdjoint.star_eq] + rw [isStarProjection_starProjection.le_iff_comp_eq_left + isStarProjection_starProjection, ← star_inj, + isStarProjection_starProjection.isSelfAdjoint, star_eq_adjoint, adjoint_comp] + simp_rw [← star_eq_adjoint, isStarProjection_starProjection.isSelfAdjoint.star_eq] rw [← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] · have {p : E →L[𝕜] E} : LinearMap.range p.toLinearMap = LinearMap.range p := rfl simp_rw [this, Submodule.range_starProjection] - · exact congr(LinearMapClass.linearMap $((isStarProjection_starProjection V).isIdempotentElem.eq)) + · exact congr(LinearMapClass.linearMap $(isStarProjection_starProjection.isIdempotentElem.eq)) end ContinuousLinearMap From d10d4c384f670fd9fe425c216142b07360ef9bf2 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 28 Jul 2025 20:46:04 +0000 Subject: [PATCH 29/86] move stuff around --- .../Analysis/InnerProductSpace/Adjoint.lean | 38 +++++++++++++++++++ .../Analysis/InnerProductSpace/Positive.lean | 37 ------------------ 2 files changed, 38 insertions(+), 37 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index c018afa0497681..2a1b2a65d22709 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -399,6 +399,44 @@ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E simpa [p.orthogonal_range, hp.isSelfAdjoint.isSymmetric] using congr($(hp.isIdempotentElem.mul_one_sub_self) x) +theorem ContinuousLinearMap.IsStarProjection.norm_apply_le {T : E →L[𝕜] E} [CompleteSpace E] + (hT : IsStarProjection T) (v : E) : + ‖T v‖ ≤ ‖v‖ := by + obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT + exact hht ▸ Submodule.norm_starProjection_apply_le _ _ + +theorem ContinuousLinearMap.IsStarProjection.reApplyInnerSelf_eq {T : E →L[𝕜] E} [CompleteSpace E] + (hT : IsStarProjection T) (v : E) : + T.reApplyInnerSelf v = ‖T v‖ ^ 2 := by + obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT + calc T.reApplyInnerSelf v = re (inner 𝕜 (T v) v) := rfl + _ = re (inner 𝕜 (T v) (T v)) + re (inner 𝕜 (T v) ((1 - T) v)) := by + simp [← map_add, ← inner_add_right] + _ = re (inner 𝕜 (T v) (T v)) + 0 := ?_ + _ = ‖T v‖ ^ 2 := by simp; exact inner_self_eq_norm_sq _ + congr + rw [hht, ← Submodule.starProjection_orthogonal', + Submodule.inner_starProjection_left_eq_right, + (Submodule.starProjection_apply_eq_zero_iff _).mpr (by simp)] + simp + +open ContinuousLinearMap in +theorem ContinuousLinearMap.IsStarProjection.apply_norm_eq_iff {T : E →L[𝕜] E} [CompleteSpace E] + (hT : IsStarProjection T) {v : E} : + ‖T v‖ = ‖v‖ ↔ v ∈ LinearMap.range T := by + refine ⟨fun h => ?_, fun h => congr(‖$((LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mp h)‖)⟩ + have := calc 0 = ‖v‖ ^ 2 - ‖T v‖ ^ 2 := by simp [h] + _ = ‖T v + (1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by simp + _ = ‖T v‖ ^ 2 + ‖(1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by + congr + rw [norm_add_sq (𝕜 := 𝕜), ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] + simp [← mul_apply, hT.isIdempotentElem.eq] + _ = ‖(1 - T) v‖ ^ 2 := by simp + rw [eq_comm, sq_eq_zero_iff, norm_eq_zero, sub_apply, one_apply, sub_eq_zero, eq_comm] at this + exact (LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mpr this + namespace LinearMap variable [CompleteSpace E] diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 9f77ed6e3c59db..44399ae8afcd7c 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -385,44 +385,7 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : tfae_have 2 ↔ 4 := hp.isSelfAdjoint_iff_orthogonal_range tfae_finish ---move to `Projection` -theorem IsStarProjection.norm_apply_le {T : E →L[𝕜] E} (hT : IsStarProjection T) (v : E) : - ‖T v‖ ≤ ‖v‖ := by - obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT - exact hht ▸ Submodule.norm_starProjection_apply_le _ _ - -open RCLike ---move to `Projection` -theorem IsStarProjection.reApplyInnerSelf_eq {T : E →L[𝕜] E} (hT : IsStarProjection T) (v : E) : - T.reApplyInnerSelf v = ‖T v‖ ^ 2 := by - obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT - calc T.reApplyInnerSelf v = re (inner 𝕜 (T v) v) := rfl - _ = re (inner 𝕜 (T v) (T v)) + re (inner 𝕜 (T v) ((1 - T) v)) := by - simp [← map_add, ← inner_add_right] - _ = re (inner 𝕜 (T v) (T v)) + 0 := ?_ - _ = ‖T v‖ ^ 2 := by simp; exact inner_self_eq_norm_sq _ - congr - rw [hht, ← Submodule.starProjection_orthogonal', - Submodule.inner_starProjection_left_eq_right, - (Submodule.starProjection_apply_eq_zero_iff _).mpr (by simp)] - simp - open ContinuousLinearMap --- move to `Projection` -theorem IsStarProjection.apply_norm_eq_iff {T : E →L[𝕜] E} (hT : IsStarProjection T) {v : E} : - ‖T v‖ = ‖v‖ ↔ v ∈ LinearMap.range T := by - refine ⟨fun h => ?_, fun h => congr(‖$((LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mp h)‖)⟩ - have := calc 0 = ‖v‖ ^ 2 - ‖T v‖ ^ 2 := by simp [h] - _ = ‖T v + (1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by simp - _ = ‖T v‖ ^ 2 + ‖(1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by - congr - rw [norm_add_sq (𝕜 := 𝕜), ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] - simp [← mul_apply, hT.isIdempotentElem.eq] - _ = ‖(1 - T) v‖ ^ 2 := by simp - rw [eq_comm, sq_eq_zero_iff, norm_eq_zero, sub_apply, one_apply, sub_eq_zero, eq_comm] at this - exact (LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mpr this /-- For star projection operators `p,q`, we have `p ≤ q` iff `p ∘ q = p`. -/ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} From cdfacb966c5a1d8a64d7caee0dd5e7a140a6d9d2 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 28 Jul 2025 20:47:14 +0000 Subject: [PATCH 30/86] remove open --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 44399ae8afcd7c..f1454b05245dfc 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -385,8 +385,6 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : tfae_have 2 ↔ 4 := hp.isSelfAdjoint_iff_orthogonal_range tfae_finish -open ContinuousLinearMap - /-- For star projection operators `p,q`, we have `p ≤ q` iff `p ∘ q = p`. -/ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ p ∘L q = p := by From eb3d5c0770dbe3a7dc0051366ba1063719a70613 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 28 Jul 2025 20:53:50 +0000 Subject: [PATCH 31/86] remove --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 15 --------------- Mathlib/Analysis/InnerProductSpace/Positive.lean | 8 +++++++- 2 files changed, 7 insertions(+), 16 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 2a1b2a65d22709..123d950ff03ff0 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -405,21 +405,6 @@ theorem ContinuousLinearMap.IsStarProjection.norm_apply_le {T : E →L[𝕜] E} obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT exact hht ▸ Submodule.norm_starProjection_apply_le _ _ -theorem ContinuousLinearMap.IsStarProjection.reApplyInnerSelf_eq {T : E →L[𝕜] E} [CompleteSpace E] - (hT : IsStarProjection T) (v : E) : - T.reApplyInnerSelf v = ‖T v‖ ^ 2 := by - obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT - calc T.reApplyInnerSelf v = re (inner 𝕜 (T v) v) := rfl - _ = re (inner 𝕜 (T v) (T v)) + re (inner 𝕜 (T v) ((1 - T) v)) := by - simp [← map_add, ← inner_add_right] - _ = re (inner 𝕜 (T v) (T v)) + 0 := ?_ - _ = ‖T v‖ ^ 2 := by simp; exact inner_self_eq_norm_sq _ - congr - rw [hht, ← Submodule.starProjection_orthogonal', - Submodule.inner_starProjection_left_eq_right, - (Submodule.starProjection_apply_eq_zero_iff _).mpr (by simp)] - simp - open ContinuousLinearMap in theorem ContinuousLinearMap.IsStarProjection.apply_norm_eq_iff {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsStarProjection T) {v : E} : diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index f1454b05245dfc..7f5078a8936bd1 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -401,8 +401,14 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} have {T : E →L[𝕜] E} (hT : IsStarProjection T) : a ∈ LinearMap.range T ↔ T a = a := (LinearMap.IsIdempotentElem.mem_range_iff congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)) + have hh {T : E →L[𝕜] E} (hT : IsStarProjection T) : + T.reApplyInnerSelf a = ‖T a‖ ^ 2 := by + rw [reApplyInnerSelf_apply] + nth_rw 1 [← hT.isIdempotentElem] + rw [mul_apply, ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] + exact inner_self_eq_norm_sq _ simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, - ← reApplyInnerSelf_apply, hq.reApplyInnerSelf_eq, hp.reApplyInnerSelf_eq, (this hp).mp ha, + ← reApplyInnerSelf_apply, hh hq, hh hp, (this hp).mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 exact hq.apply_norm_eq_iff.mp (le_antisymm (hq.norm_apply_le a) h2) From 21b524f69ecd5b158ad99de4cb0562d28e532e12 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 28 Jul 2025 21:00:17 +0000 Subject: [PATCH 32/86] update --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 13 ++++++------- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 123d950ff03ff0..09e1d0e329f6ec 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -405,12 +405,11 @@ theorem ContinuousLinearMap.IsStarProjection.norm_apply_le {T : E →L[𝕜] E} obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT exact hht ▸ Submodule.norm_starProjection_apply_le _ _ -open ContinuousLinearMap in -theorem ContinuousLinearMap.IsStarProjection.apply_norm_eq_iff {T : E →L[𝕜] E} [CompleteSpace E] +theorem ContinuousLinearMap.IsStarProjection.mem_range_iff_norm {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsStarProjection T) {v : E} : - ‖T v‖ = ‖v‖ ↔ v ∈ LinearMap.range T := by - refine ⟨fun h => ?_, fun h => congr(‖$((LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mp h)‖)⟩ + v ∈ LinearMap.range T ↔ ‖T v‖ = ‖v‖ := by + refine ⟨fun h => congr(‖$(LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq) |>.mp h)‖), fun h => ?_⟩ have := calc 0 = ‖v‖ ^ 2 - ‖T v‖ ^ 2 := by simp [h] _ = ‖T v + (1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by simp _ = ‖T v‖ ^ 2 + ‖(1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by @@ -419,8 +418,8 @@ theorem ContinuousLinearMap.IsStarProjection.apply_norm_eq_iff {T : E →L[𝕜] simp [← mul_apply, hT.isIdempotentElem.eq] _ = ‖(1 - T) v‖ ^ 2 := by simp rw [eq_comm, sq_eq_zero_iff, norm_eq_zero, sub_apply, one_apply, sub_eq_zero, eq_comm] at this - exact (LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)).mpr this + exact LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq) |>.mpr this namespace LinearMap diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 7f5078a8936bd1..7b62fb3eb1c755 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -410,7 +410,7 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, ← reApplyInnerSelf_apply, hh hq, hh hp, (this hp).mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 - exact hq.apply_norm_eq_iff.mp (le_antisymm (hq.norm_apply_le a) h2) + exact hq.mem_range_iff_norm.mpr (le_antisymm (hq.norm_apply_le a) h2) /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) From 2b99c5fa7f5789f9d452a5f221a20b06b6227aa5 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Mon, 28 Jul 2025 21:34:09 +0000 Subject: [PATCH 33/86] Update Adjoint.lean --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 09e1d0e329f6ec..d381c6b0f59fe3 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -399,12 +399,6 @@ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E simpa [p.orthogonal_range, hp.isSelfAdjoint.isSymmetric] using congr($(hp.isIdempotentElem.mul_one_sub_self) x) -theorem ContinuousLinearMap.IsStarProjection.norm_apply_le {T : E →L[𝕜] E} [CompleteSpace E] - (hT : IsStarProjection T) (v : E) : - ‖T v‖ ≤ ‖v‖ := by - obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hT - exact hht ▸ Submodule.norm_starProjection_apply_le _ _ - theorem ContinuousLinearMap.IsStarProjection.mem_range_iff_norm {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsStarProjection T) {v : E} : v ∈ LinearMap.range T ↔ ‖T v‖ = ‖v‖ := by From cca2075936d3f890cc95cc385f00defbcd35497c Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Mon, 28 Jul 2025 21:34:38 +0000 Subject: [PATCH 34/86] Update Positive.lean --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 7b62fb3eb1c755..75f56342a2b643 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -410,7 +410,9 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, ← reApplyInnerSelf_apply, hh hq, hh hp, (this hp).mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 - exact hq.mem_range_iff_norm.mpr (le_antisymm (hq.norm_apply_le a) h2) + obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hq + exact hq.mem_range_iff_norm.mpr + (le_antisymm (hht ▸ Submodule.norm_starProjection_apply_le _ _) h2) /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) From 0d11f99b9fa90c5c2e1999eadc0f4682700ca4a0 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Mon, 28 Jul 2025 21:54:50 +0000 Subject: [PATCH 35/86] Update StarProjection.lean --- Mathlib/Algebra/Star/StarProjection.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index aa6cf5d30363ae..68008a982ddce6 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -119,12 +119,9 @@ theorem sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] theorem sub_iff_mul_eq_right [Ring R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ q * p = p := by - rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem] - simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true] - nth_rw 1 [← hp.isSelfAdjoint] - nth_rw 1 [← hq.isSelfAdjoint] - rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm] - simp_rw [and_self] + rw [← star_inj] + simp [star_mul, hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq, + sub_iff_mul_eq_left hp hq] theorem add_sub_mul_of_commute [Ring R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) : From b02edbdd9b3d89fd56e868f897ba63e51fde221b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 00:46:10 +0000 Subject: [PATCH 36/86] mem_range_iff_norm --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index e43ffd67845276..a01bf66ff36832 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -393,6 +393,22 @@ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E simpa [p.orthogonal_range, hp.isSelfAdjoint.isSymmetric] using congr($(hp.isIdempotentElem.mul_one_sub_self) x) +theorem ContinuousLinearMap.IsStarProjection.mem_range_iff_norm {T : E →L[𝕜] E} [CompleteSpace E] + (hT : IsStarProjection T) {v : E} : + v ∈ LinearMap.range T ↔ ‖T v‖ = ‖v‖ := by + refine ⟨fun h => congr(‖$(LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq) |>.mp h)‖), fun h => ?_⟩ + have := calc 0 = ‖v‖ ^ 2 - ‖T v‖ ^ 2 := by simp [h] + _ = ‖T v + (1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by simp + _ = ‖T v‖ ^ 2 + ‖(1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by + congr + rw [norm_add_sq (𝕜 := 𝕜), ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] + simp [← mul_apply, hT.isIdempotentElem.eq] + _ = ‖(1 - T) v‖ ^ 2 := by simp + rw [eq_comm, sq_eq_zero_iff, norm_eq_zero, sub_apply, one_apply, sub_eq_zero, eq_comm] at this + exact LinearMap.IsIdempotentElem.mem_range_iff + congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq) |>.mpr this + namespace LinearMap variable [CompleteSpace E] From 6f4460d38bebb207ecec3ea57c859711397938ec Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 12:44:44 +0000 Subject: [PATCH 37/86] remove and add suggestion --- .../Analysis/InnerProductSpace/Adjoint.lean | 20 +++++-------------- .../InnerProductSpace/Projection.lean | 7 +++++++ 2 files changed, 12 insertions(+), 15 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index a01bf66ff36832..15959d63939271 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -393,21 +393,11 @@ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E simpa [p.orthogonal_range, hp.isSelfAdjoint.isSymmetric] using congr($(hp.isIdempotentElem.mul_one_sub_self) x) -theorem ContinuousLinearMap.IsStarProjection.mem_range_iff_norm {T : E →L[𝕜] E} [CompleteSpace E] - (hT : IsStarProjection T) {v : E} : - v ∈ LinearMap.range T ↔ ‖T v‖ = ‖v‖ := by - refine ⟨fun h => congr(‖$(LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq) |>.mp h)‖), fun h => ?_⟩ - have := calc 0 = ‖v‖ ^ 2 - ‖T v‖ ^ 2 := by simp [h] - _ = ‖T v + (1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by simp - _ = ‖T v‖ ^ 2 + ‖(1 - T) v‖ ^ 2 - ‖T v‖ ^ 2 := by - congr - rw [norm_add_sq (𝕜 := 𝕜), ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] - simp [← mul_apply, hT.isIdempotentElem.eq] - _ = ‖(1 - T) v‖ ^ 2 := by simp - rw [eq_comm, sq_eq_zero_iff, norm_eq_zero, sub_apply, one_apply, sub_eq_zero, eq_comm] at this - exact LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq) |>.mpr this +lemma isStarProjection_iff_eq_starProjection [CompleteSpace E] {p : E →L[𝕜] E} : + IsStarProjection p + ↔ ∃ (K : Submodule 𝕜 E) (_ : K.HasOrthogonalProjection), p = K.starProjection := + ⟨fun h ↦ ⟨LinearMap.range p, isStarProjection_iff_eq_starProjection_range.mp h⟩, + by rintro ⟨_, _, rfl⟩; simp⟩ namespace LinearMap diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index be90fce452cd1f..86d3ca70d5e201 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1283,6 +1283,13 @@ theorem norm_sq_eq_add_norm_sq_starProjection (x : E) (S : Submodule 𝕜 E) ‖x‖ ^ 2 = ‖S.starProjection x‖ ^ 2 + ‖Sᗮ.starProjection x‖ ^ 2 := norm_sq_eq_add_norm_sq_projection x S +theorem mem_iff_norm_starProjection (U : Submodule 𝕜 E) + [U.HasOrthogonalProjection] (v : E) : + v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖ := by + refine ⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩ + simpa [h, sub_eq_zero, eq_comm (a := v), Submodule.starProjection_eq_self_iff] using + U.norm_sq_eq_add_norm_sq_starProjection v + /-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal complement sum to the identity. -/ theorem id_eq_sum_starProjection_self_orthogonalComplement [K.HasOrthogonalProjection] : From 2fe1328ed24cac60a11c588c45800af72173e5a3 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 12:46:17 +0000 Subject: [PATCH 38/86] remove submodule. --- Mathlib/Analysis/InnerProductSpace/Projection.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 86d3ca70d5e201..0e28bd8e80e93a 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1287,7 +1287,7 @@ theorem mem_iff_norm_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (v : E) : v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖ := by refine ⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩ - simpa [h, sub_eq_zero, eq_comm (a := v), Submodule.starProjection_eq_self_iff] using + simpa [h, sub_eq_zero, eq_comm (a := v), starProjection_eq_self_iff] using U.norm_sq_eq_add_norm_sq_starProjection v /-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal From 34f984ba0d97b66db67062ea05f1b33839b28a67 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Tue, 29 Jul 2025 12:56:50 +0000 Subject: [PATCH 39/86] Apply suggestions from code review Co-authored-by: Jireh Loreaux --- Mathlib/Algebra/Ring/Idempotent.lean | 2 +- Mathlib/Algebra/Star/StarProjection.lean | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index af70d6dab28196..9ff4d743d2f73a 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -86,7 +86,7 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : end CommRing /-- `b - a` is idempotent when `a * b = a` and `b * a = a`. -/ -lemma sub [NonAssocRing R] {a b : R} (ha : IsIdempotentElem a) +lemma sub [NonUnitalNonAssocRing R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) (hab : a * b = a) (hba : b * a = a) : IsIdempotentElem (b - a) := by simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero] diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index 68008a982ddce6..9c70c9d126ed91 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -90,7 +90,7 @@ theorem mul [NonUnitalSemiring R] [StarRing R] isIdempotentElem := hp.isIdempotentElem.mul_of_commute hpq hq.isIdempotentElem /-- `q - p` is a star projection when `p * q = p`. -/ -theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] +theorem sub_of_mul_eq_left [NonUnitalNonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) : IsStarProjection (q - p) where isSelfAdjoint := hq.isSelfAdjoint.sub hp.isSelfAdjoint @@ -99,13 +99,13 @@ theorem sub_of_mul_eq_left [NonAssocRing R] [StarRing R] (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))) /-- `q - p` is a star projection when `q * p = p`. -/ -theorem sub_of_mul_eq_right [NonAssocRing R] [StarRing R] +theorem sub_of_mul_eq_right [NonUnitalNonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hqp : q * p = p) : IsStarProjection (q - p) := hp.sub_of_mul_eq_left hq (by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))) /-- `q - p` is a star projection iff `p * q = p`. -/ -theorem sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] +theorem sub_iff_mul_eq_left [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ p * q = p := by rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem] @@ -116,7 +116,7 @@ theorem sub_iff_mul_eq_left [Ring R] [StarRing R] [IsAddTorsionFree R] simp_rw [and_self] /-- `q - p` is a star projection iff `q * p = p`. -/ -theorem sub_iff_mul_eq_right [Ring R] [StarRing R] [IsAddTorsionFree R] +theorem sub_iff_mul_eq_right [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (q - p) ↔ q * p = p := by rw [← star_inj] From af27f0882feb3ea5cc6ebd645cbd5bc4814af236 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 13:12:14 +0000 Subject: [PATCH 40/86] add suggestion --- Mathlib/Algebra/Ring/Idempotent.lean | 53 +++++++++++++++------------- 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 9ff4d743d2f73a..53aa96a6c18eb7 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Christopher Hoskin -/ import Mathlib.Algebra.GroupWithZero.Idempotent -import Mathlib.Algebra.Ring.Defs +import Mathlib.Algebra.Ring.Commute import Mathlib.Order.Notation import Mathlib.Tactic.Convert +import Mathlib.Tactic.NoncommRing import Mathlib.Algebra.Group.Torsion /-! @@ -85,30 +86,6 @@ lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : end CommRing -/-- `b - a` is idempotent when `a * b = a` and `b * a = a`. -/ -lemma sub [NonUnitalNonAssocRing R] {a b : R} (ha : IsIdempotentElem a) - (hb : IsIdempotentElem b) (hab : a * b = a) (hba : b * a = a) : IsIdempotentElem (b - a) := by - simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero] - -lemma commutes_of_isIdempotentElem_sub [Ring R] [IsAddTorsionFree R] {p q : R} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hqp : IsIdempotentElem (q - p)) : - p * q = p ∧ q * p = p := by - simp_rw [IsIdempotentElem, mul_sub, sub_mul, - hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp - have hpq : p * q = q * p := by - have h1 := congr_arg (q * ·) hqp - have h2 := congr_arg (· * q) hqp - simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1 - simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2 - exact h2.symm.trans h1 - rw [hpq, sub_eq_iff_eq_add, ← two_nsmul, ← two_nsmul, nsmul_right_inj (by simp)] at hqp - rw [hpq, hqp, and_self] - -theorem sub_iff [Ring R] [IsAddTorsionFree R] {p q : R} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : - IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := - ⟨commutes_of_isIdempotentElem_sub hp hq, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩ - /-- `a + b` is idempotent when `a` and `b` anti-commute. -/ theorem add [NonUnitalNonAssocSemiring R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) @@ -116,6 +93,21 @@ theorem add [NonUnitalNonAssocSemiring R] simp_rw [IsIdempotentElem, mul_add, add_mul, ha.eq, hb.eq, add_add_add_comm, ← add_assoc, add_assoc a, hab, zero_add] +/-- `a + b` is idempotent if and only if `a` and `b` anti-commute. -/ +theorem add_iff [NonUnitalNonAssocSemiring R] [IsCancelAdd R] + {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : + IsIdempotentElem (a + b) ↔ a * b + b * a = 0 := by + refine ⟨fun h ↦ ?_, ha.add hb⟩ + have := by simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq + rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a), + ← add_assoc, add_add_add_comm] + simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq + +/-- `b - a` is idempotent when `a * b = a` and `b * a = a`. -/ +lemma sub [NonUnitalNonAssocRing R] {a b : R} (ha : IsIdempotentElem a) + (hb : IsIdempotentElem b) (hab : a * b = a) (hba : b * a = a) : IsIdempotentElem (b - a) := by + simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero] + /-- If idempotent `a` and element `b` anti-commute, then their product is zero. -/ theorem mul_eq_zero_of_anticommute {a b : R} [NonUnitalSemiring R] [IsAddTorsionFree R] (ha : IsIdempotentElem a) (hab : a * b + b * a = 0) : a * b = 0 := by @@ -135,4 +127,15 @@ lemma commute_of_anticommute {a b : R} [NonUnitalSemiring R] [IsAddTorsionFree R rw [this, zero_add] at hab rw [Commute, SemiconjBy, hab, this] +theorem sub_iff [NonUnitalRing R] [IsAddTorsionFree R] {p q : R} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : + IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := by + refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩ + have h := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq) + have hpq := by simpa using hp.commute_of_anticommute h |>.add_right <| .refl p + rw [hpq.eq, and_self, ← nsmul_right_inj two_ne_zero, ← zero_add (2 • p)] + convert congrArg (· + 2 • p) h using 1 + simp [sub_mul, mul_sub, hp.eq, hpq.eq] + noncomm_ring + end IsIdempotentElem From 78632d8d959587448f0c6302ae298f862160e742 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 13:20:53 +0000 Subject: [PATCH 41/86] suggestions --- Mathlib/Algebra/Group/Idempotent.lean | 8 ++++++++ Mathlib/Algebra/Order/Star/Basic.lean | 13 +++++++++++-- Mathlib/Algebra/Ring/Idempotent.lean | 15 ++++++++------- Mathlib/Algebra/Star/StarProjection.lean | 2 +- 4 files changed, 28 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Group/Idempotent.lean b/Mathlib/Algebra/Group/Idempotent.lean index f079b936b38814..c3412cd6d36e20 100644 --- a/Mathlib/Algebra/Group/Idempotent.lean +++ b/Mathlib/Algebra/Group/Idempotent.lean @@ -106,4 +106,12 @@ lemma map {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M} (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e) := by rw [IsIdempotentElem, ← map_mul, he.eq] +lemma mul_mul_self {M : Type*} [Semigroup M] {x : M} + (hx : IsIdempotentElem x) (y : M) : y * x * x = y * x := + mul_assoc y x x ▸ congrArg (y * ·) hx.eq + +lemma mul_self_mul {M : Type*} [Semigroup M] {x : M} + (hx : IsIdempotentElem x) (y : M) : x * (x * y) = x * y := + mul_assoc x x y ▸ congrArg (· * y) hx.eq + end IsIdempotentElem diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean index c86ac94ae2bf74..47dc1d7db6737c 100644 --- a/Mathlib/Algebra/Order/Star/Basic.lean +++ b/Mathlib/Algebra/Order/Star/Basic.lean @@ -399,6 +399,8 @@ instance Nat.instStarOrderedRing : StarOrderedRing ℕ where simp [this, le_iff_exists_add] namespace IsStarProjection + +section Ring variable [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p : R} theorem one_sub_nonneg (hp : IsStarProjection p) : 0 ≤ 1 - p := hp.one_sub.nonneg @@ -409,12 +411,19 @@ theorem le_one (hp : IsStarProjection p) : p ≤ 1 := sub_nonneg.mp hp.one_sub_n theorem mem_Icc (hp : IsStarProjection p) : p ∈ Set.Icc (0 : R) 1 := by simp only [Set.mem_Icc, hp.nonneg, hp.le_one, and_self] +end Ring + +section NonUnitalRing +variable [NonUnitalRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {p q : R} + /-- A star projection `p` is less than or equal to a star projection `q` when `p * q = p`. -/ -theorem le_of_mul_eq_left {q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) +theorem le_of_mul_eq_left (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) : p ≤ q := sub_nonneg.mp (hp.sub_of_mul_eq_left hq hpq).nonneg /-- A star projection `p` is less than or equal to a star projection `q` when `q * p = p`. -/ -theorem le_of_mul_eq_right {q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) +theorem le_of_mul_eq_right (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : q * p = p) : p ≤ q := sub_nonneg.mp (hp.sub_of_mul_eq_right hq hpq).nonneg +end NonUnitalRing + end IsStarProjection diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 53aa96a6c18eb7..96f15af2eec2ae 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -67,16 +67,17 @@ lemma of_mul_add (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ Is end Semiring -section Ring -variable [Ring R] {a b : R} +section NonUnitalRing +variable [NonUnitalRing R] {a b : R} -lemma add_sub_mul_of_commute (h : Commute a b) (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) : +lemma add_sub_mul_of_commute (h : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b) := by - convert (hp.one_sub.mul_of_commute ?_ hq.one_sub).one_sub using 1 - · simp_rw [sub_mul, mul_sub, one_mul, mul_one, sub_sub, sub_sub_cancel, add_sub, add_comm] - · simp_rw [commute_iff_eq, sub_mul, mul_sub, one_mul, mul_one, sub_sub, add_sub, add_comm, h.eq] + rw [IsIdempotentElem] + simp only [h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq, mul_assoc, add_sub_cancel_right, + hb.eq, hb.mul_self_mul, add_sub_cancel_left, sub_right_inj] + rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right] -end Ring +end NonUnitalRing section CommRing variable [CommRing R] {a b : R} diff --git a/Mathlib/Algebra/Star/StarProjection.lean b/Mathlib/Algebra/Star/StarProjection.lean index 9c70c9d126ed91..74fbaf71c451ba 100644 --- a/Mathlib/Algebra/Star/StarProjection.lean +++ b/Mathlib/Algebra/Star/StarProjection.lean @@ -123,7 +123,7 @@ theorem sub_iff_mul_eq_right [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] simp [star_mul, hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq, sub_iff_mul_eq_left hp hq] -theorem add_sub_mul_of_commute [Ring R] [StarRing R] +theorem add_sub_mul_of_commute [NonUnitalRing R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) : IsStarProjection (p + q - p * q) where isIdempotentElem := hp.isIdempotentElem.add_sub_mul_of_commute hpq hq.isIdempotentElem From 633c07866ef9e91d25294dea3415df9f6641efd4 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 13:23:08 +0000 Subject: [PATCH 42/86] fix --- Mathlib/Algebra/Ring/Idempotent.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 96f15af2eec2ae..34b3d1ea7591fd 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -72,9 +72,8 @@ variable [NonUnitalRing R] {a b : R} lemma add_sub_mul_of_commute (h : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a + b - a * b) := by - rw [IsIdempotentElem] - simp only [h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq, mul_assoc, add_sub_cancel_right, - hb.eq, hb.mul_self_mul, add_sub_cancel_left, sub_right_inj] + simp only [IsIdempotentElem, h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq, + mul_assoc, add_sub_cancel_right, hb.eq, hb.mul_self_mul, add_sub_cancel_left, sub_right_inj] rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right] end NonUnitalRing From 5a70cfdcc157561018416de635a75b3b898b726d Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 14:00:58 +0000 Subject: [PATCH 43/86] definition --- .../Analysis/InnerProductSpace/Symmetric.lean | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 102b4e8831bdcc..003ffad49bf21f 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -154,6 +154,18 @@ theorem IsSymmetric.coe_re_inner_self_apply {T : E →ₗ[𝕜] E} (hT : T.IsSym re ⟪x, T x⟫ = ⟪x, T x⟫ := by simp [← hT x x, hT] +/-- A symmetric projection is a symmetric idempotent. -/ +def IsSymmetricProjection (T : E →ₗ[𝕜] E) : Prop := + IsIdempotentElem T ∧ T.IsSymmetric + +theorem IsSymmetricProjection.isIdempotentElem {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : + IsIdempotentElem T := + hT.1 + +theorem IsSymmetricProjection.isSymmetric {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : + T.IsSymmetric := + hT.2 + section Complex variable {V : Type*} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V] @@ -265,6 +277,15 @@ theorem _root_.Submodule.IsCompl.projection_isSymmetric_iff rw [isOrtho_iff_inner_eq] at h simp [inner_add_right, inner_add_left, h, inner_eq_zero_symm] +open Submodule in +theorem _root_.Submodule.IsCompl.projection_isSymmetricProjection_iff + {U V : Submodule 𝕜 E} (hUV : IsCompl U V) : + hUV.projection.IsSymmetricProjection ↔ U ⟂ V := by + simp [IsSymmetricProjection, hUV.projection_isSymmetric_iff, hUV.projection_isIdempotentElem] + +alias ⟨_, _root_.Submodule.IsCompl.projection_isSymmetricProjection_of_isOrtho⟩ := + _root_.Submodule.IsCompl.projection_isSymmetricProjection_iff + open Submodule LinearMap in /-- An idempotent operator is symmetric if and only if its range is pairwise orthogonal to its kernel. -/ From 7b10b3440dcca55d77fd40739b7d46fbfe61f57b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 15:59:27 +0000 Subject: [PATCH 44/86] add stuff --- .../Analysis/InnerProductSpace/Adjoint.lean | 22 +++++--------- .../InnerProductSpace/Projection.lean | 29 +++++++++++++++++++ .../Analysis/InnerProductSpace/Symmetric.lean | 6 ++++ 3 files changed, 43 insertions(+), 14 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index e43ffd67845276..206568c3438031 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -353,12 +353,6 @@ theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal : rw [isStarProjection_iff, and_congr_right_iff] exact fun h => IsIdempotentElem.isSelfAdjoint_iff_isStarNormal h -omit [CompleteSpace E] in -/-- An idempotent operator `T` is symmetric iff `(range T)ᗮ = ker T`. -/ -theorem IsIdempotentElem.isSymmetric_iff_orthogonal_range (h : IsIdempotentElem T) : - T.IsSymmetric ↔ (LinearMap.range T)ᗮ = LinearMap.ker T := - LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range congr(LinearMapClass.linearMap $h.eq) - open ContinuousLinearMap in /-- Star projection operators are equal iff their range are. -/ theorem IsStarProjection.ext_iff {S : E →L[𝕜] E} @@ -372,6 +366,11 @@ theorem IsStarProjection.ext_iff {S : E →L[𝕜] E} alias ⟨_, IsStarProjection.ext⟩ := IsStarProjection.ext_iff +theorem isStarProjection_iff_isSymmetricProjection : + IsStarProjection T ↔ T.IsSymmetricProjection := by + simp [isStarProjection_iff, LinearMap.IsSymmetricProjection, + isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def] + end ContinuousLinearMap /-- `U.starProjection` is a star projection. -/ @@ -384,14 +383,9 @@ open ContinuousLinearMap in /-- An operator is a star projection if and only if it is an orthogonal projection. -/ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E →L[𝕜] E} : IsStarProjection p ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), - p = (LinearMap.range p).starProjection := by - refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isStarProjection_starProjection⟩ - have := IsIdempotentElem.hasOrthogonalProjection_range hp.isIdempotentElem - refine ⟨this, Eq.symm ?_⟩ - ext x - refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_ - simpa [p.orthogonal_range, hp.isSelfAdjoint.isSymmetric] - using congr($(hp.isIdempotentElem.mul_one_sub_self) x) + p = (LinearMap.range p).starProjection := + p.isStarProjection_iff_isSymmetricProjection.symm.eq ▸ + isSymmetricProjection_iff_eq_starProjection_range namespace LinearMap diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index be90fce452cd1f..a8b65c97d11410 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1145,6 +1145,13 @@ theorem topologicalClosure_eq_top_iff [CompleteSpace E] : end Submodule +open LinearMap in +theorem LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range + {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : + (range p).HasOrthogonalProjection := ⟨fun v => ⟨p v, by + simp [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric, + ← Module.End.mul_apply, hp.isIdempotentElem.eq]⟩⟩ + open ContinuousLinearMap in theorem ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : (LinearMap.range p).HasOrthogonalProjection := @@ -1328,6 +1335,28 @@ theorem starProjection_isSymmetric [K.HasOrthogonalProjection] : @[deprecated (since := "2025-07-07")] alias orthogonalProjection_isSymmetric := starProjection_isSymmetric +open ContinuousLinearMap in +/-- `U.starProjection` is a symmetric projection. -/ +theorem isSymmetricProjection_starProjection {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : + U.starProjection.IsSymmetricProjection := + ⟨by simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] + using U.isIdempotentElem_starProjection, U.starProjection_isSymmetric⟩ + +open ContinuousLinearMap in +/-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ +theorem isSymmetricProjection_iff_eq_starProjection_range {p : E →L[𝕜] E} : + p.IsSymmetricProjection ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), + p = (LinearMap.range p).starProjection := by + refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection⟩ + have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range + refine ⟨this, Eq.symm ?_⟩ + ext x + refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_ + rw [(IsIdempotentElem.isSymmetric_iff_orthogonal_range _).mp hp.isSymmetric] + · simpa using congr($hp.isIdempotentElem.mul_one_sub_self x) + · simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] + using hp.isIdempotentElem.eq + theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ := by refine ⟨fun h w hw => ?_, fun hv => ?_⟩ diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 003ffad49bf21f..4e0907bd318451 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -308,4 +308,10 @@ theorem IsIdempotentElem.isSymmetric_iff_orthogonal_range {T : E →ₗ[𝕜] E} end LinearMap +/-- An idempotent operator `T` is symmetric iff `(range T)ᗮ = ker T`. -/ +theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range + {T : E →L[𝕜] E} (h : IsIdempotentElem T) : + T.IsSymmetric ↔ (LinearMap.range T)ᗮ = LinearMap.ker T := + LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range congr(LinearMapClass.linearMap $h.eq) + end Normed From 198b010d3354cdfe7c24512e860f60dbcb9a6238 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 16:13:25 +0000 Subject: [PATCH 45/86] ext --- .../Analysis/InnerProductSpace/Adjoint.lean | 20 +++++++++---------- .../InnerProductSpace/Projection.lean | 20 ++++++++++++++++--- 2 files changed, 26 insertions(+), 14 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 206568c3438031..b2d9e59d4f377f 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -353,24 +353,22 @@ theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal : rw [isStarProjection_iff, and_congr_right_iff] exact fun h => IsIdempotentElem.isSelfAdjoint_iff_isStarNormal h +theorem isStarProjection_iff_isSymmetricProjection : + IsStarProjection T ↔ T.IsSymmetricProjection := by + simp [isStarProjection_iff, LinearMap.IsSymmetricProjection, + isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def] + open ContinuousLinearMap in /-- Star projection operators are equal iff their range are. -/ theorem IsStarProjection.ext_iff {S : E →L[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) : S = T ↔ LinearMap.range S = LinearMap.range T := by - refine ⟨fun h => h ▸ rfl, fun h => ?_⟩ - rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem, - ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSelfAdjoint.isSymmetric, - ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSelfAdjoint.isSymmetric] - simp [h] + simpa using LinearMap.IsSymmetricProjection.ext_iff + (isStarProjection_iff_isSymmetricProjection.mp hS) + (isStarProjection_iff_isSymmetricProjection.mp hT) alias ⟨_, IsStarProjection.ext⟩ := IsStarProjection.ext_iff -theorem isStarProjection_iff_isSymmetricProjection : - IsStarProjection T ↔ T.IsSymmetricProjection := by - simp [isStarProjection_iff, LinearMap.IsSymmetricProjection, - isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def] - end ContinuousLinearMap /-- `U.starProjection` is a star projection. -/ @@ -385,7 +383,7 @@ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E IsStarProjection p ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection := p.isStarProjection_iff_isSymmetricProjection.symm.eq ▸ - isSymmetricProjection_iff_eq_starProjection_range + LinearMap.isSymmetricProjection_iff_eq_starProjection_range namespace LinearMap diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index a8b65c97d11410..239f5dc00c0c0f 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1337,17 +1337,18 @@ theorem starProjection_isSymmetric [K.HasOrthogonalProjection] : open ContinuousLinearMap in /-- `U.starProjection` is a symmetric projection. -/ -theorem isSymmetricProjection_starProjection {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : +theorem _root_.LinearMap.isSymmetricProjection_starProjection + {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : U.starProjection.IsSymmetricProjection := ⟨by simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] using U.isIdempotentElem_starProjection, U.starProjection_isSymmetric⟩ open ContinuousLinearMap in /-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ -theorem isSymmetricProjection_iff_eq_starProjection_range {p : E →L[𝕜] E} : +theorem _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection_range {p : E →L[𝕜] E} : p.IsSymmetricProjection ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection := by - refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection⟩ + refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ LinearMap.isSymmetricProjection_starProjection⟩ have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range refine ⟨this, Eq.symm ?_⟩ ext x @@ -1357,6 +1358,19 @@ theorem isSymmetricProjection_iff_eq_starProjection_range {p : E →L[𝕜] E} : · simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] using hp.isIdempotentElem.eq +open LinearMap in +/-- Symmetric projections are equal iff their range are. -/ +theorem _root_.LinearMap.IsSymmetricProjection.ext_iff {S T : E →ₗ[𝕜] E} + (hS : S.IsSymmetricProjection) (hT : T.IsSymmetricProjection) : + S = T ↔ LinearMap.range S = LinearMap.range T := by + refine ⟨fun h => h ▸ rfl, fun h => ?_⟩ + rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem, + ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric, + ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric] + simp [h] + +alias ⟨_, _root_.LinearMap.IsSymmetricProjection.ext⟩ := LinearMap.IsSymmetricProjection.ext_iff + theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ := by refine ⟨fun h w hw => ?_, fun hv => ?_⟩ From 37f4b38cb958201e5275526c72249d6f38512654 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 29 Jul 2025 16:28:22 +0000 Subject: [PATCH 46/86] longfile --- Mathlib/Analysis/InnerProductSpace/Projection.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 239f5dc00c0c0f..0852ff342dfa2d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -41,7 +41,7 @@ The orthogonal projection construction is adapted from The Coq code is available at the following address: -/ -set_option linter.style.longFile 1700 +set_option linter.style.longFile 1900 noncomputable section From 3beff72ba83aaa71d48e16b1df10dfec2a0b77ec Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Wed, 30 Jul 2025 21:51:34 +0000 Subject: [PATCH 47/86] remove noncomm import --- Mathlib/Algebra/Ring/Idempotent.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 34b3d1ea7591fd..463a7bcd4523c2 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -7,7 +7,6 @@ import Mathlib.Algebra.GroupWithZero.Idempotent import Mathlib.Algebra.Ring.Commute import Mathlib.Order.Notation import Mathlib.Tactic.Convert -import Mathlib.Tactic.NoncommRing import Mathlib.Algebra.Group.Torsion /-! @@ -98,7 +97,7 @@ theorem add_iff [NonUnitalNonAssocSemiring R] [IsCancelAdd R] {a b : R} (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a + b) ↔ a * b + b * a = 0 := by refine ⟨fun h ↦ ?_, ha.add hb⟩ - have := by simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq + have : a + b * a + (a * b + b) = a + b := by simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq rw [← add_right_cancel_iff (a := b), add_assoc, ← add_left_cancel_iff (a := a), ← add_assoc, add_add_add_comm] simpa [add_mul, mul_add, ha.eq, hb.eq] using h.eq @@ -131,11 +130,11 @@ theorem sub_iff [NonUnitalRing R] [IsAddTorsionFree R] {p q : R} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := by refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩ - have h := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq) - have hpq := by simpa using hp.commute_of_anticommute h |>.add_right <| .refl p + have h : p * (q - p) + (q - p) * p = 0 := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq) + have hpq : Commute p q := by simpa using hp.commute_of_anticommute h |>.add_right <| .refl p rw [hpq.eq, and_self, ← nsmul_right_inj two_ne_zero, ← zero_add (2 • p)] convert congrArg (· + 2 • p) h using 1 - simp [sub_mul, mul_sub, hp.eq, hpq.eq] - noncomm_ring + simp [sub_mul, mul_sub, hp.eq, hpq.eq, two_nsmul, + sub_add, sub_sub] end IsIdempotentElem From e929001b7847ce47d13cd3285a4af7b743dad0b2 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Wed, 30 Jul 2025 22:05:38 +0000 Subject: [PATCH 48/86] remove other import --- Mathlib/Algebra/Ring/Idempotent.lean | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Ring/Idempotent.lean b/Mathlib/Algebra/Ring/Idempotent.lean index 463a7bcd4523c2..e511be5744e6c7 100644 --- a/Mathlib/Algebra/Ring/Idempotent.lean +++ b/Mathlib/Algebra/Ring/Idempotent.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Christopher Hoskin -/ import Mathlib.Algebra.GroupWithZero.Idempotent -import Mathlib.Algebra.Ring.Commute +import Mathlib.Algebra.Ring.Defs import Mathlib.Order.Notation import Mathlib.Tactic.Convert import Mathlib.Algebra.Group.Torsion @@ -131,10 +131,16 @@ theorem sub_iff [NonUnitalRing R] [IsAddTorsionFree R] {p q : R} IsIdempotentElem (q - p) ↔ p * q = p ∧ q * p = p := by refine ⟨fun hqp ↦ ?_, fun ⟨h1, h2⟩ => hp.sub hq h1 h2⟩ have h : p * (q - p) + (q - p) * p = 0 := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq) - have hpq : Commute p q := by simpa using hp.commute_of_anticommute h |>.add_right <| .refl p - rw [hpq.eq, and_self, ← nsmul_right_inj two_ne_zero, ← zero_add (2 • p)] + have hpq : Commute p q := by + simp_rw [IsIdempotentElem, mul_sub, sub_mul, + hp.eq, hq.eq, ← sub_add_eq_sub_sub, sub_right_inj, add_sub] at hqp + have h1 := congr_arg (q * ·) hqp + have h2 := congr_arg (· * q) hqp + simp_rw [mul_sub, mul_add, ← mul_assoc, hq.eq, add_sub_cancel_right] at h1 + simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2 + exact h2.symm.trans h1 + rw [hpq.eq, and_self, ← nsmul_right_inj (by simp : 2 ≠ 0), ← zero_add (2 • p)] convert congrArg (· + 2 • p) h using 1 - simp [sub_mul, mul_sub, hp.eq, hpq.eq, two_nsmul, - sub_add, sub_sub] + simp [sub_mul, mul_sub, hp.eq, hpq.eq, two_nsmul, sub_add, sub_sub] end IsIdempotentElem From e251cdc9484e97e20a9ce51ea8b2edb6a3119fbb Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Wed, 30 Jul 2025 22:45:51 +0000 Subject: [PATCH 49/86] Update Positive.lean --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 3dc2a07368e823..cd769346bfdb1e 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -411,9 +411,9 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, ← reApplyInnerSelf_apply, hh hq, hh hp, (this hp).mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 - obtain ⟨h, hht⟩ := isStarProjection_iff_eq_starProjection_range.mp hq - exact hq.mem_range_iff_norm.mpr - (le_antisymm (hht ▸ Submodule.norm_starProjection_apply_le _ _) h2) + obtain ⟨h, hht, rfl⟩ := isStarProjection_iff_eq_starProjection.mp hq + exact Submodule.starProjection_mem_range_iff_norm _ _ |>.mpr + (le_antisymm (Submodule.norm_starProjection_apply_le _ _) h2) /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) From e86dae634ebc3ed32e29c7300a67f2826c755830 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 31 Jul 2025 06:16:34 +0000 Subject: [PATCH 50/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index cd769346bfdb1e..063ca8490894e0 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -411,9 +411,9 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, ← reApplyInnerSelf_apply, hh hq, hh hp, (this hp).mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 - obtain ⟨h, hht, rfl⟩ := isStarProjection_iff_eq_starProjection.mp hq - exact Submodule.starProjection_mem_range_iff_norm _ _ |>.mpr - (le_antisymm (Submodule.norm_starProjection_apply_le _ _) h2) + obtain ⟨U, hU, rfl⟩ := isStarProjection_iff_eq_starProjection.mp hq + simpa using U.mem_iff_norm_starProjection _ |>.mpr + (le_antisymm (U.norm_starProjection_apply_le _) h2) /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) From 4507a1c71712aa4ba775054d915ec3c1a2ef1798 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 31 Jul 2025 06:20:45 +0000 Subject: [PATCH 51/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 063ca8490894e0..9b0d1e01f45b9d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -386,13 +386,11 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : (ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp) tfae_finish -/-- For star projection operators `p,q`, we have `p ≤ q` iff `p ∘ q = p`. -/ -theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} - (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ p ∘L q = p := by +/-- For star projection operators `p,q`, we have `p ≤ q` iff `q ∘ p = p`. -/ +theorem IsStarProjection.le_iff_comp_eq_right {p q : E →L[𝕜] E} + (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ q ∘L p = p := by refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ IsPositive.of_isStarProjection (hp.sub_of_mul_eq_left hq hpq)⟩ - rw [← star_inj] - simp_rw [star_eq_adjoint, adjoint_comp, hp.isSelfAdjoint.adjoint_eq, hq.isSelfAdjoint.adjoint_eq] have : q.comp p = p ↔ LinearMap.range p ≤ LinearMap.range q := by simpa [coe_comp, ← coe_inj] using LinearMap.IsIdempotentElem.comp_eq_right_iff congr(LinearMapClass.linearMap $hq.isIdempotentElem.eq) p.toLinearMap @@ -419,11 +417,8 @@ theorem IsStarProjection.le_iff_comp_eq_left {p q : E →L[𝕜] E} theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection ≤ V.starProjection ↔ U ≤ V := by - rw [isStarProjection_starProjection.le_iff_comp_eq_left - isStarProjection_starProjection, ← star_inj, - isStarProjection_starProjection.isSelfAdjoint, star_eq_adjoint, adjoint_comp] - simp_rw [← star_eq_adjoint, isStarProjection_starProjection.isSelfAdjoint.star_eq] - rw [← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] + rw [isStarProjection_starProjection.le_iff_comp_eq_right isStarProjection_starProjection, + ← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] · have {p : E →L[𝕜] E} : LinearMap.range p.toLinearMap = LinearMap.range p := rfl simp_rw [this, Submodule.range_starProjection] · exact congr(LinearMapClass.linearMap $(isStarProjection_starProjection.isIdempotentElem.eq)) From 2f9c355867b00888217cb892469cefb966f23d52 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 31 Jul 2025 06:21:21 +0000 Subject: [PATCH 52/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 9b0d1e01f45b9d..3c547c0806ea29 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -390,7 +390,7 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : theorem IsStarProjection.le_iff_comp_eq_right {p q : E →L[𝕜] E} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ q ∘L p = p := by refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ - IsPositive.of_isStarProjection (hp.sub_of_mul_eq_left hq hpq)⟩ + IsPositive.of_isStarProjection (hp.sub_of_mul_eq_right hq hpq)⟩ have : q.comp p = p ↔ LinearMap.range p ≤ LinearMap.range q := by simpa [coe_comp, ← coe_inj] using LinearMap.IsIdempotentElem.comp_eq_right_iff congr(LinearMapClass.linearMap $hq.isIdempotentElem.eq) p.toLinearMap From 0545283548860910a57c30ed9eb413d7ce3aa73b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 31 Jul 2025 06:32:54 +0000 Subject: [PATCH 53/86] update --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 3c547c0806ea29..6cc883c73e44c8 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -421,7 +421,7 @@ theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) ← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] · have {p : E →L[𝕜] E} : LinearMap.range p.toLinearMap = LinearMap.range p := rfl simp_rw [this, Submodule.range_starProjection] - · exact congr(LinearMapClass.linearMap $(isStarProjection_starProjection.isIdempotentElem.eq)) + · exact congr(LinearMapClass.linearMap $V.isIdempotentElem_starProjection.eq) end ContinuousLinearMap From f14908ba52648eab99fe61e686750ed52ab24378 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Mon, 4 Aug 2025 23:13:26 +0000 Subject: [PATCH 54/86] Update Symmetric.lean --- Mathlib/Analysis/InnerProductSpace/Symmetric.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 4e0907bd318451..406216237dd651 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -308,10 +308,11 @@ theorem IsIdempotentElem.isSymmetric_iff_orthogonal_range {T : E →ₗ[𝕜] E} end LinearMap +open ContinuousLinearMap in /-- An idempotent operator `T` is symmetric iff `(range T)ᗮ = ker T`. -/ theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range {T : E →L[𝕜] E} (h : IsIdempotentElem T) : T.IsSymmetric ↔ (LinearMap.range T)ᗮ = LinearMap.ker T := - LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range congr(LinearMapClass.linearMap $h.eq) + LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range h.toLinearMap end Normed From a389d18fdd44171bf4417058fa68ff45cc6e7247 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 4 Aug 2025 23:16:03 +0000 Subject: [PATCH 55/86] merge conflict --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 7 ------- 1 file changed, 7 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index b43035e87e93c1..65bc7337ba7b8a 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -358,13 +358,6 @@ theorem isStarProjection_iff_isSymmetricProjection : simp [isStarProjection_iff, LinearMap.IsSymmetricProjection, isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def] -open ContinuousLinearMap in -omit [CompleteSpace E] in -/-- An idempotent operator `T` is symmetric iff `(range T)ᗮ = ker T`. -/ -theorem IsIdempotentElem.isSymmetric_iff_orthogonal_range (h : IsIdempotentElem T) : - T.IsSymmetric ↔ (LinearMap.range T)ᗮ = LinearMap.ker T := - LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range h.toLinearMap - open ContinuousLinearMap in /-- Star projection operators are equal iff their range are. -/ theorem IsStarProjection.ext_iff {S : E →L[𝕜] E} From abe071e68382409635a737f8d88c0337df3dcc9c Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 4 Aug 2025 23:32:04 +0000 Subject: [PATCH 56/86] update --- .../Analysis/InnerProductSpace/Adjoint.lean | 7 ++-- .../InnerProductSpace/Projection.lean | 33 +++++++------------ .../Analysis/InnerProductSpace/Symmetric.lean | 13 ++++++++ 3 files changed, 29 insertions(+), 24 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 65bc7337ba7b8a..913b2674560339 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -381,9 +381,10 @@ open ContinuousLinearMap in /-- An operator is a star projection if and only if it is an orthogonal projection. -/ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E →L[𝕜] E} : IsStarProjection p ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), - p = (LinearMap.range p).starProjection := - p.isStarProjection_iff_isSymmetricProjection.symm.eq ▸ - LinearMap.isSymmetricProjection_iff_eq_starProjection_range + p = (LinearMap.range p).starProjection := by + simp_rw [← p.isStarProjection_iff_isSymmetricProjection.symm.eq, + LinearMap.isSymmetricProjection_iff_eq_starProjection_range, coe_inj] + rfl lemma isStarProjection_iff_eq_starProjection [CompleteSpace E] {p : E →L[𝕜] E} : IsStarProjection p diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index dcfa4c62b00dae..983f18cee0998f 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1344,39 +1344,30 @@ theorem starProjection_isSymmetric [K.HasOrthogonalProjection] : open ContinuousLinearMap in /-- `U.starProjection` is a symmetric projection. -/ -theorem _root_.LinearMap.isSymmetricProjection_starProjection +theorem starProjection_isSymmetricProjection {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : U.starProjection.IsSymmetricProjection := ⟨by simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] using U.isIdempotentElem_starProjection, U.starProjection_isSymmetric⟩ -open ContinuousLinearMap in +open LinearMap in /-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ -theorem _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection_range {p : E →L[𝕜] E} : +theorem _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection_range {p : E →ₗ[𝕜] E} : p.IsSymmetricProjection ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection := by - refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ LinearMap.isSymmetricProjection_starProjection⟩ + refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ starProjection_isSymmetricProjection⟩ have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range refine ⟨this, Eq.symm ?_⟩ ext x refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_ - rw [(IsIdempotentElem.isSymmetric_iff_orthogonal_range _).mp hp.isSymmetric] - · simpa using congr($hp.isIdempotentElem.mul_one_sub_self x) - · simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] - using hp.isIdempotentElem.eq - -open LinearMap in -/-- Symmetric projections are equal iff their range are. -/ -theorem _root_.LinearMap.IsSymmetricProjection.ext_iff {S T : E →ₗ[𝕜] E} - (hS : S.IsSymmetricProjection) (hT : T.IsSymmetricProjection) : - S = T ↔ LinearMap.range S = LinearMap.range T := by - refine ⟨fun h => h ▸ rfl, fun h => ?_⟩ - rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem, - ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric, - ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric] - simp [h] - -alias ⟨_, _root_.LinearMap.IsSymmetricProjection.ext⟩ := LinearMap.IsSymmetricProjection.ext_iff + rw [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric] + simpa using congr($hp.isIdempotentElem.mul_one_sub_self x) + +lemma _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection {p : E →ₗ[𝕜] E} : + p.IsSymmetricProjection + ↔ ∃ (K : Submodule 𝕜 E) (_ : K.HasOrthogonalProjection), p = K.starProjection := + ⟨fun h ↦ ⟨LinearMap.range p, p.isSymmetricProjection_iff_eq_starProjection_range.mp h⟩, + by rintro ⟨_, _, rfl⟩; exact starProjection_isSymmetricProjection⟩ theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ := by diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 406216237dd651..d865e686312791 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -306,6 +306,19 @@ theorem IsIdempotentElem.isSymmetric_iff_orthogonal_range {T : E →ₗ[𝕜] E} ⟨fun hT => hT.orthogonal_range, fun hT => h.isSymmetric_iff_isOrtho_range_ker.eq ▸ hT.symm ▸ isOrtho_orthogonal_right _⟩ +open LinearMap in +/-- Symmetric projections are equal iff their range are. -/ +theorem IsSymmetricProjection.ext_iff {S T : E →ₗ[𝕜] E} + (hS : S.IsSymmetricProjection) (hT : T.IsSymmetricProjection) : + S = T ↔ LinearMap.range S = LinearMap.range T := by + refine ⟨fun h => h ▸ rfl, fun h => ?_⟩ + rw [hS.isIdempotentElem.ext_iff hT.isIdempotentElem, + ← hT.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hT.isSymmetric, + ← hS.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hS.isSymmetric] + simp [h] + +alias ⟨_, IsSymmetricProjection.ext⟩ := IsSymmetricProjection.ext_iff + end LinearMap open ContinuousLinearMap in From 9cb649b869fc329aca9e2ff587ccfd39ae2297f4 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 4 Aug 2025 23:52:04 +0000 Subject: [PATCH 57/86] ispositive.of_issymmetricproj --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 7645fe719f1132..f55ba7e05aee6d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -168,6 +168,10 @@ theorem IsIdempotentElem.isPositive_iff_isSymmetric {T : E →ₗ[𝕜] E} (hT : rw [← hT.eq, Module.End.mul_apply, h] exact inner_self_nonneg +theorem IsPositive.of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : + p.IsPositive := + hp.isIdempotentElem.isPositive_iff_isSymmetric.mpr hp.isSymmetric + end LinearMap namespace ContinuousLinearMap From 2f3481230a89ebbb67907a4ab36373cb552ffd10 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 4 Aug 2025 23:55:23 +0000 Subject: [PATCH 58/86] issymmetricproj instead of isstarproj --- .../Analysis/InnerProductSpace/Positive.lean | 64 +++++++++++-------- 1 file changed, 36 insertions(+), 28 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 770435ca7ecd43..784e5c14c2421b 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -172,6 +172,40 @@ theorem IsPositive.of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSym p.IsPositive := hp.isIdempotentElem.isPositive_iff_isSymmetric.mpr hp.isSymmetric +theorem IsSymmetricProjection.sub_of_mul_eq_right {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : q ∘ₗ p = p) : + (q - p).IsSymmetricProjection := by + refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜 + fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩ + simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp] + +theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ q ∘ₗ p = p := by + refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ + IsPositive.of_isSymmetricProjection (hp.sub_of_mul_eq_right hq hpq)⟩ + rw [hq.isIdempotentElem.comp_eq_right_iff] + intro a ha + specialize h2 a + have hh {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : RCLike.re ⟪T a, a⟫_𝕜 = ‖T a‖ ^ 2 := by + nth_rw 1 [← hT.isIdempotentElem] + rw [Module.End.mul_apply, hT.isSymmetric] + exact inner_self_eq_norm_sq _ + simp_rw [sub_apply, inner_sub_left, map_sub, hh hq, hh hp, + hp.isIdempotentElem.mem_range_iff.mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 + obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_starProjection.mp hq + simpa [Submodule.starProjection_coe_eq_isCompl_projection] using + U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2 + +open Submodule in +theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) + [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : + U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by + simp_rw [starProjection_isSymmetricProjection.le_iff_comp_eq_right + starProjection_isSymmetricProjection, starProjection_coe_eq_isCompl_projection, + IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff] + simp + + end LinearMap namespace ContinuousLinearMap @@ -363,7 +397,8 @@ end PartialOrder @[grind →] theorem IsIdempotentElem.isPositive_iff_isSelfAdjoint {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : p.IsPositive ↔ IsSelfAdjoint p := by - rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap] + rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric + (congr(LinearMapClass.linearMap $hp.eq))] exact isSelfAdjoint_iff_isSymmetric.symm /-- A star projection operator is positive. @@ -389,33 +424,6 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : (ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp) tfae_finish -/-- For star projection operators `p,q`, we have `p ≤ q` iff `q ∘ p = p`. -/ -theorem IsStarProjection.le_iff_comp_eq_right {p q : E →L[𝕜] E} - (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ q ∘L p = p := by - refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ - IsPositive.of_isStarProjection (hp.sub_of_mul_eq_right hq hpq)⟩ - have : q.comp p = p ↔ LinearMap.range p ≤ LinearMap.range q := by - simpa [coe_comp, ← coe_inj] using LinearMap.IsIdempotentElem.comp_eq_right_iff - congr(LinearMapClass.linearMap $hq.isIdempotentElem.eq) p.toLinearMap - rw [this] - intro a ha - specialize h2 a - have {T : E →L[𝕜] E} (hT : IsStarProjection T) : a ∈ LinearMap.range T ↔ T a = a := - (LinearMap.IsIdempotentElem.mem_range_iff - congr(LinearMapClass.linearMap $hT.isIdempotentElem.eq)) - have hh {T : E →L[𝕜] E} (hT : IsStarProjection T) : - T.reApplyInnerSelf a = ‖T a‖ ^ 2 := by - rw [reApplyInnerSelf_apply] - nth_rw 1 [← hT.isIdempotentElem] - rw [mul_apply, ← adjoint_inner_right, hT.isSelfAdjoint.adjoint_eq] - exact inner_self_eq_norm_sq _ - simp_rw [reApplyInnerSelf, sub_apply, inner_sub_left, map_sub, - ← reApplyInnerSelf_apply, hh hq, hh hp, (this hp).mp ha, - sub_nonneg, sq_le_sq, abs_norm] at h2 - obtain ⟨U, hU, rfl⟩ := isStarProjection_iff_eq_starProjection.mp hq - simpa using U.mem_iff_norm_starProjection _ |>.mpr - (le_antisymm (U.norm_starProjection_apply_le _) h2) - /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : From 72c0c7e4aff95519602efc304b01a47c8152e40b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 5 Aug 2025 00:00:25 +0000 Subject: [PATCH 59/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 784e5c14c2421b..64fa7a3e09dc9c 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -197,7 +197,7 @@ theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2 open Submodule in -theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) +theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by simp_rw [starProjection_isSymmetricProjection.le_iff_comp_eq_right @@ -425,14 +425,10 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : tfae_finish /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ -theorem starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) +theorem _root_.Submodule.starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : - U.starProjection ≤ V.starProjection ↔ U ≤ V := by - rw [isStarProjection_starProjection.le_iff_comp_eq_right isStarProjection_starProjection, - ← coe_inj, coe_comp, LinearMap.IsIdempotentElem.comp_eq_right_iff] - · have {p : E →L[𝕜] E} : LinearMap.range p.toLinearMap = LinearMap.range p := rfl - simp_rw [this, Submodule.range_starProjection] - · exact congr(LinearMapClass.linearMap $V.isIdempotentElem_starProjection.eq) + U.starProjection ≤ V.starProjection ↔ U ≤ V := + coe_le_coe_iff (𝕜 := 𝕜) (E := E) _ _ |>.eq ▸ U.coe_starProjection_le_coe_starProjection_iff V end ContinuousLinearMap From daa736e5dc5a50d084e324a5335b395a243264af Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 5 Aug 2025 13:54:07 +0000 Subject: [PATCH 60/86] revert commit --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 64fa7a3e09dc9c..a66dd1f14defb5 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -397,8 +397,7 @@ end PartialOrder @[grind →] theorem IsIdempotentElem.isPositive_iff_isSelfAdjoint {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : p.IsPositive ↔ IsSelfAdjoint p := by - rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric - (congr(LinearMapClass.linearMap $hp.eq))] + rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap] exact isSelfAdjoint_iff_isSymmetric.symm /-- A star projection operator is positive. From d61284be61dd9baaf2e77b8f1f403cd8ae3b385d Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 8 Aug 2025 09:02:15 +0000 Subject: [PATCH 61/86] merge conflict --- .../InnerProductSpace/Projection/Basic.lean | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index e2da90df5139c3..508d832ce3e5e7 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -549,6 +549,13 @@ theorem _root_.ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_rang have := hp.isClosed_range.completeSpace_coe .ofCompleteSpace _ +open LinearMap in +theorem _root_.LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range + {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : + (range p).HasOrthogonalProjection := ⟨fun v => ⟨p v, by + simp [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric, + ← Module.End.mul_apply, hp.isIdempotentElem.eq]⟩⟩ + /-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/ theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero (v : E) : (𝕜 ∙ v)ᗮ.orthogonalProjection v = 0 := @@ -641,6 +648,33 @@ theorem starProjection_isSymmetric [K.HasOrthogonalProjection] : @[deprecated (since := "2025-07-07")] alias orthogonalProjection_isSymmetric := starProjection_isSymmetric +open ContinuousLinearMap in +/-- `U.starProjection` is a symmetric projection. -/ +theorem starProjection_isSymmetricProjection + {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : + U.starProjection.IsSymmetricProjection := + ⟨by simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] + using U.isIdempotentElem_starProjection, U.starProjection_isSymmetric⟩ + +open LinearMap in +/-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ +theorem _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection_range {p : E →ₗ[𝕜] E} : + p.IsSymmetricProjection ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), + p = (LinearMap.range p).starProjection := by + refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ starProjection_isSymmetricProjection⟩ + have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range + refine ⟨this, Eq.symm ?_⟩ + ext x + refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_ + rw [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric] + simpa using congr($hp.isIdempotentElem.mul_one_sub_self x) + +lemma _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection {p : E →ₗ[𝕜] E} : + p.IsSymmetricProjection + ↔ ∃ (K : Submodule 𝕜 E) (_ : K.HasOrthogonalProjection), p = K.starProjection := + ⟨fun h ↦ ⟨LinearMap.range p, p.isSymmetricProjection_iff_eq_starProjection_range.mp h⟩, + by rintro ⟨_, _, rfl⟩; exact starProjection_isSymmetricProjection⟩ + theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ := by refine ⟨fun h w hw => ?_, fun hv => ?_⟩ From 316f4128c215ac5570007412451e68be09222d9b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 10 Aug 2025 11:19:03 +0000 Subject: [PATCH 62/86] update name --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 2 +- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index b9800ee7a16212..5e2a4fbae241d0 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -396,7 +396,7 @@ theorem isStarProjection_iff_eq_starProjection_range [CompleteSpace E] {p : E IsStarProjection p ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection := by simp_rw [← p.isStarProjection_iff_isSymmetricProjection.symm.eq, - LinearMap.isSymmetricProjection_iff_eq_starProjection_range, coe_inj] + LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, coe_inj] rfl lemma isStarProjection_iff_eq_starProjection [CompleteSpace E] {p : E →L[𝕜] E} : diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 508d832ce3e5e7..8be509629cc2fe 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -658,7 +658,7 @@ theorem starProjection_isSymmetricProjection open LinearMap in /-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ -theorem _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection_range {p : E →ₗ[𝕜] E} : +theorem _root_.LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range {p : E →ₗ[𝕜] E} : p.IsSymmetricProjection ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection := by refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ starProjection_isSymmetricProjection⟩ @@ -669,10 +669,10 @@ theorem _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection_range {p : rw [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric] simpa using congr($hp.isIdempotentElem.mul_one_sub_self x) -lemma _root_.LinearMap.isSymmetricProjection_iff_eq_starProjection {p : E →ₗ[𝕜] E} : +lemma _root_.LinearMap.isSymmetricProjection_iff_eq_coe_starProjection {p : E →ₗ[𝕜] E} : p.IsSymmetricProjection ↔ ∃ (K : Submodule 𝕜 E) (_ : K.HasOrthogonalProjection), p = K.starProjection := - ⟨fun h ↦ ⟨LinearMap.range p, p.isSymmetricProjection_iff_eq_starProjection_range.mp h⟩, + ⟨fun h ↦ ⟨LinearMap.range p, p.isSymmetricProjection_iff_eq_coe_starProjection_range.mp h⟩, by rintro ⟨_, _, rfl⟩; exact starProjection_isSymmetricProjection⟩ theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : From 880bcce248b222d29066b4ced046d737625d7c26 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 10 Aug 2025 11:55:27 +0000 Subject: [PATCH 63/86] turn into structure --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 2 +- .../Analysis/InnerProductSpace/Symmetric.lean | 16 +++++----------- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 5e2a4fbae241d0..312e0ec6356d1d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -368,7 +368,7 @@ theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal : theorem isStarProjection_iff_isSymmetricProjection : IsStarProjection T ↔ T.IsSymmetricProjection := by - simp [isStarProjection_iff, LinearMap.IsSymmetricProjection, + simp [isStarProjection_iff, LinearMap.isSymmetricProjection_iff, isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def] open ContinuousLinearMap in diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index d865e686312791..4de377b9c67e37 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -155,16 +155,10 @@ theorem IsSymmetric.coe_re_inner_self_apply {T : E →ₗ[𝕜] E} (hT : T.IsSym simp [← hT x x, hT] /-- A symmetric projection is a symmetric idempotent. -/ -def IsSymmetricProjection (T : E →ₗ[𝕜] E) : Prop := - IsIdempotentElem T ∧ T.IsSymmetric - -theorem IsSymmetricProjection.isIdempotentElem {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : - IsIdempotentElem T := - hT.1 - -theorem IsSymmetricProjection.isSymmetric {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : - T.IsSymmetric := - hT.2 +@[mk_iff] +structure IsSymmetricProjection (T : E →ₗ[𝕜] E) : Prop where + isIdempotentElem : IsIdempotentElem T + isSymmetric : T.IsSymmetric section Complex @@ -281,7 +275,7 @@ open Submodule in theorem _root_.Submodule.IsCompl.projection_isSymmetricProjection_iff {U V : Submodule 𝕜 E} (hUV : IsCompl U V) : hUV.projection.IsSymmetricProjection ↔ U ⟂ V := by - simp [IsSymmetricProjection, hUV.projection_isSymmetric_iff, hUV.projection_isIdempotentElem] + simp [isSymmetricProjection_iff, hUV.projection_isSymmetric_iff, hUV.projection_isIdempotentElem] alias ⟨_, _root_.Submodule.IsCompl.projection_isSymmetricProjection_of_isOrtho⟩ := _root_.Submodule.IsCompl.projection_isSymmetricProjection_iff From c2809a2365044eb772fbebe094c48ec96fd41d5b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 10 Aug 2025 12:00:40 +0000 Subject: [PATCH 64/86] fix --- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 8be509629cc2fe..a31be56194df48 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -652,9 +652,9 @@ open ContinuousLinearMap in /-- `U.starProjection` is a symmetric projection. -/ theorem starProjection_isSymmetricProjection {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : - U.starProjection.IsSymmetricProjection := - ⟨by simpa [IsIdempotentElem, mul_def, ← coe_comp, Module.End.mul_eq_comp] - using U.isIdempotentElem_starProjection, U.starProjection_isSymmetric⟩ + U.starProjection.IsSymmetricProjection where + isIdempotentElem := U.isIdempotentElem_starProjection.toLinearMap + isSymmetric := U.starProjection_isSymmetric open LinearMap in /-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ From 5901617d304c9e7df477feb839fbc94957c00d88 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 10 Aug 2025 12:03:45 +0000 Subject: [PATCH 65/86] update --- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index a31be56194df48..97f461b71a90ba 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -652,9 +652,8 @@ open ContinuousLinearMap in /-- `U.starProjection` is a symmetric projection. -/ theorem starProjection_isSymmetricProjection {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : - U.starProjection.IsSymmetricProjection where - isIdempotentElem := U.isIdempotentElem_starProjection.toLinearMap - isSymmetric := U.starProjection_isSymmetric + U.starProjection.IsSymmetricProjection := + ⟨U.isIdempotentElem_starProjection.toLinearMap, U.starProjection_isSymmetric⟩ open LinearMap in /-- An operator is a symmetric projection if and only if it is an orthogonal projection. -/ From 6fb2fc3d60502b09f48b22880b587ae2683d79b5 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 10 Aug 2025 12:09:49 +0000 Subject: [PATCH 66/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index a66dd1f14defb5..5c699459ea3474 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -182,7 +182,7 @@ theorem IsSymmetricProjection.sub_of_mul_eq_right {p q : E →ₗ[𝕜] E} theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ q ∘ₗ p = p := by refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ - IsPositive.of_isSymmetricProjection (hp.sub_of_mul_eq_right hq hpq)⟩ + IsPositive.of_isSymmetricProjection <| hp.sub_of_mul_eq_right hq hpq⟩ rw [hq.isIdempotentElem.comp_eq_right_iff] intro a ha specialize h2 a @@ -192,7 +192,7 @@ theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} exact inner_self_eq_norm_sq _ simp_rw [sub_apply, inner_sub_left, map_sub, hh hq, hh hp, hp.isIdempotentElem.mem_range_iff.mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2 - obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_starProjection.mp hq + obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_coe_starProjection.mp hq simpa [Submodule.starProjection_coe_eq_isCompl_projection] using U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2 @@ -202,9 +202,7 @@ theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Sub U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by simp_rw [starProjection_isSymmetricProjection.le_iff_comp_eq_right starProjection_isSymmetricProjection, starProjection_coe_eq_isCompl_projection, - IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff] - simp - + IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff, IsCompl.projection_range] end LinearMap From b980d4fc66f9557900ed0b0bee935f40765162fc Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sun, 10 Aug 2025 12:10:52 +0000 Subject: [PATCH 67/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 5c699459ea3474..3013157f37c6b9 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -187,7 +187,7 @@ theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} intro a ha specialize h2 a have hh {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : RCLike.re ⟪T a, a⟫_𝕜 = ‖T a‖ ^ 2 := by - nth_rw 1 [← hT.isIdempotentElem] + conv_lhs => rw [← hT.isIdempotentElem] rw [Module.End.mul_apply, hT.isSymmetric] exact inner_self_eq_norm_sq _ simp_rw [sub_apply, inner_sub_left, map_sub, hh hq, hh hp, From 776c49155128715b8d4999428ad6b357f2976e63 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Tue, 19 Aug 2025 20:06:34 +0000 Subject: [PATCH 68/86] Update Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean Co-authored-by: Jireh Loreaux --- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 97f461b71a90ba..7794c9b61b4fd1 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -552,9 +552,10 @@ theorem _root_.ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_rang open LinearMap in theorem _root_.LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : - (range p).HasOrthogonalProjection := ⟨fun v => ⟨p v, by - simp [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric, - ← Module.End.mul_apply, hp.isIdempotentElem.eq]⟩⟩ + (range p).HasOrthogonalProjection := + ⟨fun v => ⟨p v, by + simp [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric, + ← Module.End.mul_apply, hp.isIdempotentElem.eq]⟩⟩ /-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero. -/ theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero (v : E) : From 0534ff3844fefcfddaf92bf6778044089ba952f0 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Tue, 19 Aug 2025 20:07:34 +0000 Subject: [PATCH 69/86] Update Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean Co-authored-by: Jireh Loreaux --- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 7794c9b61b4fd1..b7679ddf147813 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -651,8 +651,9 @@ theorem starProjection_isSymmetric [K.HasOrthogonalProjection] : open ContinuousLinearMap in /-- `U.starProjection` is a symmetric projection. -/ -theorem starProjection_isSymmetricProjection - {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] : +@[simp] +theorem isSymmetricProjection_starProjection + (U : Submodule 𝕜 E}) [U.HasOrthogonalProjection] : U.starProjection.IsSymmetricProjection := ⟨U.isIdempotentElem_starProjection.toLinearMap, U.starProjection_isSymmetric⟩ From 04fcc38b197f4cb93b1c5718aa82e001b946260b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 19 Aug 2025 20:20:34 +0000 Subject: [PATCH 70/86] deprecate ispositive ofisstarprojection --- .../Analysis/InnerProductSpace/Positive.lean | 18 ++++++------------ .../InnerProductSpace/Projection/Basic.lean | 6 +++--- 2 files changed, 9 insertions(+), 15 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index f55ba7e05aee6d..067e2745aeef6a 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -168,10 +168,16 @@ theorem IsIdempotentElem.isPositive_iff_isSymmetric {T : E →ₗ[𝕜] E} (hT : rw [← hT.eq, Module.End.mul_apply, h] exact inner_self_nonneg +/-- A symmetric projection is positive. -/ +@[aesop 10% apply, grind →] theorem IsPositive.of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : p.IsPositive := hp.isIdempotentElem.isPositive_iff_isSymmetric.mpr hp.isSymmetric +/-- A star projection operator is positive. -/ +@[deprecated (since := "19-08-2025")] +alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection + end LinearMap namespace ContinuousLinearMap @@ -390,15 +396,3 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : tfae_finish end ContinuousLinearMap - -namespace LinearMap - -/-- A star projection operator is positive. -/ -@[aesop 10% apply, grind →] -theorem IsPositive.of_isStarProjection [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} - (hT : IsStarProjection T) : T.IsPositive := - have := FiniteDimensional.complete 𝕜 E - T.isPositive_toContinuousLinearMap_iff.mp (ContinuousLinearMap.IsPositive.of_isStarProjection - (isStarProjection_toContinuousLinearMap_iff.mpr hT)) - -end LinearMap diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 222a7df4c40601..bf066da3a0c21b 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -652,7 +652,7 @@ open ContinuousLinearMap in /-- `U.starProjection` is a symmetric projection. -/ @[simp] theorem isSymmetricProjection_starProjection - (U : Submodule 𝕜 E}) [U.HasOrthogonalProjection] : + (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : U.starProjection.IsSymmetricProjection := ⟨U.isIdempotentElem_starProjection.toLinearMap, U.starProjection_isSymmetric⟩ @@ -661,7 +661,7 @@ open LinearMap in theorem _root_.LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range {p : E →ₗ[𝕜] E} : p.IsSymmetricProjection ↔ ∃ (_ : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection := by - refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ starProjection_isSymmetricProjection⟩ + refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection _⟩ have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range refine ⟨this, Eq.symm ?_⟩ ext x @@ -673,7 +673,7 @@ lemma _root_.LinearMap.isSymmetricProjection_iff_eq_coe_starProjection {p : E p.IsSymmetricProjection ↔ ∃ (K : Submodule 𝕜 E) (_ : K.HasOrthogonalProjection), p = K.starProjection := ⟨fun h ↦ ⟨LinearMap.range p, p.isSymmetricProjection_iff_eq_coe_starProjection_range.mp h⟩, - by rintro ⟨_, _, rfl⟩; exact starProjection_isSymmetricProjection⟩ + by rintro ⟨_, _, rfl⟩; exact isSymmetricProjection_starProjection _⟩ theorem starProjection_apply_eq_zero_iff [K.HasOrthogonalProjection] {v : E} : K.starProjection v = 0 ↔ v ∈ Kᗮ := by From bbe3ef2ac5776a3546a0c7e4bf2390ce9d158c9c Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 19 Aug 2025 20:41:27 +0000 Subject: [PATCH 71/86] LinearMap.isStarProjection_iff_isSymmetricProjection --- Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean index 1f8aad62448735..c939f2e72f76ae 100644 --- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean +++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean @@ -598,6 +598,11 @@ theorem isStarProjection_toContinuousLinearMap_iff {T : E →ₗ[𝕜] E} : simp [isStarProjection_iff, isSelfAdjoint_toContinuousLinearMap_iff, ← ContinuousLinearMap.isIdempotentElem_toLinearMap_iff] +theorem isStarProjection_iff_isSymmetricProjection {T : E →ₗ[𝕜] E} : + IsStarProjection T ↔ T.IsSymmetricProjection := by + simp [← isStarProjection_toContinuousLinearMap_iff, + ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection] + open LinearMap in /-- Star projection operators are equal iff their range are. -/ theorem IsStarProjection.ext_iff {S T : E →ₗ[𝕜] E} From c98cc9b23b9ba517ad273123213bb225584ae596 Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Tue, 19 Aug 2025 22:48:26 +0000 Subject: [PATCH 72/86] Update Positive.lean --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 88686b74a5bf85..b4793d0f82a542 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -207,7 +207,7 @@ theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Sub [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by simp_rw [starProjection_isSymmetricProjection.le_iff_comp_eq_right - starProjection_isSymmetricProjection, starProjection_coe_eq_isCompl_projection, + isSymmetricProjection_starProjection, starProjection_coe_eq_isCompl_projection, IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff, IsCompl.projection_range] end LinearMap From 9489d7119bd8f074b5ca544c8dc106e88fd455ee Mon Sep 17 00:00:00 2001 From: themathqueen <23701951+themathqueen@users.noreply.github.com> Date: Tue, 19 Aug 2025 22:55:04 +0000 Subject: [PATCH 73/86] Update Positive.lean --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index b4793d0f82a542..8be4e1c2b89946 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -206,8 +206,8 @@ open Submodule in theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by - simp_rw [starProjection_isSymmetricProjection.le_iff_comp_eq_right - isSymmetricProjection_starProjection, starProjection_coe_eq_isCompl_projection, + simp_rw [(isSymmetricProjection_starProjection _).le_iff_comp_eq_right + (isSymmetricProjection_starProjection _), starProjection_coe_eq_isCompl_projection, IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff, IsCompl.projection_range] end LinearMap From 3ceeebfc4a6472bc9fd655fde7c0ebc8204d1723 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 19 Aug 2025 22:59:14 +0000 Subject: [PATCH 74/86] move --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 7 ------- Mathlib/Analysis/InnerProductSpace/Symmetric.lean | 7 +++++++ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 8be4e1c2b89946..ab39e343559000 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -178,13 +178,6 @@ theorem IsPositive.of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSym @[deprecated (since := "19-08-2025")] alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection -theorem IsSymmetricProjection.sub_of_mul_eq_right {p q : E →ₗ[𝕜] E} - (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : q ∘ₗ p = p) : - (q - p).IsSymmetricProjection := by - refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜 - fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩ - simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp] - theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ q ∘ₗ p = p := by refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index e622dc3fe710c2..f3f5ddb29ae8d1 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -320,6 +320,13 @@ theorem IsSymmetricProjection.ext_iff {S T : E →ₗ[𝕜] E} alias ⟨_, IsSymmetricProjection.ext⟩ := IsSymmetricProjection.ext_iff +theorem IsSymmetricProjection.sub_of_mul_eq_right {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : q ∘ₗ p = p) : + (q - p).IsSymmetricProjection := by + refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜 + fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩ + simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp] + end LinearMap open ContinuousLinearMap in From 4e744a2fe5ae984cbb29187bb1c137b337559a17 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 19 Aug 2025 23:00:05 +0000 Subject: [PATCH 75/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- Mathlib/Analysis/InnerProductSpace/Symmetric.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index ab39e343559000..f080360877f149 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -181,7 +181,7 @@ alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ q ∘ₗ p = p := by refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ - IsPositive.of_isSymmetricProjection <| hp.sub_of_mul_eq_right hq hpq⟩ + IsPositive.of_isSymmetricProjection <| hp.sub_of_comp_eq_right hq hpq⟩ rw [hq.isIdempotentElem.comp_eq_right_iff] intro a ha specialize h2 a diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index f3f5ddb29ae8d1..5938c833674cf7 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -320,7 +320,7 @@ theorem IsSymmetricProjection.ext_iff {S T : E →ₗ[𝕜] E} alias ⟨_, IsSymmetricProjection.ext⟩ := IsSymmetricProjection.ext_iff -theorem IsSymmetricProjection.sub_of_mul_eq_right {p q : E →ₗ[𝕜] E} +theorem IsSymmetricProjection.sub_of_comp_eq_right {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : q ∘ₗ p = p) : (q - p).IsSymmetricProjection := by refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜 From 16bb624b45d0c28765b3e95d66dc9eb819a20870 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 19 Aug 2025 23:02:07 +0000 Subject: [PATCH 76/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index f080360877f149..1be2c3a601e875 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -199,8 +199,8 @@ open Submodule in theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by - simp_rw [(isSymmetricProjection_starProjection _).le_iff_comp_eq_right - (isSymmetricProjection_starProjection _), starProjection_coe_eq_isCompl_projection, + simp_rw [isSymmetricProjection_starProjection _ |>.le_iff_comp_eq_right <| + isSymmetricProjection_starProjection _, starProjection_coe_eq_isCompl_projection, IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff, IsCompl.projection_range] end LinearMap From aa9bc1dc23239b27e484f9757fb3c4c5bd28fbe0 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 25 Aug 2025 15:42:52 +0000 Subject: [PATCH 77/86] comp_eq_left versions --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 7 +++++++ Mathlib/Analysis/InnerProductSpace/Symmetric.lean | 6 ++++++ 2 files changed, 13 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 1be2c3a601e875..be39bd50e5b7b3 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -195,6 +195,13 @@ theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} simpa [Submodule.starProjection_coe_eq_isCompl_projection] using U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2 +theorem IsSymmetricProjection.le_iff_comp_eq_left {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ p ∘ₗ q = p := by + rw [hp.le_iff_comp_eq_right hq] + constructor <;> intro h <;> ext x <;> apply ext_inner_left 𝕜 fun y => ?_ <;> + simp only [coe_comp, Function.comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _] <;> + simp only [← LinearMap.comp_apply, h] + open Submodule in theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 5938c833674cf7..1dc037b545c855 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -327,6 +327,12 @@ theorem IsSymmetricProjection.sub_of_comp_eq_right {p q : E →ₗ[𝕜] E} fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩ simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp] +theorem IsSymmetricProjection.sub_of_comp_eq_left {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hpq : p ∘ₗ q = p) : + (q - p).IsSymmetricProjection := by + refine hp.sub_of_comp_eq_right hq <| LinearMap.ext fun x => ext_inner_left 𝕜 fun y => ?_ + simp_rw [comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _, ← comp_apply, hpq] + end LinearMap open ContinuousLinearMap in From 2c5cb59c870d92b684b0a6c78acc7c827fc5525a Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Thu, 28 Aug 2025 19:25:26 +0000 Subject: [PATCH 78/86] starprojection_inj --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index d4e4e5ef7aee98..3f432f1bd7cecc 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -202,15 +202,19 @@ theorem IsSymmetricProjection.le_iff_comp_eq_left {p q : E →ₗ[𝕜] E} simp only [coe_comp, Function.comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _] <;> simp only [← LinearMap.comp_apply, h] -open Submodule in -theorem _root_.Submodule.coe_starProjection_le_coe_starProjection_iff (U V : Submodule 𝕜 E) +end LinearMap + +theorem Submodule.coe_starProjection_le_coe_starProjection_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by simp_rw [isSymmetricProjection_starProjection _ |>.le_iff_comp_eq_right <| isSymmetricProjection_starProjection _, starProjection_coe_eq_isCompl_projection, IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff, IsCompl.projection_range] -end LinearMap +theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} + [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : + U.starProjection = V.starProjection ↔ U = V := by + simp only [le_antisymm_iff, ← Submodule.coe_starProjection_le_coe_starProjection_iff, ← coe_inj] namespace ContinuousLinearMap @@ -443,9 +447,9 @@ theorem IsIdempotentElem.TFAE {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : tfae_finish /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ -theorem _root_.Submodule.starProjection_le_starProjection_iff (U V : Submodule 𝕜 E) +theorem _root_.Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection ≤ V.starProjection ↔ U ≤ V := - coe_le_coe_iff (𝕜 := 𝕜) (E := E) _ _ |>.eq ▸ U.coe_starProjection_le_coe_starProjection_iff V + coe_le_coe_iff (𝕜 := 𝕜) (E := E) _ _ |>.eq ▸ U.coe_starProjection_le_coe_starProjection_iff end ContinuousLinearMap From df78e88e2fa31eb6450ab17bd77c0c08d349d86b Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Sat, 6 Sep 2025 18:17:14 +0000 Subject: [PATCH 79/86] all_goals instead of <;> --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 3f432f1bd7cecc..6087e46e2e91d6 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -198,9 +198,12 @@ theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} theorem IsSymmetricProjection.le_iff_comp_eq_left {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ p ∘ₗ q = p := by rw [hp.le_iff_comp_eq_right hq] - constructor <;> intro h <;> ext x <;> apply ext_inner_left 𝕜 fun y => ?_ <;> - simp only [coe_comp, Function.comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _] <;> - simp only [← LinearMap.comp_apply, h] + constructor + all_goals + intro h + apply LinearMap.ext fun x => ext_inner_left 𝕜 fun y => ?_ + simp only [LinearMap.comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _] + simp only [← LinearMap.comp_apply, h] end LinearMap From 3d4d810ee6f0ac01c528da235b600d5e309f0b23 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Tue, 23 Sep 2025 19:07:02 +0000 Subject: [PATCH 80/86] range_le_range instead of comp --- .../Analysis/InnerProductSpace/Positive.lean | 25 ++++++------------- 1 file changed, 7 insertions(+), 18 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 6087e46e2e91d6..05c4085f92dac6 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -178,12 +178,11 @@ theorem IsPositive.of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSym @[deprecated (since := "19-08-2025")] alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection -theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} - (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ q ∘ₗ p = p := by - refine ⟨fun ⟨h1, h2⟩ => ?_, fun hpq ↦ - IsPositive.of_isSymmetricProjection <| hp.sub_of_comp_eq_right hq hpq⟩ - rw [hq.isIdempotentElem.comp_eq_right_iff] - intro a ha +theorem IsSymmetricProjection.le_iff_range_le_range {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ range p ≤ range q := by + refine ⟨fun ⟨h1, h2⟩ a ha => ?_, fun hpq ↦ + IsPositive.of_isSymmetricProjection <| hp.sub_of_comp_eq_right hq <| + hq.isIdempotentElem.comp_eq_right_iff _|>.mpr hpq⟩ specialize h2 a have hh {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : RCLike.re ⟪T a, a⟫_𝕜 = ‖T a‖ ^ 2 := by conv_lhs => rw [← hT.isIdempotentElem] @@ -195,24 +194,14 @@ theorem IsSymmetricProjection.le_iff_comp_eq_right {p q : E →ₗ[𝕜] E} simpa [Submodule.starProjection_coe_eq_isCompl_projection] using U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2 -theorem IsSymmetricProjection.le_iff_comp_eq_left {p q : E →ₗ[𝕜] E} - (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ p ∘ₗ q = p := by - rw [hp.le_iff_comp_eq_right hq] - constructor - all_goals - intro h - apply LinearMap.ext fun x => ext_inner_left 𝕜 fun y => ?_ - simp only [LinearMap.comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _] - simp only [← LinearMap.comp_apply, h] - end LinearMap theorem Submodule.coe_starProjection_le_coe_starProjection_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by - simp_rw [isSymmetricProjection_starProjection _ |>.le_iff_comp_eq_right <| + simp_rw [isSymmetricProjection_starProjection _ |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _, starProjection_coe_eq_isCompl_projection, - IsCompl.projection_isIdempotentElem _ |>.comp_eq_right_iff, IsCompl.projection_range] + IsCompl.projection_range] theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : From ca83f20240173fe89ab1742d1a1e71d6b4445d08 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 17 Oct 2025 19:39:56 +0000 Subject: [PATCH 81/86] move and delete, etc --- .../Analysis/InnerProductSpace/Positive.lean | 27 ++++++++----------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 4ba4b4b9c9b3b4..445e1c8ab5ae30 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -228,18 +228,6 @@ theorem IsSymmetricProjection.le_iff_range_le_range {p q : E →ₗ[𝕜] E} end LinearMap -theorem Submodule.coe_starProjection_le_coe_starProjection_iff {U V : Submodule 𝕜 E} - [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : - U.starProjection.toLinearMap ≤ V.starProjection ↔ U ≤ V := by - simp_rw [isSymmetricProjection_starProjection _ |>.le_iff_range_le_range <| - isSymmetricProjection_starProjection _, starProjection_coe_eq_isCompl_projection, - IsCompl.projection_range] - -theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} - [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : - U.starProjection = V.starProjection ↔ U = V := by - simp only [le_antisymm_iff, ← Submodule.coe_starProjection_le_coe_starProjection_iff, ← coe_inj] - namespace ContinuousLinearMap /-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is symmetric @@ -486,10 +474,17 @@ theorem IsIdempotentElem.TFAE [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIde (ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp) tfae_finish +end ContinuousLinearMap + /-- `U.starProjection ≤ V.starProjection` iff `U ≤ V`. -/ -theorem _root_.Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E} +theorem Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : - U.starProjection ≤ V.starProjection ↔ U ≤ V := - coe_le_coe_iff (𝕜 := 𝕜) (E := E) _ _ |>.eq ▸ U.coe_starProjection_le_coe_starProjection_iff + U.starProjection ≤ V.starProjection ↔ U ≤ V := by + simp_rw [← ContinuousLinearMap.coe_le_coe_iff, isSymmetricProjection_starProjection _ + |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _, + starProjection_coe_eq_isCompl_projection, IsCompl.projection_range] -end ContinuousLinearMap +theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} + [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : + U.starProjection = V.starProjection ↔ U = V := by + simp only [le_antisymm_iff, ← Submodule.starProjection_le_starProjection] From d26da30cba7e1b471397933726a407c0759d8439 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 17 Oct 2025 19:45:16 +0000 Subject: [PATCH 82/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 445e1c8ab5ae30..150cff177124e0 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -487,4 +487,4 @@ theorem Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E} theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection = V.starProjection ↔ U = V := by - simp only [le_antisymm_iff, ← Submodule.starProjection_le_starProjection] + simp only [le_antisymm_iff, ← Submodule.starProjection_le_starProjection_iff] From ebed7f80ff9b0092343fc3b7c8a83f87ca57fda5 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 17 Oct 2025 19:47:38 +0000 Subject: [PATCH 83/86] cleanup --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 150cff177124e0..b322e6cdd40600 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -480,10 +480,11 @@ end ContinuousLinearMap theorem Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection ≤ V.starProjection ↔ U ≤ V := by - simp_rw [← ContinuousLinearMap.coe_le_coe_iff, isSymmetricProjection_starProjection _ + simp_rw [← coe_le_coe_iff, isSymmetricProjection_starProjection _ |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _, starProjection_coe_eq_isCompl_projection, IsCompl.projection_range] +/-- `U.starProjection = V.starProjection` iff `U = V`. -/ theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection = V.starProjection ↔ U = V := by From 14cf5b3c3c0b43b57c173579de69082ef438027f Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 17 Oct 2025 19:50:48 +0000 Subject: [PATCH 84/86] more cleanup --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index b322e6cdd40600..8fee49cd171b8a 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -212,7 +212,7 @@ alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection theorem IsSymmetricProjection.le_iff_range_le_range {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ range p ≤ range q := by - refine ⟨fun ⟨h1, h2⟩ a ha => ?_, fun hpq ↦ + refine ⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ IsPositive.of_isSymmetricProjection <| hp.sub_of_comp_eq_right hq <| hq.isIdempotentElem.comp_eq_right_iff _|>.mpr hpq⟩ specialize h2 a @@ -488,4 +488,4 @@ theorem Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E} theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection = V.starProjection ↔ U = V := by - simp only [le_antisymm_iff, ← Submodule.starProjection_le_starProjection_iff] + simp only [le_antisymm_iff, ← starProjection_le_starProjection_iff] From 8d88dbf2e0d9ccf30633521ea213a63e0ba72622 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 17 Oct 2025 20:01:03 +0000 Subject: [PATCH 85/86] change to range_le_range instead of comps --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 11 ++++++----- Mathlib/Analysis/InnerProductSpace/Symmetric.lean | 12 ++++-------- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index 8fee49cd171b8a..dab25630dd1784 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -202,19 +202,20 @@ open ComplexOrder in /-- A symmetric projection is positive. -/ @[aesop 10% apply, grind →] -theorem IsPositive.of_isSymmetricProjection {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : +theorem IsSymmetricProjection.isPositive {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : p.IsPositive := hp.isIdempotentElem.isPositive_iff_isSymmetric.mpr hp.isSymmetric +@[deprecated (since := "2025-10-17")] alias IsPositive.of_isSymmetricProjection := + IsSymmetricProjection.isPositive + /-- A star projection operator is positive. -/ -@[deprecated (since := "19-08-2025")] +@[deprecated (since := "2025-08-19")] alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection theorem IsSymmetricProjection.le_iff_range_le_range {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ range p ≤ range q := by - refine ⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ - IsPositive.of_isSymmetricProjection <| hp.sub_of_comp_eq_right hq <| - hq.isIdempotentElem.comp_eq_right_iff _|>.mpr hpq⟩ + refine ⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ (hp.sub_of_range_le_range hq hpq).isPositive⟩ specialize h2 a have hh {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : RCLike.re ⟪T a, a⟫_𝕜 = ‖T a‖ ^ 2 := by conv_lhs => rw [← hT.isIdempotentElem] diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 45c229cfdbdf13..8c339beeabde51 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -320,19 +320,15 @@ theorem IsSymmetricProjection.ext_iff {S T : E →ₗ[𝕜] E} alias ⟨_, IsSymmetricProjection.ext⟩ := IsSymmetricProjection.ext_iff -theorem IsSymmetricProjection.sub_of_comp_eq_right {p q : E →ₗ[𝕜] E} - (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : q ∘ₗ p = p) : +open LinearMap in +theorem IsSymmetricProjection.sub_of_range_le_range {p q : E →ₗ[𝕜] E} + (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : range p ≤ range q) : (q - p).IsSymmetricProjection := by + rw [← hq.isIdempotentElem.comp_eq_right_iff] at hqp refine ⟨hp.isIdempotentElem.sub hq.isIdempotentElem (LinearMap.ext fun x => ext_inner_left 𝕜 fun y => ?_) hqp, hq.isSymmetric.sub hp.isSymmetric⟩ simp_rw [Module.End.mul_apply, ← hp.isSymmetric _, ← hq.isSymmetric _, ← comp_apply, hqp] -theorem IsSymmetricProjection.sub_of_comp_eq_left {p q : E →ₗ[𝕜] E} - (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hpq : p ∘ₗ q = p) : - (q - p).IsSymmetricProjection := by - refine hp.sub_of_comp_eq_right hq <| LinearMap.ext fun x => ext_inner_left 𝕜 fun y => ?_ - simp_rw [comp_apply, ← hq.isSymmetric _, ← hp.isSymmetric _, ← comp_apply, hpq] - end LinearMap open ContinuousLinearMap in From e94a8b7ac2b3ac13fefb40b997964e21698dc8dd Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Fri, 17 Oct 2025 20:01:53 +0000 Subject: [PATCH 86/86] fix --- Mathlib/Analysis/InnerProductSpace/Positive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean index dab25630dd1784..21d27e22084dc6 100644 --- a/Mathlib/Analysis/InnerProductSpace/Positive.lean +++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean @@ -211,7 +211,7 @@ theorem IsSymmetricProjection.isPositive {p : E →ₗ[𝕜] E} (hp : p.IsSymmet /-- A star projection operator is positive. -/ @[deprecated (since := "2025-08-19")] -alias IsPositive.of_isStarProjection := IsPositive.of_isSymmetricProjection +alias IsPositive.of_isStarProjection := IsSymmetricProjection.isPositive theorem IsSymmetricProjection.le_iff_range_le_range {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ range p ≤ range q := by