BanLat/Substructures/Band/Projection.lean
All source files · Download exact source
SHA-256: 5400e8d1efbbfda77ccc00e0f8a00e93030960f9325ac5541044686b58469127
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Substructures.Band.DisjointComplement6import BanLat.Substructures.Band.Lattice7import BanLat.Substructures.Band.Generated8import BanLat.Operators.Positive9import BanLat.Operators.Hom1011/-!12# Projection bands1314A band `B` in a vector lattice `X` is a **projection band** when every element15of `X` decomposes (uniquely) as a sum of an element of `B` and an element of16the disjoint complement `Bᵈ`. Equivalently, `X = B ⊕ Bᵈ` as a direct sum.1718The associated **band projection** is the linear map sending `x` to its19component in `B`; it is an idempotent positive operator dominated by the20identity, and a vector lattice homomorphism. A linear operator `T` arises as a21band projection iff `T² = T` and `0 ≤ T ≤ I`.22-/2324variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]25 [VectorLattice X]2627/-- A band `B` in a vector lattice is a **projection band** if every element28of `X` decomposes (uniquely) as a sum of an element of `B` and an element of29`Bᵈ`. Equivalently, `X = B ⊕ Bᵈ` as a direct sum. -/30structure ProjectionBand (X : Type*) [AddCommGroup X] [Lattice X]31 [IsOrderedAddMonoid X] [VectorLattice X]32 extends Band X where33 decomposition' : ∀ x : X, ∃ y z : X, y ∈ carrier34 ∧ z ∈ disjointComplement carrier ∧ x = y + z3536namespace ProjectionBand3738instance : SetLike (ProjectionBand X) X where39 coe B := B.carrier40 coe_injective p q h := by41 cases p; cases q; congr42 exact SetLike.ext' h4344variable (B : ProjectionBand X)4546/-- Every element of `X` decomposes as `y + z` with `y ∈ B` and `z ∈ Bᵈ`. -/47theorem decomposition (x : X) :48 ∃ y z : X, y ∈ B ∧ z ∈ disjointComplement (B : Set X) ∧ x = y + z :=49 B.decomposition' x5051/-- The decomposition in a projection band is unique. -/52theorem decomposition_unique {x y₁ z₁ y₂ z₂ : X}53 (hy₁ : y₁ ∈ B) (hz₁ : z₁ ∈ disjointComplement (B : Set X))54 (hy₂ : y₂ ∈ B) (hz₂ : z₂ ∈ disjointComplement (B : Set X))55 (h₁ : x = y₁ + z₁) (h₂ : x = y₂ + z₂) :56 y₁ = y₂ ∧ z₁ = z₂ := by57 -- y₁ - y₂ = z₂ - z₁, and this element lies in B ∩ Bᵈ ⊆ {0}58 have heq : y₁ - y₂ = z₂ - z₁ := by59 have h := h₁.symm.trans h₂60 calc y₁ - y₂ = (y₁ + z₁) - z₁ - y₂ := by abel61 _ = (y₂ + z₂) - z₁ - y₂ := by rw [h]62 _ = z₂ - z₁ := by abel63 have hmem_B : y₁ - y₂ ∈ B :=64 B.toBand.toOrderIdeal.toSubmodule.sub_mem hy₁ hy₂65 have hmem_Bd : y₁ - y₂ ∈ disjointComplement (B : Set X) := by66 rw [heq]67 exact (Band.disjointComplement68 (B : Set X)).toOrderIdeal.toSubmodule.sub_mem69 (show z₂ ∈ (Band.disjointComplement (B : Set X)).toOrderIdeal.toSubmodule70 from hz₂) hz₁71 have hmem_both : y₁ - y₂ ∈ (↑B) ∩ (↑B)ᵈ := ⟨hmem_B, hmem_Bd⟩72 have hzero : y₁ - y₂ = 0 :=73 Set.mem_singleton_iff.mp (disjointComplement_inter_eq_zero (↑B) hmem_both)74 refine ⟨sub_eq_zero.mp hzero, ?_⟩75 have : z₂ - z₁ = 0 := heq ▸ hzero76 exact eq_of_sub_eq_zero this |>.symm7778/-- The **band projection** onto a projection band: the linear map sending79`x` to its component in `B`. -/80noncomputable def bandProjection : X →ₗ[ℝ] X where81 toFun x := (B.decomposition x).choose82 map_add' := fun x y => by83 set yx := (B.decomposition x).choose84 set zx := (B.decomposition x).choose_spec.choose85 set yy := (B.decomposition y).choose86 set zy := (B.decomposition y).choose_spec.choose87 set yxy := (B.decomposition (x + y)).choose88 set zxy := (B.decomposition (x + y)).choose_spec.choose89 have hyx : yx ∈ B := (B.decomposition x).choose_spec.choose_spec.190 have hzx : zx ∈ (↑B)ᵈ := (B.decomposition x).choose_spec.choose_spec.2.191 have hx_eq : x = yx + zx := (B.decomposition x).choose_spec.choose_spec.2.292 have hyy : yy ∈ B := (B.decomposition y).choose_spec.choose_spec.193 have hzy : zy ∈ (↑B)ᵈ := (B.decomposition y).choose_spec.choose_spec.2.194 have hy_eq : y = yy + zy := (B.decomposition y).choose_spec.choose_spec.2.295 have hyxy : yxy ∈ B := (B.decomposition (x + y)).choose_spec.choose_spec.196 have hzxy : zxy ∈ (↑B)ᵈ :=97 (B.decomposition (x + y)).choose_spec.choose_spec.2.198 have hxy_eq : x + y = yxy + zxy :=99 (B.decomposition (x + y)).choose_spec.choose_spec.2.2100 have hsum_B : yx + yy ∈ B := B.toBand.toOrderIdeal.toSubmodule.add_mem hyx hyy101 have hsum_Bd : zx + zy ∈ (↑B)ᵈ :=102 ((Band.disjointComplement (B : Set X)).toOrderIdeal).toSubmodule.add_mem103 (show zx ∈ ((Band.disjointComplement (B : Set X)).toOrderIdeal).toSubmodule from hzx)104 hzy105 have hsum_eq : x + y = (yx + yy) + (zx + zy) := by rw [hx_eq, hy_eq]; abel106 exact (B.decomposition_unique hyxy hzxy hsum_B hsum_Bd hxy_eq hsum_eq).1107 map_smul' := fun r x => by108 set yx := (B.decomposition x).choose109 set zx := (B.decomposition x).choose_spec.choose110 set yr := (B.decomposition (r • x)).choose111 set zr := (B.decomposition (r • x)).choose_spec.choose112 have hyx : yx ∈ B := (B.decomposition x).choose_spec.choose_spec.1113 have hzx : zx ∈ (↑B)ᵈ := (B.decomposition x).choose_spec.choose_spec.2.1114 have hx_eq : x = yx + zx := (B.decomposition x).choose_spec.choose_spec.2.2115 have hyr : yr ∈ B := (B.decomposition (r • x)).choose_spec.choose_spec.1116 have hzr : zr ∈ (↑B)ᵈ :=117 (B.decomposition (r • x)).choose_spec.choose_spec.2.1118 have hr_eq : r • x = yr + zr :=119 (B.decomposition (r • x)).choose_spec.choose_spec.2.2120 have hscal_B : r • yx ∈ B := B.toBand.toOrderIdeal.toSubmodule.smul_mem r hyx121 have hscal_Bd : r • zx ∈ (↑B)ᵈ :=122 ((Band.disjointComplement (B : Set X)).toOrderIdeal).toSubmodule.smul_mem r123 (show zx ∈ ((Band.disjointComplement (B : Set X)).toOrderIdeal).toSubmodule from hzx)124 have hscal_eq : r • x = r • yx + r • zx := by rw [hx_eq, smul_add]125 simp only [RingHom.id_apply]126 exact (B.decomposition_unique hyr hzr hscal_B hscal_Bd hr_eq hscal_eq).1127128/-- The band projection is idempotent. -/129theorem bandProjection_sq :130 B.bandProjection ∘ₗ B.bandProjection = B.bandProjection := by131 ext x132 simp only [LinearMap.comp_apply]133 -- Bx ∈ B, and Bx = Bx + 0 with 0 ∈ Bᵈ134 have hBx_mem : B.bandProjection x ∈ B :=135 (B.decomposition x).choose_spec.choose_spec.1136 have hBBx_mem : B.bandProjection (B.bandProjection x) ∈ B :=137 (B.decomposition (B.bandProjection x)).choose_spec.choose_spec.1138 set z' := (B.decomposition (B.bandProjection x)).choose_spec.choose139 have hz' : z' ∈ disjointComplement (B : Set X) :=140 (B.decomposition (B.bandProjection x)).choose_spec.choose_spec.2.1141 have hBx_dec : B.bandProjection x =142 B.bandProjection (B.bandProjection x) + z' :=143 (B.decomposition (B.bandProjection x)).choose_spec.choose_spec.2.2144 have h0_mem : (0 : X) ∈ disjointComplement (B : Set X) :=145 ((Band.disjointComplement (B : Set X)).toOrderIdeal).toSubmodule.zero_mem146 have hBx_eq : B.bandProjection x = B.bandProjection x + 0 := (add_zero _).symm147 exact (B.decomposition_unique hBBx_mem hz' hBx_mem h0_mem hBx_dec hBx_eq).1148149private theorem id_sub_bandProjection_mem' (x : X) :150 x - B.bandProjection x ∈ disjointComplement (B : Set X) := by151 have spec := (B.decomposition x).choose_spec.choose_spec152 have heq : x = B.bandProjection x + (B.decomposition x).choose_spec.choose :=153 spec.2.2154 have : x - B.bandProjection x = (B.decomposition x).choose_spec.choose :=155 (eq_sub_of_add_eq' heq.symm).symm156 rw [this]; exact spec.2.1157158/-- The band projection is nonnegative as an operator: `0 ≤ B`. -/159theorem bandProjection_nonneg : 0 ≤ B.bandProjection := by160 rw [Positive.zero_le_iff]161 intro x hx162 set Bx := B.bandProjection x163 set Qx := x - Bx with hQx_def164 have hBx_mem : Bx ∈ B := (B.decomposition x).choose_spec.choose_spec.1165 have hQx_mem : Qx ∈ disjointComplement (B : Set X) := id_sub_bandProjection_mem' B x166 have hBxneg_mem_B : Bx⁻ ∈ B :=167 B.toBand.toOrderIdeal.solid (B.toBand.abs_mem hBx_mem)168 (negPart_nonneg Bx) (sup_le (neg_le_abs Bx) (abs_nonneg Bx))169 have hle_neg_Bx : -Bx ≤ Qx := by170 rw [neg_le_sub_iff_le_add]; exact le_add_of_nonneg_left hx171 have hle : Bx⁻ ≤ |Qx| :=172 le_trans (sup_le_sup_right hle_neg_Bx 0)173 (sup_le (le_abs_self Qx) (abs_nonneg Qx))174 have hQx_abs_mem : |Qx| ∈ disjointComplement (B : Set X) :=175 ((Band.disjointComplement (B : Set X)).toOrderIdeal).abs_mem hQx_mem176 have hBxneg_mem_Bd : Bx⁻ ∈ disjointComplement (B : Set X) :=177 ((Band.disjointComplement (B : Set X)).toOrderIdeal).solid178 hQx_abs_mem (negPart_nonneg Bx) hle179 have hzero : Bx⁻ = 0 :=180 Set.mem_singleton_iff.mp (disjointComplement_inter_eq_zero (↑B)181 ⟨hBxneg_mem_B, hBxneg_mem_Bd⟩)182 exact negPart_eq_zero.mp hzero183184/-- The band projection is dominated by the identity as an operator: `B ≤ I`. -/185theorem bandProjection_le_id : B.bandProjection ≤ LinearMap.id := by186 rw [Positive.le_iff]187 intro x hx188 rw [← sub_nonneg]189 change 0 ≤ LinearMap.id x - B.bandProjection x190 set Bx := B.bandProjection x191 set Qx := x - Bx192 have hBx_mem : Bx ∈ B := (B.decomposition x).choose_spec.choose_spec.1193 have hQx_mem : Qx ∈ disjointComplement (B : Set X) :=194 id_sub_bandProjection_mem' B x195 have hQxneg_mem_Bd : Qx⁻ ∈ disjointComplement (B : Set X) :=196 ((Band.disjointComplement (B : Set X)).toOrderIdeal).solid197 (((Band.disjointComplement (B : Set X)).toOrderIdeal).abs_mem hQx_mem)198 (negPart_nonneg Qx) (sup_le (neg_le_abs Qx) (abs_nonneg Qx))199 have hle_neg_Qx : -Qx ≤ Bx := by200 change -(x - Bx) ≤ Bx; rw [neg_sub]; exact sub_le_self Bx (by exact hx)201 have hle : Qx⁻ ≤ |Bx| :=202 le_trans (sup_le_sup_right hle_neg_Qx 0)203 (sup_le (le_abs_self Bx) (abs_nonneg Bx))204 have hQxneg_mem_B : Qx⁻ ∈ B :=205 B.toBand.toOrderIdeal.solid (B.toBand.abs_mem hBx_mem) (negPart_nonneg Qx) hle206 have hzero : Qx⁻ = 0 :=207 Set.mem_singleton_iff.mp (disjointComplement_inter_eq_zero (↑B)208 ⟨hQxneg_mem_B, hQxneg_mem_Bd⟩)209 exact negPart_eq_zero.mp hzero210211/-- The band projection maps into the band. -/212theorem bandProjection_mem (x : X) :213 B.bandProjection x ∈ B := by214 exact (B.decomposition x).choose_spec.choose_spec.1215216/-- The complement `I - B` maps into the disjoint complement. -/217theorem id_sub_bandProjection_mem (x : X) :218 x - B.bandProjection x ∈ disjointComplement (B : Set X) := by219 set y := (B.decomposition x).choose220 set z := (B.decomposition x).choose_spec.choose221 have hz : z ∈ disjointComplement (B : Set X) :=222 (B.decomposition x).choose_spec.choose_spec.2.1223 have hxyz : x = y + z :=224 (B.decomposition x).choose_spec.choose_spec.2.2225 have : x - B.bandProjection x = z := by226 change x - y = z; rw [hxyz, add_sub_cancel_left]227 rw [this]; exact hz228229/-- A band projection acts as the identity on elements already in the band. -/230theorem bandProjection_eq_of_mem {x : X} (hx : x ∈ B) :231 B.bandProjection x = x := by232 have h0_mem : (0 : X) ∈ disjointComplement (B : Set X) :=233 ((Band.disjointComplement (B : Set X)).toOrderIdeal).toSubmodule.zero_mem234 have hQx_mem : x - B.bandProjection x ∈ disjointComplement (B : Set X) :=235 id_sub_bandProjection_mem' B x236 have hx_dec : x = B.bandProjection x + (x - B.bandProjection x) := by abel237 exact (B.decomposition_unique (B.bandProjection_mem x) hQx_mem238 hx h0_mem hx_dec (add_zero x).symm).1239240/-- The range of the band projection is the band itself. -/241theorem range_bandProjection :242 Set.range B.bandProjection = (B : Set X) := by243 ext x; constructor244 · rintro ⟨y, rfl⟩; exact B.bandProjection_mem y245 · intro hx; exact ⟨x, B.bandProjection_eq_of_mem hx⟩246247/-- The band projection vanishes on elements of the disjoint complement. -/248theorem bandProjection_eq_zero_of_mem_dc {x : X}249 (hx : x ∈ disjointComplement (B : Set X)) :250 B.bandProjection x = 0 := by251 have h0_mem : (0 : X) ∈ (B : Set X) := B.toBand.toOrderIdeal.toSubmodule.zero_mem252 have hdec : x = B.bandProjection x + (x - B.bandProjection x) := by abel253 exact (B.decomposition_unique (B.bandProjection_mem x)254 (B.id_sub_bandProjection_mem x) h0_mem hx hdec (zero_add x).symm).1255256/-- The disjoint complement of a projection band is a projection band. -/257def disjointComplementProjectionBand : ProjectionBand X where258 toBand := Band.disjointComplement (B : Set X)259 decomposition' := fun x => ⟨x - B.bandProjection x, B.bandProjection x,260 (show x - B.bandProjection x ∈ ((B : Set X))ᵈ from B.id_sub_bandProjection_mem x),261 (show B.bandProjection x ∈ ((B : Set X))ᵈᵈ from262 subset_disjointComplement_disjointComplement (B : Set X) (B.bandProjection_mem x)),263 by abel⟩264265/-- An ideal `J` is a projection band iff `J + Jᵈ = X`. -/266theorem projectionBand_iff_add_disjointComplement267 (J : OrderIdeal X) :268 (∃ B : ProjectionBand X, (B : Set X) = (J : Set X)) ↔269 ∀ x : X, ∃ y z : X, y ∈ (J : Set X)270 ∧ z ∈ disjointComplement (J : Set X) ∧ x = y + z := by271 constructor272 · rintro ⟨B, hBJ⟩ x273 obtain ⟨y, z, hy, hz, hxyz⟩ := B.decomposition x274 exact ⟨y, z, hBJ ▸ hy, hBJ ▸ hz, hxyz⟩275 · intro hdecomp276 have heq : ((J : Set X)ᵈ)ᵈ = (J : Set X) := by277 apply Set.Subset.antisymm278 · intro x hx279 obtain ⟨y, z, hy, hz, hxyz⟩ := hdecomp x280 have hy_dd : y ∈ ((J : Set X)ᵈ)ᵈ :=281 subset_disjointComplement_disjointComplement (J : Set X) hy282 have hxmy_dd : x - y ∈ ((J : Set X)ᵈ)ᵈ :=283 ((Band.disjointComplement ((J : Set X)ᵈ)).toOrderIdeal).toSubmodule.sub_mem284 hx hy_dd285 have hxmy_both : x - y ∈ (J : Set X)ᵈ ∩ ((J : Set X)ᵈ)ᵈ :=286 ⟨(hxyz ▸ add_sub_cancel_left y z : x - y = z) ▸ hz, hxmy_dd⟩287 rwa [sub_eq_zero.mp (Set.mem_singleton_iff.mp288 (disjointComplement_inter_eq_zero ((J : Set X)ᵈ) hxmy_both))]289 · exact subset_disjointComplement_disjointComplement (J : Set X)290 exact ⟨{291 toBand := Band.ofPosDirectedSSupMem J292 (fun S hS _hpos _hdir hne x hx => by293 have hS_dd : S ⊆ ((J : Set X)ᵈ)ᵈ := fun s hs =>294 subset_disjointComplement_disjointComplement (J : Set X) (hS hs)295 have hx_dd := (Band.disjointComplement ((J : Set X)ᵈ)).sSup_mem296 hS_dd hne hx297 change x ∈ ((J : Set X)ᵈ)ᵈ at hx_dd298 rw [heq] at hx_dd; exact hx_dd)299 decomposition' := hdecomp }, rfl⟩300301/-- If `X = J₁ ⊕ J₂` where `J₁` and `J₂` are ideals with `J₁ ⊥ J₂`, then302both are projection bands and `J₂ = J₁ᵈ`. -/303theorem of_direct_sum_of_disjoint (J₁ J₂ : OrderIdeal X)304 (hperp : ∀ x ∈ (J₁ : Set X), ∀ y ∈ (J₂ : Set X), IsVLDisjoint x y)305 (hdecomp : ∀ x : X, ∃ y ∈ (J₁ : Set X), ∃ z ∈ (J₂ : Set X),306 x = y + z) :307 disjointComplement (J₁ : Set X) = (J₂ : Set X)308 ∧ ∃ B : ProjectionBand X, (B : Set X) = (J₁ : Set X) := by309 have hJ₂_sub : (J₂ : Set X) ⊆ ((J₁ : Set X))ᵈ := fun z hz a ha =>310 isVLDisjoint_comm.mpr (hperp a ha z hz)311 have hJ₁d_sub : ((J₁ : Set X))ᵈ ⊆ (J₂ : Set X) := by312 intro z hz313 obtain ⟨y, hy, w, hw, hzyw⟩ := hdecomp z314 have hw_d : w ∈ ((J₁ : Set X))ᵈ := hJ₂_sub hw315 have hy_d : y ∈ ((J₁ : Set X))ᵈ := by316 have : y = z - w := by rw [hzyw]; abel317 rw [this]318 exact ((Band.disjointComplement (J₁ : Set X)).toOrderIdeal).toSubmodule.sub_mem319 (show z ∈ ((Band.disjointComplement (J₁ : Set X)).toOrderIdeal).toSubmodule320 from hz) hw_d321 have hy_zero : y = 0 := Set.mem_singleton_iff.mp322 (disjointComplement_inter_eq_zero (J₁ : Set X) ⟨hy, hy_d⟩)323 rw [hy_zero, zero_add] at hzyw; rwa [hzyw]324 refine ⟨Set.Subset.antisymm hJ₁d_sub hJ₂_sub, ?_⟩325 have hdecomp' : ∀ x : X, ∃ y z : X, y ∈ (J₁ : Set X)326 ∧ z ∈ disjointComplement (J₁ : Set X) ∧ x = y + z := fun x => by327 obtain ⟨y, hy, z, hz, hxyz⟩ := hdecomp x328 exact ⟨y, z, hy, hJ₂_sub hz, hxyz⟩329 exact (projectionBand_iff_add_disjointComplement J₁).mpr hdecomp'330331/-! ### Characterisation of band projections -/332333private theorem bpi_monotone {T : X →ₗ[ℝ] X}334 (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x) {x y : X} (hxy : x ≤ y) :335 T x ≤ T y := by336 have : 0 ≤ T (y - x) := hpos _ (sub_nonneg.mpr hxy)337 rwa [map_sub, sub_nonneg] at this338339/-- Range and kernel have disjoint positive cones. -/340private theorem bpi_pos_cone_disjoint {T : X →ₗ[ℝ] X}341 (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)342 (hle : ∀ x : X, 0 ≤ x → T x ≤ x)343 {y z : X} (hy : 0 ≤ y) (hz : 0 ≤ z)344 (hTy : T y = y) (hTz : T z = 0) :345 y ⊓ z = 0 := by346 have hyz_nn : 0 ≤ y ⊓ z := le_inf hy hz347 have hT_yz_le_z : T (y ⊓ z) ≤ T z := bpi_monotone hpos inf_le_right348 rw [hTz] at hT_yz_le_z349 have hT_yz_zero : T (y ⊓ z) = 0 := le_antisymm hT_yz_le_z (hpos _ hyz_nn)350 -- Apply the same argument to `I - T`, which is positive and dominated by the identity.351 have hIT_mono : ∀ {a b : X}, a ≤ b → a - T a ≤ b - T b := fun {a b} hab => by352 have h1 : 0 ≤ (b - a) - T (b - a) := sub_nonneg.mpr353 (hle (b - a) (sub_nonneg.mpr hab))354 rw [map_sub] at h1355 -- h1 : 0 ≤ (b - a) - (T b - T a) = (b - T b) - (a - T a)356 rwa [show (b - a) - (T b - T a) = (b - T b) - (a - T a) by abel,357 sub_nonneg] at h1358 have : y ⊓ z ≤ 0 := by359 calc y ⊓ z = (y ⊓ z) - T (y ⊓ z) := by rw [hT_yz_zero, sub_zero]360 _ ≤ y - T y := hIT_mono inf_le_left361 _ = 0 := by rw [hTy, sub_self]362 exact le_antisymm this hyz_nn363364/-- If `T w = w` then `T(w⁺) = w⁺` and `T(w⁻) = w⁻`. -/365private theorem bpi_preserves_parts {T : X →ₗ[ℝ] X}366 (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)367 (hle : ∀ x : X, 0 ≤ x → T x ≤ x)368 {w : X} (hTw : T w = w) :369 T w⁺ = w⁺ ∧ T w⁻ = w⁻ := by370 have hTwp_le : T w⁺ ≤ w⁺ := hle w⁺ (posPart_nonneg w)371 have hTwn_le : T w⁻ ≤ w⁻ := hle w⁻ (negPart_nonneg w)372 have hdiff : T w⁺ - T w⁻ = w⁺ - w⁻ := by373 rw [← map_sub, posPart_sub_negPart, hTw]374 have hTdisj : T w⁺ ⊓ T w⁻ = 0 :=375 le_antisymm (le_trans (inf_le_inf hTwp_le hTwn_le)376 (le_of_eq (posPart_inf_negPart_eq_zero w)))377 (le_inf (hpos w⁺ (posPart_nonneg w)) (hpos w⁻ (negPart_nonneg w)))378 exact isVLDisjoint_decomposition_unique379 (hpos w⁺ (posPart_nonneg w)) (hpos w⁻ (negPart_nonneg w))380 (posPart_nonneg w) (negPart_nonneg w)381 (isVLDisjoint_of_inf_eq_zero hTdisj)382 (isVLDisjoint_of_inf_eq_zero (posPart_inf_negPart_eq_zero w))383 hdiff384385/-- If `T w = w` then `T |w| = |w|`. -/386private theorem bpi_preserves_abs {T : X →ₗ[ℝ] X}387 (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)388 (hle : ∀ x : X, 0 ≤ x → T x ≤ x)389 {w : X} (hTw : T w = w) : T |w| = |w| := by390 rw [show |w| = w⁺ + w⁻ from (posPart_add_negPart w).symm, map_add,391 (bpi_preserves_parts hpos hle hTw).1, (bpi_preserves_parts hpos hle hTw).2]392393/-- Solidity of the range: if `T x = x`, `0 ≤ y ≤ x`, then `T y = y`. -/394private theorem bpi_range_solid {T : X →ₗ[ℝ] X}395 (hTT : T ∘ₗ T = T) (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)396 (hle : ∀ x : X, 0 ≤ x → T x ≤ x)397 {x y : X} (hx_fixed : T x = x) (hy_nn : 0 ≤ y) (hyx : y ≤ x) :398 T y = y := by399 have hTy_le_y : T y ≤ y := hle y hy_nn400 have hd_nn : 0 ≤ y - T y := sub_nonneg.mpr hTy_le_y401 have hd_le_x : y - T y ≤ x := le_trans (sub_le_self y (hpos y hy_nn)) hyx402 have hx_nn : 0 ≤ x := le_trans hy_nn hyx403 have hres : T (y - T y) = 0 := by404 have : T (T y) = T y := LinearMap.congr_fun hTT y405 rw [map_sub, this, sub_self]406 have hdisjoint := bpi_pos_cone_disjoint hpos hle hx_nn hd_nn hx_fixed hres407 have hle_zero : y - T y ≤ 0 := by408 calc y - T y ≤ x ⊓ (y - T y) := le_inf hd_le_x le_rfl409 _ = 0 := hdisjoint410 exact eq_of_sub_eq_zero (le_antisymm hle_zero hd_nn) |>.symm411412/-- The range `{x | T x = x}` is an `OrderIdeal`. -/413private noncomputable def bpi_rangeIdeal {T : X →ₗ[ℝ] X}414 (hTT : T ∘ₗ T = T) (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)415 (hle : ∀ x : X, 0 ≤ x → T x ≤ x) : OrderIdeal X :=416 OrderIdeal.ofSolid417 { carrier := {x | T x = x}418 add_mem' := fun {a b} (ha : T a = a) (hb : T b = b) =>419 show T (a + b) = a + b by rw [map_add, ha, hb]420 zero_mem' := map_zero T421 smul_mem' := fun r a (ha : T a = a) =>422 show T (r • a) = r • a by rw [map_smul, ha] }423 (fun a b (ha : T a = a) hab => by424 change T b = b425 have ha_abs : T |a| = |a| := bpi_preserves_abs hpos hle ha426 have hb_abs : T |b| = |b| :=427 bpi_range_solid hTT hpos hle ha_abs (abs_nonneg b) hab428 have hTyp : T b⁺ = b⁺ := bpi_range_solid hTT hpos hle hb_abs429 (posPart_nonneg b) (sup_le (le_abs_self b) (abs_nonneg b))430 have hTyn : T b⁻ = b⁻ := bpi_range_solid hTT hpos hle hb_abs431 (negPart_nonneg b) (sup_le (neg_le_abs b) (abs_nonneg b))432 calc T b = T (b⁺ - b⁻) := by rw [posPart_sub_negPart]433 _ = T b⁺ - T b⁻ := map_sub T b⁺ b⁻434 _ = b⁺ - b⁻ := by rw [hTyp, hTyn]435 _ = b := posPart_sub_negPart b)436437/-- The kernel `{x | T x = 0}` is an `OrderIdeal`. -/438private noncomputable def bpi_kernelIdeal {T : X →ₗ[ℝ] X}439 (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)440 (hle : ∀ x : X, 0 ≤ x → T x ≤ x) : OrderIdeal X :=441 OrderIdeal.ofSolid442 { carrier := {x | T x = 0}443 add_mem' := fun {a b} (ha : T a = 0) (hb : T b = 0) =>444 show T (a + b) = 0 by rw [map_add, ha, hb, add_zero]445 zero_mem' := map_zero T446 smul_mem' := fun r a (ha : T a = 0) =>447 show T (r • a) = 0 by rw [map_smul, ha, smul_zero] }448 (fun a b (ha : T a = 0) hab => by449 change T b = 0450 -- From T a = 0 derive T|a| = 0 via T a⁺ = T a⁻ and disjointness451 have hTxp_le : T a⁺ ≤ a⁺ := hle a⁺ (posPart_nonneg a)452 have hTxn_le : T a⁻ ≤ a⁻ := hle a⁻ (negPart_nonneg a)453 have hTdiff : T a⁺ - T a⁻ = 0 := by454 rw [← map_sub, posPart_sub_negPart]; exact ha455 have heq : T a⁺ = T a⁻ := sub_eq_zero.mp hTdiff456 have hTxp_zero : T a⁺ = 0 := by457 apply le_antisymm _ (hpos a⁺ (posPart_nonneg a))458 calc T a⁺ ≤ a⁺ ⊓ T a⁺ := le_inf hTxp_le le_rfl459 _ ≤ a⁺ ⊓ a⁻ := inf_le_inf_left a⁺ (heq ▸ hTxn_le)460 _ = 0 := posPart_inf_negPart_eq_zero a461 have hTxn_zero : T a⁻ = 0 := heq ▸ hTxp_zero462 have hTabsa : T |a| = 0 := by463 rw [show |a| = a⁺ + a⁻ from (posPart_add_negPart a).symm,464 map_add, hTxp_zero, hTxn_zero, add_zero]465 -- T|b| ≤ T|a| = 0 by monotonicity466 have hTabsb : T |b| = 0 :=467 le_antisymm (le_trans (bpi_monotone hpos hab) (le_of_eq hTabsa))468 (hpos |b| (abs_nonneg b))469 -- T b⁺, T b⁻ ≤ T|b| = 0470 have hTyp : T b⁺ = 0 :=471 le_antisymm (le_trans (bpi_monotone hpos472 (sup_le (le_abs_self b) (abs_nonneg b))) (le_of_eq hTabsb))473 (hpos b⁺ (posPart_nonneg b))474 have hTyn : T b⁻ = 0 :=475 le_antisymm (le_trans (bpi_monotone hpos476 (sup_le (neg_le_abs b) (abs_nonneg b))) (le_of_eq hTabsb))477 (hpos b⁻ (negPart_nonneg b))478 calc T b = T (b⁺ - b⁻) := by rw [posPart_sub_negPart]479 _ = T b⁺ - T b⁻ := map_sub T b⁺ b⁻480 _ = 0 := by rw [hTyp, hTyn, sub_self])481482/-- Range and kernel are VL-disjoint. -/483private theorem bpi_range_kernel_disjoint {T : X →ₗ[ℝ] X}484 (hTT : T ∘ₗ T = T) (hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x)485 (hle : ∀ x : X, 0 ≤ x → T x ≤ x)486 (u : X) (hu : u ∈ (bpi_rangeIdeal hTT hpos hle : Set X))487 (v : X) (hv : v ∈ (bpi_kernelIdeal hpos hle : Set X)) :488 IsVLDisjoint u v := by489 change T u = u at hu; change T v = 0 at hv490 have hu_abs : T |u| = |u| := bpi_preserves_abs hpos hle hu491 have hv_abs : T |v| = 0 :=492 show |v| ∈ (bpi_kernelIdeal hpos hle : Set X) from493 (bpi_kernelIdeal hpos hle).abs_mem hv494 change |u| ⊓ |v| = 0495 exact bpi_pos_cone_disjoint (y := |u|) (z := |v|) hpos hle496 (abs_nonneg u) (abs_nonneg v) hu_abs hv_abs497498/-- A linear operator is a band projection iff `T² = T` and `0 ≤ T ≤ id`. -/499theorem bandProjection_iff (T : X →ₗ[ℝ] X) :500 (∃ B : ProjectionBand X, B.bandProjection = T) ↔501 T ∘ₗ T = T ∧ 0 ≤ T ∧ T ≤ LinearMap.id := by502 constructor503 · rintro ⟨B, rfl⟩504 exact ⟨B.bandProjection_sq, B.bandProjection_nonneg, B.bandProjection_le_id⟩505 · -- The converse requires showing Range(T) is a projection band506 rintro ⟨hTT, hpos₀, hle₀⟩507 have hpos : ∀ x : X, 0 ≤ x → 0 ≤ T x := Positive.zero_le_iff.mp hpos₀508 have hle : ∀ x : X, 0 ≤ x → T x ≤ x := fun x hx => Positive.le_iff.mp hle₀ x hx509 set R := bpi_rangeIdeal hTT hpos hle510 set K := bpi_kernelIdeal hpos hle511 -- R and K are disjoint and decompose X512 have hperp : ∀ u ∈ (R : Set X), ∀ v ∈ (K : Set X),513 IsVLDisjoint u v :=514 bpi_range_kernel_disjoint hTT hpos hle515 have hdecomp : ∀ x : X, ∃ y ∈ (R : Set X), ∃ z ∈ (K : Set X),516 x = y + z := fun x => by517 refine ⟨T x, ?_, x - T x, ?_, ?_⟩518 · change T (T x) = T x; exact LinearMap.congr_fun hTT x519 · change T (x - T x) = 0520 have : T (T x) = T x := LinearMap.congr_fun hTT x521 rw [map_sub, this, sub_self]522 · abel523 obtain ⟨hdc, B, hBset⟩ := of_direct_sum_of_disjoint R K hperp hdecomp524 refine ⟨B, ?_⟩525 ext x526 -- B.bandProjection x and T x are both the R-component of x527 have hTx_B : T x ∈ (B : Set X) := by528 rw [hBset]; change T (T x) = T x; exact LinearMap.congr_fun hTT x529 have hQx_Bd : x - T x ∈ disjointComplement (B : Set X) := by530 rw [hBset, hdc]531 change T (x - T x) = 0532 have : T (T x) = T x := LinearMap.congr_fun hTT x533 rw [map_sub, this, sub_self]534 have hBx_dec : x = B.bandProjection x + (x - B.bandProjection x) := by535 abel536 have hTx_dec : x = T x + (x - T x) := by abel537 exact (B.decomposition_unique (B.bandProjection_mem x)538 (B.id_sub_bandProjection_mem x) hTx_B hQx_Bd hBx_dec hTx_dec).1539540/-- A band projection is a lattice homomorphism. -/541theorem bandProjection_isVecLatHom :542 IsVecLatHom B.bandProjection.toFun := by543 have hpos : Positive B.bandProjection := Positive.zero_le_iff.mp B.bandProjection_nonneg544 have hle : ∀ x : X, 0 ≤ x → B.bandProjection x ≤ x :=545 fun x hx => Positive.le_iff.mp B.bandProjection_le_id x hx546 apply IsVecLatHom.of_disjoint547 · exact B.bandProjection.isLinear548 · exact hpos549 · intro x y hxy550 have hx : 0 ≤ x := hxy ▸ inf_le_left551 have hy : 0 ≤ y := hxy ▸ inf_le_right552 apply le_antisymm553 · calc B.bandProjection x ⊓ B.bandProjection y554 ≤ x ⊓ y := inf_le_inf (hle x hx) (hle y hy)555 _ = 0 := hxy556 · exact le_inf (hpos _ hx) (hpos _ hy)557558/-! ### Band projection lemmas -/559560/-- A band projection sends every band to itself: for any band `J` and any561projection band `B`, if `x ∈ J` then `B.bandProjection x ∈ J`. -/562private lemma bandProjection_mem_band (B : ProjectionBand X) (J : Band X)563 {x : X} (hx : x ∈ J) : B.bandProjection x ∈ J := by564 have hpos : ∀ y, 0 ≤ y → y ∈ J → B.bandProjection y ∈ J := fun y hy hyJ =>565 J.solid hyJ566 (Positive.zero_le_iff.mp B.bandProjection_nonneg y hy)567 (Positive.le_iff.mp B.bandProjection_le_id y hy)568 have habs : |x| ∈ J := J.abs_mem hx569 have hxp : x⁺ ∈ J :=570 J.solid habs (posPart_nonneg x) (sup_le (le_abs_self x) (abs_nonneg x))571 have hxn : x⁻ ∈ J :=572 J.solid habs (negPart_nonneg x) (sup_le (neg_le_abs x) (abs_nonneg x))573 have heq : B.bandProjection x =574 B.bandProjection x⁺ - B.bandProjection x⁻ := by575 rw [← map_sub, posPart_sub_negPart]576 rw [heq]577 exact J.toOrderIdeal.toSubmodule.sub_mem578 (hpos _ (posPart_nonneg x) hxp) (hpos _ (negPart_nonneg x) hxn)579580/-- An element disjoint from two bands is disjoint from their supremum. -/581private lemma mem_disjointComplement_band_sup {B₁ B₂ : Band X} {z : X}582 (h₁ : z ∈ disjointComplement (B₁ : Set X))583 (h₂ : z ∈ disjointComplement (B₂ : Set X)) :584 z ∈ disjointComplement ((B₁ ⊔ B₂ : Band X) : Set X) := by585 intro a ha586 have hle : B₁ ⊔ B₂ ≤ Band.disjointComplement {z} :=587 sup_le588 (fun b hb c hc => by rcases hc with rfl; exact isVLDisjoint_comm.mp (h₁ b hb))589 (fun b hb c hc => by rcases hc with rfl; exact isVLDisjoint_comm.mp (h₂ b hb))590 exact isVLDisjoint_comm.mp (hle ha z rfl)591592/-! ### Lattice structure of projection bands593594Projection bands of `X`, ordered by inclusion, form a Boolean algebra. The595order, top, and bottom are inherited from the lattice of bands; binary infima596are given by intersection, binary suprema set-theoretically by the algebraic597sum `B₁ + B₂ = {y + z : y ∈ B₁, z ∈ B₂}`, and the complement is the disjoint598complement. -/599600/-- Projection bands inherit the partial order by inclusion from `SetLike`. -/601instance : PartialOrder (ProjectionBand X) := .ofSetLike (ProjectionBand X) X602603/-- The whole space `X` is a projection band. -/604instance : Top (ProjectionBand X) where605 top :=606 { toBand := (⊤ : Band X)607 decomposition' := fun x => ⟨x, 0,608 show x ∈ ((⊤ : Band X) : Set X) from Band.mem_top,609 fun a _ => isVLDisjoint_zero_left a, (add_zero x).symm⟩ }610611@[simp] theorem mem_top {x : X} : x ∈ (⊤ : ProjectionBand X) :=612 show x ∈ ((⊤ : Band X) : Set X) from Band.mem_top613614/-- The trivial band `{0}` is a projection band. -/615instance : Bot (ProjectionBand X) where616 bot :=617 { toBand := (⊥ : Band X)618 decomposition' := fun x => ⟨0, x,619 show (0 : X) ∈ ((⊥ : Band X) : Set X) from620 (⊥ : Band X).toOrderIdeal.toSubmodule.zero_mem,621 fun a ha => by622 have ha0 : a = 0 := Band.mem_bot.mp ha623 rw [ha0]; exact isVLDisjoint_zero_right x,624 (zero_add x).symm⟩ }625626@[simp] theorem mem_bot {x : X} : x ∈ (⊥ : ProjectionBand X) ↔ x = 0 :=627 show x ∈ ((⊥ : Band X) : Set X) ↔ x = 0 from Band.mem_bot628629/-- The disjoint complement of a projection band, again a projection band. -/630instance : Compl (ProjectionBand X) where631 compl B := B.disjointComplementProjectionBand632633/-- The complement projection band has the expected underlying disjoint complement. -/634theorem coe_compl (B : ProjectionBand X) :635 ((Bᶜ : ProjectionBand X) : Set X) = ((B : Set X))ᵈ := rfl636637/-- Binary infimum of projection bands: the set-theoretic intersection. -/638instance : Min (ProjectionBand X) where639 min B₁ B₂ :=640 { toBand := B₁.toBand ⊓ B₂.toBand641 decomposition' := fun x => by642 refine ⟨B₂.bandProjection (B₁.bandProjection x),643 x - B₂.bandProjection (B₁.bandProjection x),644 ⟨bandProjection_mem_band B₂ B₁.toBand (B₁.bandProjection_mem x),645 B₂.bandProjection_mem _⟩, ?_, by abel⟩646 intro a ha647 have ha₁ : a ∈ (B₁ : Set X) := ha.1648 have ha₂ : a ∈ (B₂ : Set X) := ha.2649 have hsplit : x - B₂.bandProjection (B₁.bandProjection x)650 = (x - B₁.bandProjection x) +651 (B₁.bandProjection x - B₂.bandProjection (B₁.bandProjection x)) := by652 abel653 rw [hsplit]654 exact (B₁.id_sub_bandProjection_mem x a ha₁).add_left655 (B₂.id_sub_bandProjection_mem (B₁.bandProjection x) a ha₂) }656657/-- Binary supremum of projection bands: the algebraic sum658`{y + z : y ∈ B₁, z ∈ B₂}`. -/659instance : Max (ProjectionBand X) where660 max B₁ B₂ :=661 { toBand := B₁.toBand ⊔ B₂.toBand662 decomposition' := fun x => by663 set p := B₁.bandProjection x with hp_def664 set q := B₂.bandProjection (x - p) with hq_def665 refine ⟨p + q, x - (p + q), ?_, ?_, by abel⟩666 · -- p + q ∈ B₁.toBand ⊔ B₂.toBand667 have hp : p ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=668 (le_sup_left : B₁.toBand ≤ _) (B₁.bandProjection_mem x)669 have hq : q ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=670 (le_sup_right : B₂.toBand ≤ _) (B₂.bandProjection_mem _)671 exact (B₁.toBand ⊔ B₂.toBand).toOrderIdeal.toSubmodule.add_mem hp hq672 · -- x - (p + q) ∈ disjointComplement673 have hxmp : x - p ∈ disjointComplement (B₁ : Set X) :=674 B₁.id_sub_bandProjection_mem x675 have hq_B₁d : q ∈ disjointComplement (B₁ : Set X) :=676 bandProjection_mem_band B₂677 (Band.disjointComplement (B₁ : Set X)) hxmp678 have hxpq_B₁d : x - (p + q) ∈ disjointComplement (B₁ : Set X) := by679 have heq : x - (p + q) = (x - p) - q := by abel680 rw [heq]681 exact (Band.disjointComplement (B₁ : Set X)).toOrderIdeal.toSubmodule.sub_mem682 hxmp hq_B₁d683 have hxpq_B₂d : x - (p + q) ∈ disjointComplement (B₂ : Set X) := by684 have heq : x - (p + q) = (x - p) - q := by abel685 rw [heq]686 exact B₂.id_sub_bandProjection_mem (x - p)687 exact mem_disjointComplement_band_sup hxpq_B₁d hxpq_B₂d }688689@[simp] theorem inf_toBand (B₁ B₂ : ProjectionBand X) :690 (B₁ ⊓ B₂).toBand = B₁.toBand ⊓ B₂.toBand := rfl691692@[simp] theorem sup_toBand (B₁ B₂ : ProjectionBand X) :693 (B₁ ⊔ B₂).toBand = B₁.toBand ⊔ B₂.toBand := rfl694695/-- For two projection bands, the supremum of their underlying bands coincides696with the set of algebraic sums `{y + z : y ∈ B₁, z ∈ B₂}`. -/697theorem coe_band_sup_eq_add (B₁ B₂ : ProjectionBand X) :698 ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X)699 = {x | ∃ y ∈ (B₁ : Set X), ∃ z ∈ (B₂ : Set X), x = y + z} := by700 ext x701 refine ⟨fun hx => ?_, ?_⟩702 · set p := B₁.bandProjection x with hp_def703 set q := B₂.bandProjection (x - p) with hq_def704 refine ⟨p, B₁.bandProjection_mem x, q, B₂.bandProjection_mem _, ?_⟩705 have hxmp : x - p ∈ disjointComplement (B₁ : Set X) :=706 B₁.id_sub_bandProjection_mem x707 have hq_B₁d : q ∈ disjointComplement (B₁ : Set X) :=708 bandProjection_mem_band B₂709 (Band.disjointComplement (B₁ : Set X)) hxmp710 have hxpq_B₁d : x - (p + q) ∈ disjointComplement (B₁ : Set X) := by711 have heq : x - (p + q) = (x - p) - q := by abel712 rw [heq]713 exact (Band.disjointComplement (B₁ : Set X)).toOrderIdeal.toSubmodule.sub_mem714 hxmp hq_B₁d715 have hxpq_B₂d : x - (p + q) ∈ disjointComplement (B₂ : Set X) := by716 have heq : x - (p + q) = (x - p) - q := by abel717 rw [heq]718 exact B₂.id_sub_bandProjection_mem (x - p)719 have hxpq_supd : x - (p + q) ∈720 disjointComplement ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=721 mem_disjointComplement_band_sup hxpq_B₁d hxpq_B₂d722 have hxpq_sup : x - (p + q) ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) := by723 have hp_sup : p ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=724 (le_sup_left : B₁.toBand ≤ _) (B₁.bandProjection_mem x)725 have hq_sup : q ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=726 (le_sup_right : B₂.toBand ≤ _) (B₂.bandProjection_mem _)727 exact (B₁.toBand ⊔ B₂.toBand).toOrderIdeal.toSubmodule.sub_mem hx728 ((B₁.toBand ⊔ B₂.toBand).toOrderIdeal.toSubmodule.add_mem hp_sup hq_sup)729 have hzero : x - (p + q) = 0 :=730 Set.mem_singleton_iff.mp731 (disjointComplement_inter_eq_zero _ ⟨hxpq_sup, hxpq_supd⟩)732 exact (sub_eq_zero.mp hzero)733 · rintro ⟨y, hy, z, hz, rfl⟩734 have hy_sup : y ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=735 (le_sup_left : B₁.toBand ≤ _) hy736 have hz_sup : z ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=737 (le_sup_right : B₂.toBand ≤ _) hz738 exact (B₁.toBand ⊔ B₂.toBand).toOrderIdeal.toSubmodule.add_mem hy_sup hz_sup739740/-- Projection bands of `X`, ordered by inclusion, form a Boolean algebra.741The binary lattice operations are intersection and algebraic sum, top and742bottom are the whole space and the trivial band `{0}`, and the complement is743the disjoint complement. -/744instance : BooleanAlgebra (ProjectionBand X) where745 sup := (· ⊔ ·)746 inf := (· ⊓ ·)747 le_sup_left B₁ B₂ x hx := (le_sup_left : B₁.toBand ≤ B₁.toBand ⊔ B₂.toBand) hx748 le_sup_right B₁ B₂ x hx := (le_sup_right : B₂.toBand ≤ B₁.toBand ⊔ B₂.toBand) hx749 sup_le B₁ B₂ K h₁ h₂ x hx :=750 (sup_le (show B₁.toBand ≤ K.toBand from h₁)751 (show B₂.toBand ≤ K.toBand from h₂)) hx752 inf_le_left _ _ _ h := h.1753 inf_le_right _ _ _ h := h.2754 le_inf _ _ _ h₁ h₂ _ hx := ⟨h₁ hx, h₂ hx⟩755 le_sup_inf := fun B B₁ B₂ t ht => by756 obtain ⟨ht_BB₁, ht_BB₂⟩ := ht757 set p := B.bandProjection t with hp_def758 have hp_B : p ∈ B := B.bandProjection_mem t759 have hcomp : ∀ (J : ProjectionBand X), t ∈ ((B.toBand ⊔ J.toBand : Band X) : Set X) →760 t - p ∈ J := fun J ht_BJ => by761 rw [coe_band_sup_eq_add B J] at ht_BJ762 obtain ⟨b, hbB, a, haJ, htba⟩ := ht_BJ763 have hpa : p = b + B.bandProjection a := by764 rw [hp_def, htba, map_add, B.bandProjection_eq_of_mem hbB]765 have hq_eq : t - p = a - B.bandProjection a := by rw [htba, hpa]; abel766 rw [hq_eq]767 exact J.toBand.toOrderIdeal.toSubmodule.sub_mem haJ768 (bandProjection_mem_band B J.toBand haJ)769 have hq_B₁ : t - p ∈ B₁ := hcomp B₁ ht_BB₁770 have hq_B₂ : t - p ∈ B₂ := hcomp B₂ ht_BB₂771 change t ∈ ((B.toBand ⊔ (B₁.toBand ⊓ B₂.toBand) : Band X) : Set X)772 rw [show (B₁.toBand ⊓ B₂.toBand : Band X) = (B₁ ⊓ B₂).toBand from rfl,773 coe_band_sup_eq_add B (B₁ ⊓ B₂)]774 exact ⟨p, hp_B, t - p, ⟨hq_B₁, hq_B₂⟩, by abel⟩775 top := ⊤776 bot := ⊥777 le_top _ _ _ := Submodule.mem_top778 bot_le B x hx := by779 rw [mem_bot.mp hx]; exact B.toBand.toOrderIdeal.toSubmodule.zero_mem780 compl := (·ᶜ)781 inf_compl_le_bot := fun B x hx => by782 have hx0 : x = 0 := Set.mem_singleton_iff.mp783 (disjointComplement_inter_eq_zero (B : Set X) ⟨hx.1, hx.2⟩)784 exact mem_bot.mpr hx0785 top_le_sup_compl := fun B x _ => by786 obtain ⟨y, z, hy, hz, heq⟩ := B.decomposition x787 change x ∈ ((B.toBand ⊔ Bᶜ.toBand : Band X) : Set X)788 rw [coe_band_sup_eq_add B Bᶜ]789 exact ⟨y, hy, z, hz, heq⟩790 sdiff B₁ B₂ := B₁ ⊓ B₂ᶜ791 himp B₁ B₂ := B₂ ⊔ B₁ᶜ792793/-! ### Band projections of associated lattice operations -/794795/-- The band projection onto `B₁ ⊓ B₂` is the composition of the band796projections of `B₁` and `B₂`. -/797theorem bandProjection_inf (B₁ B₂ : ProjectionBand X) :798 (B₁ ⊓ B₂).bandProjection = B₁.bandProjection ∘ₗ B₂.bandProjection := by799 ext x800 change (B₁ ⊓ B₂).bandProjection x = B₁.bandProjection (B₂.bandProjection x)801 set y := B₁.bandProjection (B₂.bandProjection x)802 have hy_B₂ : y ∈ B₂ :=803 bandProjection_mem_band B₁ B₂.toBand (B₂.bandProjection_mem x)804 have hy_B₁ : y ∈ B₁ := B₁.bandProjection_mem _805 have hy_inf : y ∈ ((B₁ ⊓ B₂ : ProjectionBand X) : Set X) := ⟨hy_B₁, hy_B₂⟩806 have hd : x - y ∈ disjointComplement ((B₁ ⊓ B₂ : ProjectionBand X) : Set X) := by807 intro a ha808 have ha₁ : a ∈ (B₁ : Set X) := ha.1809 have ha₂ : a ∈ (B₂ : Set X) := ha.2810 have hsplit : x - y = (x - B₂.bandProjection x) +811 (B₂.bandProjection x - y) := by abel812 rw [hsplit]813 exact (B₂.id_sub_bandProjection_mem x a ha₂).add_left814 (B₁.id_sub_bandProjection_mem (B₂.bandProjection x) a ha₁)815 have heq₁ : x = (B₁ ⊓ B₂).bandProjection x + (x - (B₁ ⊓ B₂).bandProjection x) :=816 by abel817 have heq₂ : x = y + (x - y) := by abel818 exact ((B₁ ⊓ B₂).decomposition_unique819 ((B₁ ⊓ B₂).bandProjection_mem x)820 ((B₁ ⊓ B₂).id_sub_bandProjection_mem x)821 hy_inf hd heq₁ heq₂).1822823/-- Two band projections commute. -/824theorem bandProjection_comm (B₁ B₂ : ProjectionBand X) :825 B₁.bandProjection ∘ₗ B₂.bandProjection826 = B₂.bandProjection ∘ₗ B₁.bandProjection := by827 rw [← bandProjection_inf B₁ B₂, ← bandProjection_inf B₂ B₁,828 show (B₁ ⊓ B₂ : ProjectionBand X) = B₂ ⊓ B₁ from inf_comm _ _]829830/-- The band projection onto `B₁ ⊔ B₂` equals `P₁ + P₂ - P₁ ∘ P₂`. -/831theorem bandProjection_sup (B₁ B₂ : ProjectionBand X) :832 (B₁ ⊔ B₂).bandProjection833 = B₁.bandProjection + B₂.bandProjection834 - B₁.bandProjection ∘ₗ B₂.bandProjection := by835 ext x836 change (B₁ ⊔ B₂).bandProjection x =837 B₁.bandProjection x + B₂.bandProjection x -838 B₁.bandProjection (B₂.bandProjection x)839 set y := B₁.bandProjection x + B₂.bandProjection x -840 B₁.bandProjection (B₂.bandProjection x) with hy_def841 have hy_sup : y ∈ ((B₁ ⊔ B₂ : ProjectionBand X) : Set X) := by842 change y ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X)843 have h1 : B₁.bandProjection x ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=844 (le_sup_left : B₁.toBand ≤ _) (B₁.bandProjection_mem x)845 have h2 : B₂.bandProjection x ∈ ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=846 (le_sup_right : B₂.toBand ≤ _) (B₂.bandProjection_mem x)847 have h3 : B₁.bandProjection (B₂.bandProjection x) ∈848 ((B₁.toBand ⊔ B₂.toBand : Band X) : Set X) :=849 (le_sup_left : B₁.toBand ≤ _) (B₁.bandProjection_mem _)850 exact (B₁.toBand ⊔ B₂.toBand).toOrderIdeal.toSubmodule.sub_mem851 ((B₁.toBand ⊔ B₂.toBand).toOrderIdeal.toSubmodule.add_mem h1 h2) h3852 have hxy_B₁d : x - y ∈ disjointComplement (B₁ : Set X) := by853 have heq : x - y = (x - B₁.bandProjection x) -854 (B₂.bandProjection x - B₁.bandProjection (B₂.bandProjection x)) := by855 rw [hy_def]; abel856 rw [heq]857 exact (Band.disjointComplement (B₁ : Set X)).toOrderIdeal.toSubmodule.sub_mem858 (B₁.id_sub_bandProjection_mem x)859 (B₁.id_sub_bandProjection_mem (B₂.bandProjection x))860 have hxy_B₂d : x - y ∈ disjointComplement (B₂ : Set X) := by861 have heq : x - y = (x - B₂.bandProjection x) -862 B₁.bandProjection (x - B₂.bandProjection x) := by863 rw [hy_def, map_sub]; abel864 rw [heq]865 exact (Band.disjointComplement (B₂ : Set X)).toOrderIdeal.toSubmodule.sub_mem866 (B₂.id_sub_bandProjection_mem x)867 (bandProjection_mem_band B₁ (Band.disjointComplement (B₂ : Set X))868 (B₂.id_sub_bandProjection_mem x))869 have hxy_supd : x - y ∈870 disjointComplement ((B₁ ⊔ B₂ : ProjectionBand X) : Set X) :=871 mem_disjointComplement_band_sup hxy_B₁d hxy_B₂d872 have heq₁ : x = (B₁ ⊔ B₂).bandProjection x + (x - (B₁ ⊔ B₂).bandProjection x) :=873 by abel874 have heq₂ : x = y + (x - y) := by abel875 exact ((B₁ ⊔ B₂).decomposition_unique876 ((B₁ ⊔ B₂).bandProjection_mem x)877 ((B₁ ⊔ B₂).id_sub_bandProjection_mem x)878 hy_sup hxy_supd heq₁ heq₂).1879880/-- The band projection onto the complement equals `id - P`. -/881theorem bandProjection_compl (B : ProjectionBand X) :882 Bᶜ.bandProjection = LinearMap.id - B.bandProjection := by883 ext x884 simp only [LinearMap.sub_apply, LinearMap.id_apply]885 have hy_comp : x - B.bandProjection x ∈ ((Bᶜ : ProjectionBand X) : Set X) :=886 B.id_sub_bandProjection_mem x887 have hz_compd : B.bandProjection x ∈888 disjointComplement ((Bᶜ : ProjectionBand X) : Set X) := fun a ha =>889 isVLDisjoint_comm.mp (ha _ (B.bandProjection_mem x))890 have heq₁ : x = Bᶜ.bandProjection x + (x - Bᶜ.bandProjection x) := by abel891 have heq₂ : x = (x - B.bandProjection x) + B.bandProjection x := by abel892 exact (Bᶜ.decomposition_unique893 (Bᶜ.bandProjection_mem x)894 (Bᶜ.id_sub_bandProjection_mem x)895 hy_comp hz_compd heq₁ heq₂).1896897/-! ### Characterisation via order interval suprema -/898899/-- For a non-negative element, the existence of `IsLUB (B ∩ [0, x])` yields a900disjoint decomposition `x = y + z` with `y ∈ B`, `z ∈ Bᵈ`. -/901private lemma exists_decomposition_of_isLUB_pos {B : Band X}902 (hLUB : ∀ x : X, 0 ≤ x → ∃ s, IsLUB ((B : Set X) ∩ Set.Icc 0 x) s)903 {x : X} (hx_nn : 0 ≤ x) :904 ∃ y z : X, y ∈ (B : Set X) ∧ z ∈ disjointComplement (B : Set X) ∧ x = y + z := by905 obtain ⟨sp, hsp⟩ := hLUB x hx_nn906 have hzero_in_S : (0 : X) ∈ (B : Set X) ∩ Set.Icc 0 x :=907 ⟨B.toOrderIdeal.toSubmodule.zero_mem, le_refl 0, hx_nn⟩908 have hsp_mem : sp ∈ B := B.sSup_mem (fun y hy => hy.1) ⟨0, hzero_in_S⟩ hsp909 have hsp_nn : 0 ≤ sp := hsp.1 hzero_in_S910 have hsp_le : sp ≤ x := hsp.2 (fun y hy => hy.2.2)911 refine ⟨sp, x - sp, hsp_mem, ?_, by abel⟩912 intro a ha913 set d := x - sp with hd_def914 have hd_nn : 0 ≤ d := sub_nonneg.mpr hsp_le915 have hda_nn : 0 ≤ d ⊓ |a| := le_inf hd_nn (abs_nonneg _)916 have habs_B : |a| ∈ B := B.abs_mem ha917 have hda_B : d ⊓ |a| ∈ B := B.solid habs_B hda_nn inf_le_right918 have hsum_B : sp + d ⊓ |a| ∈ B :=919 B.toOrderIdeal.toSubmodule.add_mem hsp_mem hda_B920 have hsum_le : sp + d ⊓ |a| ≤ x := by921 have h1 : sp + d ⊓ |a| ≤ sp + d := by gcongr; exact inf_le_left922 have h2 : sp + d = x := by rw [hd_def]; abel923 exact h2 ▸ h1924 have hub : sp + d ⊓ |a| ≤ sp :=925 hsp.1 ⟨hsum_B, add_nonneg hsp_nn hda_nn, hsum_le⟩926 have hda_zero : d ⊓ |a| ≤ 0 := by927 have h1 : sp + d ⊓ |a| - sp ≤ sp - sp := sub_le_sub_right hub _928 rw [add_sub_cancel_left, sub_self] at h1; exact h1929 have hda_eq : d ⊓ |a| = 0 := le_antisymm hda_zero hda_nn930 change |x - sp| ⊓ |a| = 0931 rw [abs_of_nonneg hd_nn]; exact hda_eq932933/-- For a projection band `B` and `x ∈ X₊`, the band projection of `x` is the934supremum of `B ∩ [0, x]`. -/935theorem isLUB_inter_Icc_bandProjection (B : ProjectionBand X) {x : X} (hx : 0 ≤ x) :936 IsLUB ((B : Set X) ∩ Set.Icc 0 x) (B.bandProjection x) := by937 have hBx_nn : 0 ≤ B.bandProjection x :=938 Positive.zero_le_iff.mp B.bandProjection_nonneg x hx939 have hBx_le : B.bandProjection x ≤ x :=940 Positive.le_iff.mp B.bandProjection_le_id x hx941 have hBx_mem : B.bandProjection x ∈ B := B.bandProjection_mem x942 refine ⟨?_, fun u hu => hu ⟨hBx_mem, hBx_nn, hBx_le⟩⟩943 rintro y ⟨hyB, _, hyx⟩944 have hPy : B.bandProjection y = y := B.bandProjection_eq_of_mem hyB945 have h := Positive.zero_le_iff.mp B.bandProjection_nonneg (x - y)946 (sub_nonneg.mpr hyx)947 rw [map_sub] at h948 have hmono : B.bandProjection y ≤ B.bandProjection x := sub_nonneg.mp h949 exact hPy ▸ hmono950951/-- A band `B` is a projection band iff for every `x ∈ X₊` the set952`B ∩ [0, x]` admits a supremum. -/953theorem projectionBand_iff_isLUB_inter_Icc (B : Band X) :954 (∃ P : ProjectionBand X, (P : Set X) = (B : Set X))955 ↔ ∀ x : X, 0 ≤ x → ∃ s, IsLUB ((B : Set X) ∩ Set.Icc 0 x) s := by956 refine ⟨fun ⟨P, hPB⟩ x hx => ⟨P.bandProjection x, ?_⟩, fun hLUB => ?_⟩957 · have h := isLUB_inter_Icc_bandProjection P hx958 rw [hPB] at h; exact h959 · have hadd : ∀ x : X, ∃ y z : X, y ∈ (B : Set X)960 ∧ z ∈ disjointComplement (B : Set X) ∧ x = y + z := by961 intro x962 obtain ⟨yp, zp, hyp, hzp, hxp⟩ :=963 exists_decomposition_of_isLUB_pos hLUB (posPart_nonneg x)964 obtain ⟨yn, zn, hyn, hzn, hxn⟩ :=965 exists_decomposition_of_isLUB_pos hLUB (negPart_nonneg x)966 refine ⟨yp - yn, zp - zn,967 B.toOrderIdeal.toSubmodule.sub_mem hyp hyn,968 (Band.disjointComplement (B : Set X)).toOrderIdeal.toSubmodule.sub_mem hzp hzn,969 ?_⟩970 calc x = x⁺ - x⁻ := (posPart_sub_negPart x).symm971 _ = (yp + zp) - (yn + zn) := by rw [← hxp, ← hxn]972 _ = (yp - yn) + (zp - zn) := by abel973 exact (projectionBand_iff_add_disjointComplement B.toOrderIdeal).mpr hadd974975/-- If a projection band `B` has the same underlying set as the principal band976generated by `a ∈ X₊`, then for every `x ∈ X₊` the band projection of `x`977equals the supremum of `(x ⊓ n • a)_{n ∈ ℕ}`. -/978theorem isLUB_range_bandProjection_of_principalBand [IsVLArchimedean X]979 {a : X} (ha : 0 ≤ a)980 (B : ProjectionBand X) (hB : (B : Set X) = (Band.generated {a} : Set X))981 {x : X} (hx : 0 ≤ x) :982 IsLUB (Set.range fun n : ℕ => x ⊓ (n : ℕ) • a) (B.bandProjection x) := by983 have hBx_nn : 0 ≤ B.bandProjection x :=984 Positive.zero_le_iff.mp B.bandProjection_nonneg x hx985 have hBx_le : B.bandProjection x ≤ x :=986 Positive.le_iff.mp B.bandProjection_le_id x hx987 have hBx_in : B.bandProjection x ∈ B := B.bandProjection_mem x988 have ha_in : a ∈ B := by989 have : a ∈ (B : Set X) := by rw [hB]; exact Band.subset_generated _ rfl990 exact this991 have hin : ∀ n : ℕ, x ⊓ n • a ∈ B := by992 intro n993 have hna_in : n • a ∈ B :=994 B.toBand.toOrderIdeal.toSubmodule.nsmul_mem ha_in n995 exact B.toBand.solid hna_in (le_inf hx (nsmul_nonneg ha n)) inf_le_right996 refine ⟨?_, ?_⟩997 · rintro _ ⟨n, rfl⟩998 have h := isLUB_inter_Icc_bandProjection B hx999 exact h.1 ⟨hin n, le_inf hx (nsmul_nonneg ha n), inf_le_left⟩1000 · intro u hu1001 have hBx_gen : B.bandProjection x ∈ Band.generated ({a} : Set X) := by1002 have : B.bandProjection x ∈ (B : Set X) := hBx_in1003 rw [hB] at this; exact this1004 have hLUB := (Band.mem_generated_singleton_iff_isLUB_inf_nsmul ha hBx_nn).mp hBx_gen1005 apply hLUB.21006 rintro _ ⟨n, rfl⟩1007 calc B.bandProjection x ⊓ n • a1008 ≤ x ⊓ n • a := inf_le_inf_right _ hBx_le1009 _ ≤ u := hu ⟨n, rfl⟩10101011/-- The principal band generated by `a ∈ X₊` is a projection band iff for every1012`x ∈ X₊` the family `(x ⊓ n • a)_{n ∈ ℕ}` admits a supremum. -/1013theorem principalBand_projectionBand_iff_isLUB_range [IsVLArchimedean X]1014 {a : X} (ha : 0 ≤ a) :1015 (∃ P : ProjectionBand X, (P : Set X) = (Band.generated {a} : Set X))1016 ↔ ∀ x : X, 0 ≤ x →1017 ∃ s, IsLUB (Set.range fun n : ℕ => x ⊓ (n : ℕ) • a) s := by1018 refine ⟨fun ⟨P, hPB⟩ x hx => ⟨P.bandProjection x,1019 isLUB_range_bandProjection_of_principalBand ha P hPB hx⟩, fun hLUB => ?_⟩1020 apply (projectionBand_iff_isLUB_inter_Icc (Band.generated {a})).mpr1021 intro x hx1022 obtain ⟨s, hs⟩ := hLUB x hx1023 have hin : ∀ n : ℕ, x ⊓ n • a ∈ Band.generated ({a} : Set X) := by1024 intro n1025 have ha_in : a ∈ Band.generated ({a} : Set X) := Band.subset_generated _ rfl1026 have hna_in : n • a ∈ Band.generated ({a} : Set X) :=1027 (Band.generated _).toOrderIdeal.toSubmodule.nsmul_mem ha_in n1028 exact (Band.generated _).solid hna_in1029 (le_inf hx (nsmul_nonneg ha n)) inf_le_right1030 have h0_eq : (fun n : ℕ => x ⊓ n • a) 0 = 0 := by1031 change x ⊓ (0 : ℕ) • a = 01032 rw [zero_nsmul]; exact inf_of_le_right hx1033 have hs_nn : 0 ≤ s := by1034 have := hs.1 ⟨0, rfl⟩1035 rw [h0_eq] at this; exact this1036 have hs_le_x : s ≤ x := hs.2 (by rintro _ ⟨n, rfl⟩; exact inf_le_left)1037 refine ⟨s, ?_, fun u hu => ?_⟩1038 · rintro y ⟨hy_gen, hy_nn, hy_le_x⟩1039 have hLUB_y :=1040 (Band.mem_generated_singleton_iff_isLUB_inf_nsmul ha hy_nn).mp hy_gen1041 apply hLUB_y.21042 rintro _ ⟨n, rfl⟩1043 calc y ⊓ n • a1044 ≤ x ⊓ n • a := inf_le_inf_right _ hy_le_x1045 _ ≤ s := hs.1 ⟨n, rfl⟩1046 · apply hs.21047 rintro _ ⟨n, rfl⟩1048 exact hu ⟨hin n, le_inf hx (nsmul_nonneg ha n), inf_le_left⟩10491050end ProjectionBand1051