BanLat/Operators/RieszKantorovich.lean
All source files · Download exact source
SHA-256: 51846724ccfe2955e7ed2f584237c107e08356f2bdb2ec62ca5638090afab92b
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Operators.OrderBounded6import BanLat.Operators.Regular7import BanLat.OrderComplete8import BanLat.RieszDec9import BanLat.Substructures.Band.PPP1011/-!12# The Riesz-Kantorovich theorem1314When the codomain `Y` is order complete, the space `OrderBoundedHom X Y` of15order bounded operators is an order complete vector lattice, with explicit16formulas for the lattice operations (the **Riesz-Kantorovich formulas**).17-/1819namespace OrderBoundedHom2021variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y]22 [Lattice X] [ConditionallyCompleteLattice Y] [IsOrderedAddMonoid X]23 [IsOrderedAddMonoid Y] [VectorLattice X]24 [VectorLattice Y]2526private lemma obZero_apply (x : X) : (0 : OrderBoundedHom X Y) x = (0 : Y) := rfl2728private lemma obToLinearMap_apply (f : OrderBoundedHom X Y) (x : X) :29 f.toLinearMap x = f x := rfl3031/-! ### Positive part construction for the Riesz-Kantorovich theorem -/3233private def ppSet (f : OrderBoundedHom X Y) (x : X) : Set Y :=34 { w | ∃ y, 0 ≤ y ∧ y ≤ x ∧ w = f y }353637private lemma ppSet_nonempty (f : OrderBoundedHom X Y) {x : X}38 (hx : 0 ≤ x) : (ppSet f x).Nonempty :=39 ⟨0, 0, le_rfl, hx, (map_zero f.toLinearMap).symm⟩404142private lemma ppSet_bddAbove (f : OrderBoundedHom X Y) {x : X}43 (hx : 0 ≤ x) : BddAbove (ppSet f x) := by44 obtain ⟨u, _, hbound⟩ := f.isOrderBounded' x hx45 exact ⟨u, fun _ ⟨y, hy, hyx, hw⟩ => hw ▸46 (le_abs_self _).trans47 (hbound y (sup_le hyx (neg_nonpos_of_nonneg hy |>.trans hx)))⟩4849private noncomputable def ppFun (f : OrderBoundedHom X Y)50 (x : X) : Y := by51 classical52 exact if 0 ≤ x then sSup (ppSet f x) else 05354private lemma ppFun_isLUB (f : OrderBoundedHom X Y) {x : X}55 (hx : 0 ≤ x) : IsLUB (ppSet f x) (ppFun f x) := by56 simp only [ppFun, if_pos hx]57 exact isLUB_csSup (ppSet_nonempty f hx) (ppSet_bddAbove f hx)5859private lemma ppFun_nonneg (f : OrderBoundedHom X Y) {x : X}60 (hx : 0 ≤ x) : 0 ≤ ppFun f x :=61 (ppFun_isLUB f hx).162 ⟨0, le_rfl, hx, (map_zero f.toLinearMap).symm⟩6364private lemma le_ppFun (f : OrderBoundedHom X Y) {x : X}65 (hx : 0 ≤ x) : f x ≤ ppFun f x :=66 (ppFun_isLUB f hx).1 ⟨x, hx, le_refl x, rfl⟩6768private lemma ppFun_le (f : OrderBoundedHom X Y) {x : X}69 (hx : 0 ≤ x) {u : Y}70 (hu : u ∈ upperBounds (ppSet f x)) : ppFun f x ≤ u :=71 (ppFun_isLUB f hx).2 hu7273private lemma ppFun_add (f : OrderBoundedHom X Y) {x y : X}74 (hx : 0 ≤ x) (hy : 0 ≤ y) :75 ppFun f (x + y) = ppFun f x + ppFun f y := by76 apply le_antisymm77 · -- ≤: Riesz decomposition78 apply ppFun_le f (add_nonneg hx hy)79 intro w ⟨z, hz, hzxy, hw⟩80 obtain ⟨z₁, z₂, hz₁, hz₁x, hz₂, hz₂y, hsum⟩ :=81 riesz_decomposition z x y hz hx hy hzxy82 rw [hw, hsum]83 change f.toLinearMap (z₁ + z₂) ≤ ppFun f x + ppFun f y84 rw [map_add]85 exact add_le_add86 ((ppFun_isLUB f hx).1 ⟨z₁, hz₁, hz₁x, rfl⟩)87 ((ppFun_isLUB f hy).1 ⟨z₂, hz₂, hz₂y, rfl⟩)88 · -- ≥: double LUB argument89 have step1 : ∀ w₁ ∈ ppSet f x, ∀ w₂ ∈ ppSet f y,90 w₁ + w₂ ≤ ppFun f (x + y) := by91 intro w₁ ⟨z₁, hz₁, hz₁x, hw₁⟩ w₂ ⟨z₂, hz₂, hz₂y, hw₂⟩92 rw [hw₁, hw₂]93 change f.toLinearMap z₁ + f.toLinearMap z₂ ≤ ppFun f (x + y)94 rw [← map_add]95 exact (ppFun_isLUB f (add_nonneg hx hy)).196 ⟨z₁ + z₂, add_nonneg hz₁ hz₂, add_le_add hz₁x hz₂y, rfl⟩97 have step2 : ∀ w₂ ∈ ppSet f y,98 ppFun f x + w₂ ≤ ppFun f (x + y) := by99 intro w₂ hw₂100 have hub : ppFun f (x + y) - w₂ ∈ upperBounds (ppSet f x) :=101 fun w₁ hw₁ =>102 le_sub_iff_add_le.mpr (step1 w₁ hw₁ w₂ hw₂)103 exact le_sub_iff_add_le.mp (ppFun_le f hx hub)104 have hub : ppFun f (x + y) - ppFun f x ∈105 upperBounds (ppSet f y) :=106 fun w₂ hw₂ => le_sub_iff_add_le.mpr107 (by rw [add_comm]; exact step2 w₂ hw₂)108 rw [add_comm]109 exact le_sub_iff_add_le.mp (ppFun_le f hy hub)110111/-! ### The positive part operator -/112113private noncomputable def ppOp (f : OrderBoundedHom X Y) :114 X →ₗ[ℝ] Y := by115 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice116 exact Positive.extension (fun x hx => ppFun_nonneg f hx)117 (fun _ _ hx hy => ppFun_add f hx hy)118119private lemma ppOp_apply_nonneg (f : OrderBoundedHom X Y)120 {x : X} (hx : 0 ≤ x) : ppOp f x = ppFun f x := by121 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice122 exact Positive.extension_nonneg (fun x hx => ppFun_nonneg f hx)123 (fun _ _ hx hy => ppFun_add f hx hy) hx124125private lemma ppOp_positive (f : OrderBoundedHom X Y) :126 Positive (ppOp f) := by127 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice128 exact Positive.extension_positive129 (fun x hx => ppFun_nonneg f hx)130 (fun _ _ hx hy => ppFun_add f hx hy)131132private lemma le_ppOp (f : OrderBoundedHom X Y) {x : X}133 (hx : 0 ≤ x) : f x ≤ ppOp f x :=134 ppOp_apply_nonneg f hx ▸ le_ppFun f hx135136private lemma ppOp_le (f g : OrderBoundedHom X Y)137 (hg0 : ∀ x : X, 0 ≤ x → 0 ≤ g x)138 (hgf : ∀ x : X, 0 ≤ x → f x ≤ g x)139 {x : X} (hx : 0 ≤ x) : ppOp f x ≤ g x := by140 rw [ppOp_apply_nonneg f hx]141 apply ppFun_le f hx142 intro _ ⟨y, hy, hyx, hw⟩143 rw [hw]144 exact (hgf y hy).trans145 ((Positive.monotone_iff.mpr146 (show Positive g.toLinearMap from hg0)) hyx)147148/-! ### Sup, inf and lattice laws -/149150private noncomputable def obPosPart151 (f : OrderBoundedHom X Y) : OrderBoundedHom X Y :=152 ⟨ppOp f, Positive.isOrderBounded (ppOp_positive f)⟩153154private lemma obPosPart_apply (f : OrderBoundedHom X Y) (x : X) :155 obPosPart f x = ppOp f x := rfl156157private lemma obPosPart_nonneg (f : OrderBoundedHom X Y) :158 (0 : OrderBoundedHom X Y) ≤ obPosPart f :=159 le_iff.mpr fun x hx => by160 simpa only [obZero_apply, obPosPart_apply] using ppOp_positive f x hx161162private lemma le_obPosPart (f : OrderBoundedHom X Y) :163 f ≤ obPosPart f :=164 le_iff.mpr fun _ hx => le_ppOp f hx165166private lemma obPosPart_le {f g : OrderBoundedHom X Y}167 (hg0 : (0 : OrderBoundedHom X Y) ≤ g) (hgf : f ≤ g) :168 obPosPart f ≤ g :=169 le_iff.mpr fun x hx => by170 apply ppOp_le f g _ _ hx171 · intro y hy172 simpa only [obZero_apply] using le_iff.mp hg0 y hy173 · intro y hy; exact le_iff.mp hgf y hy174175private noncomputable def obSup176 (f g : OrderBoundedHom X Y) : OrderBoundedHom X Y :=177 g + obPosPart (f - g)178179private noncomputable def obInf180 (f g : OrderBoundedHom X Y) : OrderBoundedHom X Y :=181 f + g - obSup f g182183private lemma le_obSup_left (f g : OrderBoundedHom X Y) :184 f ≤ obSup f g := by185 change f ≤ g + obPosPart (f - g)186 have h1 := add_le_add_left (le_obPosPart (f - g)) g187 rw [sub_add_cancel, add_comm] at h1188 exact h1189190private lemma le_obSup_right (f g : OrderBoundedHom X Y) :191 g ≤ obSup f g := by192 change g ≤ g + obPosPart (f - g)193 exact le_add_of_nonneg_right (obPosPart_nonneg (f - g))194195private lemma obSup_le {f g h : OrderBoundedHom X Y}196 (hfh : f ≤ h) (hgh : g ≤ h) :197 obSup f g ≤ h := by198 change g + obPosPart (f - g) ≤ h199 have h1 : obPosPart (f - g) ≤ h - g :=200 obPosPart_le (sub_nonneg.mpr hgh)201 (sub_le_sub_right hfh g)202 have h2 := add_le_add_left h1 g203 rw [sub_add_cancel, add_comm] at h2204 exact h2205206private lemma obInf_le_left (f g : OrderBoundedHom X Y) :207 obInf f g ≤ f := by208 have : obInf f g = f - obPosPart (f - g) := by209 change f + g - (g + obPosPart (f - g)) =210 f - obPosPart (f - g); abel211 rw [this]212 exact sub_le_self f (obPosPart_nonneg (f - g))213214private lemma obInf_le_right (f g : OrderBoundedHom X Y) :215 obInf f g ≤ g := by216 have h1 : obInf f g = f - obPosPart (f - g) := by217 change f + g - (g + obPosPart (f - g)) =218 f - obPosPart (f - g); abel219 rw [h1]220 calc f - obPosPart (f - g)221 ≤ f - (f - g) :=222 sub_le_sub_left (le_obPosPart (f - g)) f223 _ = g := by abel224225private lemma le_obInf {f g h : OrderBoundedHom X Y}226 (hhf : h ≤ f) (hhg : h ≤ g) :227 h ≤ obInf f g := by228 have key : obPosPart (f - g) ≤ f - h :=229 obPosPart_le (sub_nonneg.mpr hhf)230 (sub_le_sub_left hhg f)231 have h2 : obInf f g = f - obPosPart (f - g) := by232 change f + g - (g + obPosPart (f - g)) =233 f - obPosPart (f - g); abel234 rw [h2]235 calc h = f - (f - h) := by abel236 _ ≤ f - obPosPart (f - g) :=237 sub_le_sub_left key f238239/-- When the codomain is order complete, the space of order bounded240operators is a lattice. -/241noncomputable instance instLattice :242 Lattice (OrderBoundedHom X Y) :=243 { (inferInstance :244 PartialOrder (OrderBoundedHom X Y)) with245 sup := obSup246 inf := obInf247 le_sup_left := le_obSup_left248 le_sup_right := le_obSup_right249 sup_le := fun _ _ _ hfh hgh => obSup_le hfh hgh250 inf_le_left := obInf_le_left251 inf_le_right := obInf_le_right252 le_inf := fun _ _ _ hhf hhg => le_obInf hhf hhg }253254/-- When the codomain is order complete, the space of order bounded255operators is a vector lattice. -/256noncomputable instance instVectorLattice :257 VectorLattice (OrderBoundedHom X Y) :=258 { (inferInstance : Module ℝ (OrderBoundedHom X Y)),259 (inferInstance :260 PosSMulMono ℝ (OrderBoundedHom X Y)) with }261262/-! ### Riesz-Kantorovich formulas -/263264265private lemma sub_apply (f g : OrderBoundedHom X Y) (y : X) :266 (f - g : OrderBoundedHom X Y) y = f y - g y :=267 show (f.toLinearMap - g.toLinearMap) y = _ from268 LinearMap.sub_apply _ _ _269270271private lemma add_apply' (f g : OrderBoundedHom X Y) (y : X) :272 (f + g : OrderBoundedHom X Y) y = f y + g y :=273 show (f.toLinearMap + g.toLinearMap) y = _ from274 LinearMap.add_apply _ _ _275276277private lemma map_sub_val (f : OrderBoundedHom X Y) (a b : X) :278 f (a - b) = f a - f b :=279 show f.toLinearMap (a - b) = _ from map_sub f.toLinearMap a b280281private lemma sup_zero_eq_obPosPart282 (f : OrderBoundedHom X Y) :283 f ⊔ 0 = obPosPart f := by284 have : f ⊔ (0 : OrderBoundedHom X Y) =285 (0 : OrderBoundedHom X Y) + obPosPart (f - 0) := rfl286 rw [sub_zero, zero_add] at this; exact this287288private lemma posPart_apply_eq_ppFun289 {f : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :290 f⁺ x = ppFun f x := by291 rw [posPart_def, sup_zero_eq_obPosPart]292 simpa only [obPosPart_apply] using ppOp_apply_nonneg f hx293294/-- The positive part at a positive element is the supremum over295the order interval `[0, x]`. -/296theorem isLUB_posPart_apply297 {f : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :298 IsLUB {w | ∃ y, 0 ≤ y ∧ y ≤ x ∧ w = f y}299 (f⁺ x) := by300 rw [posPart_apply_eq_ppFun hx]; exact ppFun_isLUB f hx301302/-- The negative part at a positive element. -/303theorem isLUB_negPart_apply304 {f : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :305 IsLUB {w | ∃ y, 0 ≤ y ∧ y ≤ x ∧ w = -(f y)}306 (f⁻ x) := by307 have h : f⁻ = (-f)⁺ := by rw [negPart_def, posPart_def]308 rw [h, posPart_apply_eq_ppFun hx]309 exact ppFun_isLUB (-f) hx310311/-- The supremum of order bounded operators at a positive element312is given by the Riesz-Kantorovich formula. -/313theorem isLUB_sup_apply314 {f g : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :315 IsLUB316 {w | ∃ y z, 0 ≤ y ∧ 0 ≤ z ∧ y + z = x317 ∧ w = f y + g z}318 ((f ⊔ g) x) := by319 have hval : (f ⊔ g) x = g x + (f - g)⁺ x := by320 have h := sup_eq_add_posPart_sub f g; rw [h, add_apply']321 have hbridge : ∀ y : X, f y + g (x - y) = g x + (f - g) y := by322 intro y; rw [sub_apply, map_sub_val]; abel323 rw [hval, posPart_apply_eq_ppFun hx]324 have hPP := ppFun_isLUB (f - g) hx325 constructor326 · intro w ⟨y, z, hy, hz, hyz, hw⟩327 have hyx : y ≤ x := hyz ▸ le_add_of_nonneg_right hz328 rw [hw, show z = x - y from eq_sub_of_add_eq' hyz, hbridge]329 gcongr; exact hPP.1 ⟨y, hy, hyx, rfl⟩330 · intro u hu331 rw [show g x + ppFun (f - g) x =332 ppFun (f - g) x + g x from add_comm _ _,333 ← le_sub_iff_add_le]334 apply hPP.2335 intro v ⟨y, hy, hyx, hv⟩336 rw [le_sub_iff_add_le, hv, add_comm, ← hbridge]337 exact hu ⟨y, x - y, hy, sub_nonneg.mpr hyx, by abel, rfl⟩338339340private lemma map_add_val (f : OrderBoundedHom X Y) (a b : X) :341 f (a + b) = f a + f b :=342 show f.toLinearMap _ = _ from map_add f.toLinearMap a b343344345private lemma neg_apply' (f : OrderBoundedHom X Y) (y : X) :346 (-f : OrderBoundedHom X Y) y = -(f y) :=347 show (-f.toLinearMap) y = _ from LinearMap.neg_apply _ _348349/-- The infimum of order bounded operators at a positive element. -/350theorem isGLB_inf_apply351 {f g : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :352 IsGLB353 {w | ∃ y z, 0 ≤ y ∧ 0 ≤ z ∧ y + z = x354 ∧ w = f y + g z}355 ((f ⊓ g) x) := by356 set S := {w : Y | ∃ y z, 0 ≤ y ∧ 0 ≤ z ∧ y + z = x357 ∧ w = f y + g z}358 set c := f x + g x359 have hsym : ∀ w ∈ S, c - w ∈ S := by360 intro w ⟨y, z, hy, hz, hyz, hw⟩361 refine ⟨z, y, hz, hy, by rw [add_comm]; exact hyz, ?_⟩362 rw [hw]; simp only [c]363 rw [← hyz, map_add_val f y z, map_add_val g y z]; abel364 have hinf : (f ⊓ g) x = c - (f ⊔ g) x := by365 have h : (f ⊓ g : OrderBoundedHom X Y) = f + g - (f ⊔ g) :=366 eq_sub_of_add_eq' ((add_comm _ _).trans (inf_add_sup f g))367 rw [h, sub_apply, add_apply']368 rw [hinf]369 have hLUB : IsLUB S ((f ⊔ g) x) := isLUB_sup_apply hx370 exact ⟨fun _ hw => sub_le_comm.mp (hLUB.1 (hsym _ hw)),371 fun _ hb => le_sub_comm.mpr372 (hLUB.2 fun _ hw => le_sub_comm.mp (hb (hsym _ hw)))⟩373374omit [VectorLattice X] in375private lemma nonneg_of_disjoint_add_eq {y z x : X}376 (hx : 0 ≤ x) (hdisj : IsVLDisjoint y z) (hsum : y + z = x) :377 0 ≤ y ∧ 0 ≤ z := by378 have habs : |y| + |z| = x := by379 calc380 |y| + |z| = |y + z| := (abs_add_of_isVLDisjoint hdisj).symm381 _ = x := by rw [hsum, abs_of_nonneg hx]382 rw [← hsum] at habs383 have hsub : (|y| - y) + (|z| - z) = 0 := by384 calc385 (|y| - y) + (|z| - z) = (|y| + |z|) - (y + z) := by abel386 _ = 0 := by rw [habs, sub_self]387 have hy' : 0 ≤ |y| - y := sub_nonneg.mpr (le_abs_self y)388 have hz' : 0 ≤ |z| - z := sub_nonneg.mpr (le_abs_self z)389 have hy0 : |y| - y = 0 := by390 apply le_antisymm391 · calc392 |y| - y ≤ (|y| - y) + (|z| - z) := le_add_of_nonneg_right hz'393 _ = 0 := hsub394 · exact hy'395 have hz0 : |z| - z = 0 := by396 rw [hy0, zero_add] at hsub397 exact hsub398 constructor399 · rw [(sub_eq_zero.mp hy0).symm]400 exact abs_nonneg y401 · rw [(sub_eq_zero.mp hz0).symm]402 exact abs_nonneg z403404private lemma isGLB_inf_apply_disjoint_zero405 [HasPrincipalProjectionProperty X]406 {f g : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x)407 (hfg0 : f ⊓ g = 0) :408 IsGLB409 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x410 ∧ w = f y + g z}411 0 := by412 let S : Set Y := {w | ∃ y z, 0 ≤ y ∧ 0 ≤ z ∧ y + z = x ∧ w = f y + g z}413 let D : Set Y := {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x ∧ w = f y + g z}414 have hf0 : (0 : OrderBoundedHom X Y) ≤ f := by415 simpa [hfg0] using (inf_le_left : f ⊓ g ≤ f)416 have hg0 : (0 : OrderBoundedHom X Y) ≤ g := by417 simpa [hfg0] using (inf_le_right : f ⊓ g ≤ g)418 have hS : IsGLB S 0 := by419 simpa only [S, hfg0, obZero_apply] using (isGLB_inf_apply (f := f) (g := g) hx)420 refine ⟨?_, ?_⟩421 · intro w hw422 rcases hw with ⟨y, z, hdisj, hyz, rfl⟩423 obtain ⟨hy, hz⟩ := nonneg_of_disjoint_add_eq hx hdisj hyz424 exact add_nonneg (le_iff.mp hf0 y hy) (le_iff.mp hg0 z hz)425 · intro b hb426 have hhalf_lb : (1 / 2 : ℝ) • b ∈ lowerBounds S := by427 intro w hw428 rcases hw with ⟨y, z, hy, hz, hyz, rfl⟩429 obtain ⟨u, v, huv, hu, hv, hu_le, hv_le, huvsum⟩ :=430 exists_disjoint_add_eq_add_of_hasPrincipalProjectionProperty hy hz431 have hbuv : b ≤ f u + g v :=432 hb ⟨u, v, huv, huvsum.trans hyz, rfl⟩433 have hfu : f u ≤ (2 : ℕ) • f y := by434 have hmono : Monotone f.toLinearMap :=435 Positive.monotone_iff.mpr (show Positive f.toLinearMap from le_iff.mp hf0)436 calc437 f u ≤ f ((2 : ℕ) • y) := hmono hu_le438 _ = (2 : ℕ) • f y := by439 change f.toLinearMap ((2 : ℕ) • y) = (2 : ℕ) • f.toLinearMap y440 rw [map_nsmul]441 have hgv : g v ≤ (2 : ℕ) • g z := by442 have hmono : Monotone g.toLinearMap :=443 Positive.monotone_iff.mpr (show Positive g.toLinearMap from le_iff.mp hg0)444 calc445 g v ≤ g ((2 : ℕ) • z) := hmono hv_le446 _ = (2 : ℕ) • g z := by447 change g.toLinearMap ((2 : ℕ) • z) = (2 : ℕ) • g.toLinearMap z448 rw [map_nsmul]449 calc450 (1 / 2 : ℝ) • b ≤ (1 / 2 : ℝ) • (f u + g v) :=451 smul_le_smul_of_nonneg_left hbuv (by positivity)452 _ ≤ (1 / 2 : ℝ) • ((2 : ℕ) • f y + (2 : ℕ) • g z) :=453 smul_le_smul_of_nonneg_left (add_le_add hfu hgv) (by positivity)454 _ = ((1 / 2 : ℝ) + (1 / 2 : ℝ)) • f y +455 (((1 / 2 : ℝ) + (1 / 2 : ℝ)) : ℝ) • g z := by456 rw [two_nsmul, two_nsmul, smul_add, smul_add, smul_add, ← add_smul, ← add_smul]457 _ = (1 : ℝ) • f y + (1 : ℝ) • g z := by458 rw [show ((1 / 2 : ℝ) + (1 / 2 : ℝ)) = 1 by norm_num]459 _ = f y + g z := by simp460 have hhalf_le : (1 / 2 : ℝ) • b ≤ 0 := hS.2 hhalf_lb461 have htwo :462 (2 : ℝ) • ((1 / 2 : ℝ) • b) ≤ (2 : ℝ) • (0 : Y) :=463 smul_le_smul_of_nonneg_left hhalf_le (show (0 : ℝ) ≤ 2 by positivity)464 simpa using htwo465466private lemma isGLB_inf_apply_disjoint_aux467 [HasPrincipalProjectionProperty X]468 {f g : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :469 IsGLB470 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x471 ∧ w = f y + g z}472 ((f ⊓ g) x) := by473 let h : OrderBoundedHom X Y := f ⊓ g474 let f' : OrderBoundedHom X Y := f - h475 let g' : OrderBoundedHom X Y := g - h476 let D' : Set Y := {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x ∧ w = f' y + g' z}477 have hf'0 : (0 : OrderBoundedHom X Y) ≤ f' := by478 refine le_iff.mpr ?_479 intro y hy480 dsimp [f', h]481 rw [sub_apply]482 exact sub_nonneg.mpr (le_iff.mp inf_le_left y hy)483 have hg'0 : (0 : OrderBoundedHom X Y) ≤ g' := by484 refine le_iff.mpr ?_485 intro y hy486 dsimp [g', h]487 rw [sub_apply]488 exact sub_nonneg.mpr (le_iff.mp inf_le_right y hy)489 have hdisj' : IsVLDisjoint f' g' := by490 dsimp [f', g', h]491 exact isVLDisjoint_sub_inf f g492 have hfg'0 : f' ⊓ g' = 0 :=493 inf_eq_zero_of_isVLDisjoint hf'0 hg'0 hdisj'494 have hD' : IsGLB D' 0 :=495 isGLB_inf_apply_disjoint_zero (f := f') (g := g') hx hfg'0496 have hset :497 ((fun w => h x + w) '' D') =498 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x499 ∧ w = f y + g z} := by500 ext w501 constructor502 · rintro ⟨w', ⟨y, z, hdisj, hyz, hw'⟩, rfl⟩503 refine ⟨y, z, hdisj, hyz, ?_⟩504 rw [hw']505 dsimp [f', g', h]506 rw [sub_apply, sub_apply, ← hyz, map_add_val (f ⊓ g) y z]507 abel508 · rintro ⟨y, z, hdisj, hyz, rfl⟩509 refine ⟨f' y + g' z, ⟨y, z, hdisj, hyz, rfl⟩, ?_⟩510 dsimp [f', g', h]511 rw [sub_apply, sub_apply, ← hyz, map_add_val (f ⊓ g) y z]512 abel513 rw [← hset]514 simpa [h] using isGLB_const_add (h x) hD'515516/-- **Disjoint Riesz-Kantorovich formula for the supremum.** If `X` has the517Principal Projection Property, then for `x ≥ 0` the value `(f ⊔ g) x` is the518supremum of `f y + g z` over all disjoint decompositions `x = y + z`. -/519theorem isLUB_sup_apply_disjoint [HasPrincipalProjectionProperty X]520 {f g : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :521 IsLUB522 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x523 ∧ w = f y + g z}524 ((f ⊔ g) x) := by525 have hneg :526 IsGLB527 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x528 ∧ w = (-f) y + (-g) z}529 (((-f) ⊓ (-g)) x) :=530 isGLB_inf_apply_disjoint_aux (f := -f) (g := -g) hx531 have hval : (((-f) ⊓ (-g)) x) = -((f ⊔ g) x) := by532 rw [show ((-f) ⊓ (-g) : OrderBoundedHom X Y) = -(f ⊔ g) by rw [neg_sup], neg_apply']533 refine ⟨?_, ?_⟩534 · rintro w ⟨y, z, hdisj, hyz, rfl⟩535 have hw :536 - (f y + g z) ∈537 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x538 ∧ w = (-f) y + (-g) z} := by539 refine ⟨y, z, hdisj, hyz, ?_⟩540 rw [neg_apply', neg_apply']541 abel542 have hle := hneg.1 hw543 rw [hval] at hle544 exact neg_le_neg_iff.mp hle545 · intro u hu546 have hulb :547 -u ∈ lowerBounds548 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x549 ∧ w = (-f) y + (-g) z} := by550 rintro _ ⟨y, z, hdisj, hyz, rfl⟩551 have hle : f y + g z ≤ u := hu ⟨y, z, hdisj, hyz, rfl⟩552 simpa [neg_apply', neg_add, add_comm, add_left_comm, add_assoc]553 using (neg_le_neg hle)554 have hle := hneg.2 hulb555 rw [hval] at hle556 exact neg_le_neg_iff.mp hle557558/-- **Disjoint Riesz-Kantorovich formula for the infimum.** If `X` has the559Principal Projection Property, then for `x ≥ 0` the value `(f ⊓ g) x` is the560infimum of `f y + g z` over all disjoint decompositions `x = y + z`. -/561theorem isGLB_inf_apply_disjoint [HasPrincipalProjectionProperty X]562 {f g : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :563 IsGLB564 {w | ∃ y z, IsVLDisjoint y z ∧ y + z = x565 ∧ w = f y + g z}566 ((f ⊓ g) x) := by567 exact isGLB_inf_apply_disjoint_aux hx568569/-- The modulus at a positive element. -/570theorem isLUB_abs_apply571 {f : OrderBoundedHom X Y} {x : X} (hx : 0 ≤ x) :572 IsLUB {w | ∃ y, |y| ≤ x ∧ w = |f y|}573 (|f| x) := by574 have habs_val : |f| x = f⁺ x + f⁻ x := by575 have h : (|f| : OrderBoundedHom X Y) = f⁺ + f⁻ :=576 (posPart_add_negPart f).symm577 rw [h]; exact add_apply' f⁺ f⁻ x578 constructor579 · -- Upper bound: |f y| ≤ |f| x for |y| ≤ x580 intro w ⟨y, hyx, hw⟩581 rw [hw, habs_val]582 have hPP := isLUB_posPart_apply (f := f) hx583 have hNP := isLUB_negPart_apply (f := f) hx584 have hpos_le : y⁺ ≤ x :=585 (sup_le (le_abs_self y) (abs_nonneg y)).trans hyx586 have hneg_le : y⁻ ≤ x :=587 (sup_le (neg_le_abs y) (abs_nonneg y)).trans hyx588 have hfy : f y = f y⁺ - f y⁻ := by589 rw [← map_sub_val]; congr 1; exact (posPart_sub_negPart y).symm590 have hfyle : f y ≤ f⁺ x + f⁻ x := by591 rw [hfy, sub_eq_add_neg]592 exact add_le_add593 (hPP.1 ⟨y⁺, posPart_nonneg y, hpos_le, rfl⟩)594 (hNP.1 ⟨y⁻, negPart_nonneg y, hneg_le, rfl⟩)595 have hnfyle : -(f y) ≤ f⁺ x + f⁻ x := by596 rw [hfy, neg_sub, sub_eq_add_neg]597 exact add_le_add598 (hPP.1 ⟨y⁻, negPart_nonneg y, hneg_le, rfl⟩)599 (hNP.1 ⟨y⁺, posPart_nonneg y, hpos_le, rfl⟩)600 exact sup_le hfyle hnfyle601 · -- LUB: any upper bound u of B satisfies |f| x ≤ u602 intro u hu603 change (f ⊔ (-f : OrderBoundedHom X Y)) x ≤ u604 have hLUB : IsLUB _ ((f ⊔ (-f : OrderBoundedHom X Y)) x) :=605 isLUB_sup_apply hx606 exact hLUB.2 fun w ⟨a, b, ha, hb, hab, hw⟩ => by607 have habsle : |a - b| ≤ x :=608 sup_le609 ((sub_le_self a hb).trans (hab ▸ le_add_of_nonneg_right hb))610 ((neg_sub a b ▸ (sub_le_self b ha).trans611 (hab ▸ le_add_of_nonneg_left ha)))612 have hweq : w = f (a - b) := by613 rw [hw, neg_apply', map_sub_val]; abel614 rw [hweq]615 exact (le_abs_self _).trans (hu ⟨a - b, habsle, rfl⟩)616617/-! ### Dual Riesz-Kantorovich formulas618619The **dual** Riesz-Kantorovich formulas are companions to those above: instead620of computing the lattice operations of varying operators at a fixed positive621element of `X`, they fix a positive operator `f : X → Y` and describe `f`622applied to a lattice expression in `X` (`x⁺`, `x ⊔ y`, `|x|`, ...) as a623supremum or infimum taken over the order interval `[0, f]` of operators624dominated by `f`.625-/626627/-! #### Witness operator construction628629For a positive operator `f` and a positive element `x₀`, we build an operator630`wit f x₀` with `0 ≤ wit f x₀ ≤ f`, equal to `f` at `x₀`, and vanishing on631elements disjoint from `x₀`. Concretely we set632`wit f x₀ y = sup_n f (y ⊓ n • x₀)` on the positive cone and extend linearly. -/633634635private lemma f_mono_of_nonneg {f : OrderBoundedHom X Y}636 (hf : (0 : OrderBoundedHom X Y) ≤ f) : Monotone f.toLinearMap :=637 Positive.monotone_iff.mpr fun y hy => by638 have := le_iff.mp hf y hy639 simpa only [obZero_apply, obToLinearMap_apply] using this640641642private lemma f_apply_nonneg {f : OrderBoundedHom X Y}643 (hf : (0 : OrderBoundedHom X Y) ≤ f) {y : X} (hy : 0 ≤ y) : 0 ≤ f y := by644 have := le_iff.mp hf y hy645 simpa only [obZero_apply] using this646647/-- The value of the witness operator on the positive cone:648`witFun f x₀ y = sup_n f (y ⊓ n • x₀)`. Defaults to `0` outside the regime where649the supremum exists. -/650private noncomputable def witFun (f : OrderBoundedHom X Y) (x₀ y : X) : Y :=651 sSup (Set.range fun n : ℕ => f (y ⊓ n • x₀))652653private lemma witFun_isLUB {f : OrderBoundedHom X Y}654 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}655 (_hx₀ : 0 ≤ x₀) (_hy : 0 ≤ y) :656 IsLUB (Set.range fun n : ℕ => f (y ⊓ n • x₀)) (witFun f x₀ y) := by657 refine isLUB_csSup ⟨_, 0, rfl⟩ ⟨f y, ?_⟩658 rintro _ ⟨n, rfl⟩659 exact f_mono_of_nonneg hf inf_le_left660661private lemma witFun_le_f {f : OrderBoundedHom X Y}662 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}663 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) : witFun f x₀ y ≤ f y := by664 apply (witFun_isLUB hf hx₀ hy).2665 rintro _ ⟨n, rfl⟩666 exact f_mono_of_nonneg hf inf_le_left667668private lemma witFun_nonneg {f : OrderBoundedHom X Y}669 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}670 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) : 0 ≤ witFun f x₀ y := by671 refine (witFun_isLUB hf hx₀ hy).1 ⟨0, ?_⟩672 change f (y ⊓ (0 : ℕ) • x₀) = 0673 rw [zero_nsmul, inf_of_le_right hy]674 exact map_zero f.toLinearMap675676private lemma witFun_eq_at {f : OrderBoundedHom X Y}677 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :678 witFun f x₀ x₀ = f x₀ := by679 refine le_antisymm (witFun_le_f hf hx₀ hx₀) ?_680 refine (witFun_isLUB hf hx₀ hx₀).1 ⟨1, ?_⟩681 change f (x₀ ⊓ (1 : ℕ) • x₀) = f x₀682 rw [one_nsmul, inf_idem]683684private lemma witFun_zero_of_disjoint {f : OrderBoundedHom X Y}685 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}686 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) (hd : y ⊓ x₀ = 0) :687 witFun f x₀ y = 0 := by688 have hyn : ∀ n : ℕ, y ⊓ n • x₀ = 0 := by689 intro n690 induction n with691 | zero => rw [zero_nsmul, inf_of_le_right hy]692 | succ n ih =>693 have hle : y ⊓ (n + 1) • x₀ ≤ y ⊓ (n • x₀) + y ⊓ x₀ := by694 rw [succ_nsmul]695 exact inf_le_inf_add_inf_of_nonneg y (n • x₀) x₀ hy696 (nsmul_nonneg hx₀ n) hx₀697 rw [ih, hd, add_zero] at hle698 exact le_antisymm hle (le_inf hy (nsmul_nonneg hx₀ (n + 1)))699 refine le_antisymm ?_ (witFun_nonneg hf hx₀ hy)700 apply (witFun_isLUB hf hx₀ hy).2701 rintro _ ⟨n, rfl⟩702 change f (y ⊓ n • x₀) ≤ 0703 rw [hyn n]704 exact (map_zero f.toLinearMap).le705706private lemma witFun_add {f : OrderBoundedHom X Y}707 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y₁ y₂ : X}708 (hx₀ : 0 ≤ x₀) (hy₁ : 0 ≤ y₁) (hy₂ : 0 ≤ y₂) :709 witFun f x₀ (y₁ + y₂) = witFun f x₀ y₁ + witFun f x₀ y₂ := by710 refine le_antisymm ?_ ?_711 · apply (witFun_isLUB hf hx₀ (add_nonneg hy₁ hy₂)).2712 rintro _ ⟨n, rfl⟩713 have hznn : 0 ≤ (y₁ + y₂) ⊓ n • x₀ :=714 le_inf (add_nonneg hy₁ hy₂) (nsmul_nonneg hx₀ n)715 have hzy : (y₁ + y₂) ⊓ n • x₀ ≤ y₁ + y₂ := inf_le_left716 obtain ⟨z₁, z₂, hz₁nn, hz₁y₁, hz₂nn, hz₂y₂, hzeq⟩ :=717 riesz_decomposition (x := (y₁ + y₂) ⊓ n • x₀) y₁ y₂ hznn hy₁ hy₂ hzy718 have hz_le : (y₁ + y₂) ⊓ n • x₀ ≤ n • x₀ := inf_le_right719 have hz₁_nx : z₁ ≤ n • x₀ :=720 ((le_add_of_nonneg_right hz₂nn).trans hzeq.symm.le).trans hz_le721 have hz₂_nx : z₂ ≤ n • x₀ :=722 ((le_add_of_nonneg_left hz₁nn).trans hzeq.symm.le).trans hz_le723 have hz₁_inf : z₁ ≤ y₁ ⊓ n • x₀ := le_inf hz₁y₁ hz₁_nx724 have hz₂_inf : z₂ ≤ y₂ ⊓ n • x₀ := le_inf hz₂y₂ hz₂_nx725 calc f ((y₁ + y₂) ⊓ n • x₀)726 = f (z₁ + z₂) := by rw [hzeq]727 _ = f z₁ + f z₂ := map_add f.toLinearMap z₁ z₂728 _ ≤ f (y₁ ⊓ n • x₀) + f (y₂ ⊓ n • x₀) :=729 add_le_add (f_mono_of_nonneg hf hz₁_inf) (f_mono_of_nonneg hf hz₂_inf)730 _ ≤ witFun f x₀ y₁ + witFun f x₀ y₂ :=731 add_le_add ((witFun_isLUB hf hx₀ hy₁).1 ⟨n, rfl⟩)732 ((witFun_isLUB hf hx₀ hy₂).1 ⟨n, rfl⟩)733 · have step1 : ∀ n m : ℕ,734 f (y₁ ⊓ n • x₀) + f (y₂ ⊓ m • x₀) ≤ witFun f x₀ (y₁ + y₂) := by735 intro n m736 have hsum : (y₁ ⊓ n • x₀) + (y₂ ⊓ m • x₀) ≤ (y₁ + y₂) ⊓ ((n + m) • x₀) := by737 refine le_inf (add_le_add inf_le_left inf_le_left) ?_738 rw [add_nsmul]; exact add_le_add inf_le_right inf_le_right739 calc f (y₁ ⊓ n • x₀) + f (y₂ ⊓ m • x₀)740 = f ((y₁ ⊓ n • x₀) + (y₂ ⊓ m • x₀)) :=741 (map_add f.toLinearMap _ _).symm742 _ ≤ f ((y₁ + y₂) ⊓ (n + m) • x₀) := f_mono_of_nonneg hf hsum743 _ ≤ witFun f x₀ (y₁ + y₂) :=744 (witFun_isLUB hf hx₀ (add_nonneg hy₁ hy₂)).1 ⟨n + m, rfl⟩745 have step2 : ∀ m : ℕ,746 witFun f x₀ y₁ + f (y₂ ⊓ m • x₀) ≤ witFun f x₀ (y₁ + y₂) := by747 intro m748 have hub : witFun f x₀ (y₁ + y₂) - f (y₂ ⊓ m • x₀) ∈749 upperBounds (Set.range fun n : ℕ => f (y₁ ⊓ n • x₀)) := by750 rintro _ ⟨n, rfl⟩751 exact le_sub_iff_add_le.mpr (step1 n m)752 exact le_sub_iff_add_le.mp ((witFun_isLUB hf hx₀ hy₁).2 hub)753 have hub : witFun f x₀ (y₁ + y₂) - witFun f x₀ y₁ ∈754 upperBounds (Set.range fun n : ℕ => f (y₂ ⊓ n • x₀)) := by755 rintro _ ⟨m, rfl⟩756 rw [le_sub_iff_add_le, add_comm]; exact step2 m757 have h := (witFun_isLUB hf hx₀ hy₂).2 hub758 have h2 := le_sub_iff_add_le.mp h759 rwa [add_comm] at h2760761/-- The witness linear map for `f` and `x₀ ≥ 0`. -/762private noncomputable def witLin {f : OrderBoundedHom X Y}763 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :764 X →ₗ[ℝ] Y := by765 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice766 exact Positive.extension767 (fun y hy => witFun_nonneg hf hx₀ hy)768 (fun y₁ y₂ hy₁ hy₂ => witFun_add hf hx₀ hy₁ hy₂)769770private lemma witLin_apply_nonneg {f : OrderBoundedHom X Y}771 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}772 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) : witLin hf hx₀ y = witFun f x₀ y := by773 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice774 exact Positive.extension_nonneg _ _ hy775776private lemma witLin_positive {f : OrderBoundedHom X Y}777 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :778 Positive (witLin hf hx₀) := by779 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice780 exact Positive.extension_positive _ _781782/-- The witness operator as an `OrderBoundedHom`. -/783private noncomputable def witOp {f : OrderBoundedHom X Y}784 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :785 OrderBoundedHom X Y :=786 ⟨witLin hf hx₀, Positive.isOrderBounded (witLin_positive hf hx₀)⟩787788private lemma witOp_apply {f : OrderBoundedHom X Y}789 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) (y : X) :790 witOp hf hx₀ y = witLin hf hx₀ y := rfl791792private lemma witOp_nonneg {f : OrderBoundedHom X Y}793 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :794 (0 : OrderBoundedHom X Y) ≤ witOp hf hx₀ :=795 le_iff.mpr fun y hy => by796 have h := witLin_positive hf hx₀ y hy797 change (0 : Y) ≤ witLin hf hx₀ y at h798 simpa only [obZero_apply, witOp_apply] using h799800private lemma witOp_le_f {f : OrderBoundedHom X Y}801 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :802 witOp hf hx₀ ≤ f :=803 le_iff.mpr fun y hy => by804 change witLin hf hx₀ y ≤ f y805 rw [witLin_apply_nonneg hf hx₀ hy]806 exact witFun_le_f hf hx₀ hy807808private lemma witOp_apply_self {f : OrderBoundedHom X Y}809 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :810 witOp hf hx₀ x₀ = f x₀ := by811 change witLin hf hx₀ x₀ = f x₀812 rw [witLin_apply_nonneg hf hx₀ hx₀, witFun_eq_at hf hx₀]813814private lemma witOp_apply_disjoint {f : OrderBoundedHom X Y}815 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X} (hx₀ : 0 ≤ x₀)816 (hy : 0 ≤ y) (hd : y ⊓ x₀ = 0) : witOp hf hx₀ y = 0 := by817 change witLin hf hx₀ y = 0818 rw [witLin_apply_nonneg hf hx₀ hy, witFun_zero_of_disjoint hf hx₀ hy hd]819820/-- The witness operator at `x = x⁺ - x⁻` recovers `f x⁺`. -/821private lemma witOp_apply_eq_posPart {f : OrderBoundedHom X Y}822 (hf : (0 : OrderBoundedHom X Y) ≤ f) (x : X) :823 witOp hf (posPart_nonneg x) x = f x⁺ := by824 have hlin : (witOp hf (posPart_nonneg x)).toLinearMap x =825 (witOp hf (posPart_nonneg x)).toLinearMap x⁺ -826 (witOp hf (posPart_nonneg x)).toLinearMap x⁻ := by827 rw [← map_sub, posPart_sub_negPart]828 change (witOp hf (posPart_nonneg x)).toLinearMap x = f x⁺829 rw [hlin]830 have h1 : (witOp hf (posPart_nonneg x)).toLinearMap x⁺ = f x⁺ :=831 witOp_apply_self hf (posPart_nonneg x)832 have h2 : (witOp hf (posPart_nonneg x)).toLinearMap x⁻ = 0 := by833 apply witOp_apply_disjoint hf (posPart_nonneg x) (negPart_nonneg x)834 rw [inf_comm]; exact posPart_inf_negPart_eq_zero x835 rw [h1, h2, sub_zero]836837/-! #### Dual Riesz–Kantorovich theorems -/838839/-- **Dual Riesz-Kantorovich for the positive part.** For a positive order840bounded operator `f : X → Y` and an arbitrary `x : X`, the value `f x⁺` is the841supremum of `g x` taken over all order bounded operators `g` with `0 ≤ g ≤ f`.842-/843theorem isLUB_apply_posPart {f : OrderBoundedHom X Y}844 (hf : (0 : OrderBoundedHom X Y) ≤ f) (x : X) :845 IsLUB {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = g x}846 (f x⁺) := by847 refine ⟨?_, ?_⟩848 · rintro _ ⟨g, hg0, hgf, rfl⟩849 have hg_neg : 0 ≤ g x⁻ := f_apply_nonneg hg0 (negPart_nonneg x)850 have key : g x = g x⁺ - g x⁻ := by851 change g.toLinearMap x = g.toLinearMap x⁺ - g.toLinearMap x⁻852 rw [← map_sub, posPart_sub_negPart]853 rw [key]854 exact (sub_le_self _ hg_neg).trans (le_iff.mp hgf x⁺ (posPart_nonneg x))855 · intro u hu856 have hwit_in :857 witOp hf (posPart_nonneg x) x ∈858 {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = g x} :=859 ⟨witOp hf (posPart_nonneg x), witOp_nonneg hf (posPart_nonneg x),860 witOp_le_f hf (posPart_nonneg x), rfl⟩861 have hub := hu hwit_in862 rwa [witOp_apply_eq_posPart hf x] at hub863864/-- **Dual Riesz-Kantorovich for the negative part.** For a positive order865bounded operator `f` and `x : X`, `f x⁻ = sup {-(g x) | 0 ≤ g ≤ f}`. -/866theorem isLUB_apply_negPart {f : OrderBoundedHom X Y}867 (hf : (0 : OrderBoundedHom X Y) ≤ f) (x : X) :868 IsLUB {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = -(g x)}869 (f x⁻) := by870 have hpp := isLUB_apply_posPart hf (-x)871 rw [posPart_neg] at hpp872 have hgneg : ∀ g : OrderBoundedHom X Y, g (-x) = -(g x) := fun g => by873 change g.toLinearMap (-x) = -(g.toLinearMap x); rw [map_neg]874 refine ⟨?_, ?_⟩875 · rintro _ ⟨g, hg0, hgf, rfl⟩876 have hmem : g (-x) ∈877 {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = g (-x)} :=878 ⟨g, hg0, hgf, rfl⟩879 have h1 := hpp.1 hmem880 rw [hgneg] at h1; exact h1881 · intro u hu882 apply hpp.2883 rintro _ ⟨g, hg0, hgf, rfl⟩884 have hin : -(g x) ∈885 {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = -(g x)} :=886 ⟨g, hg0, hgf, rfl⟩887 have h1 := hu hin888 rw [hgneg]; exact h1889890/-- **Dual Riesz-Kantorovich for the supremum.** For a positive order bounded891operator `f` and `x y : X`,892`f (x ⊔ y) = sup {g x + (f - g) y | 0 ≤ g ≤ f}`. -/893theorem isLUB_apply_sup {f : OrderBoundedHom X Y}894 (hf : (0 : OrderBoundedHom X Y) ≤ f) (x y : X) :895 IsLUB {w | ∃ g : OrderBoundedHom X Y,896 0 ≤ g ∧ g ≤ f ∧ w = g x + (f - g) y}897 (f (x ⊔ y)) := by898 -- Use x ⊔ y = y + (x - y)⁺899 have hxy : (x ⊔ y) = y + (x - y)⁺ := by900 rw [posPart_def, add_sup, add_sub_cancel, add_zero, sup_comm]901 have hfxy : f (x ⊔ y) = f y + f ((x - y)⁺) := by902 rw [hxy]; exact map_add_val f y _903 rw [hfxy]904 refine ⟨?_, ?_⟩905 · rintro _ ⟨g, hg0, hgf, rfl⟩906 have hgxy : g x + (f - g) y = f y + g (x - y) := by907 rw [sub_apply, map_sub_val g]; abel908 rw [hgxy]909 have hgneg : 0 ≤ g (x - y)⁻ := f_apply_nonneg hg0 (negPart_nonneg _)910 have hgsplit : g (x - y) = g (x - y)⁺ - g (x - y)⁻ := by911 change g.toLinearMap (x - y) = g.toLinearMap (x - y)⁺ - g.toLinearMap (x - y)⁻912 rw [← map_sub, posPart_sub_negPart]913 have h1 : g (x - y) ≤ g (x - y)⁺ := by rw [hgsplit]; exact sub_le_self _ hgneg914 have h2 : g (x - y)⁺ ≤ f (x - y)⁺ := le_iff.mp hgf _ (posPart_nonneg _)915 exact add_le_add (le_refl (f y)) (h1.trans h2)916 · intro u hu917 set g := witOp hf (posPart_nonneg (x - y)) with hgdef918 have hg0 : (0 : OrderBoundedHom X Y) ≤ g := witOp_nonneg hf _919 have hgf : g ≤ f := witOp_le_f hf _920 have hgxy : g (x - y) = f (x - y)⁺ := witOp_apply_eq_posPart hf (x - y)921 have hin : g x + (f - g) y ∈922 {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = g x + (f - g) y} :=923 ⟨g, hg0, hgf, rfl⟩924 have hub := hu hin925 have hcalc : g x + (f - g) y = f y + f (x - y)⁺ := by926 have h0 : g x + (f - g) y = f y + g (x - y) := by927 rw [sub_apply, map_sub_val g]; abel928 rw [h0, hgxy]929 rw [hcalc] at hub; exact hub930931/-- **Dual Riesz-Kantorovich for the infimum.** For a positive order bounded932operator `f` and `x y : X`,933`f (x ⊓ y) = inf {g x + (f - g) y | 0 ≤ g ≤ f}`. -/934theorem isGLB_apply_inf {f : OrderBoundedHom X Y}935 (hf : (0 : OrderBoundedHom X Y) ≤ f) (x y : X) :936 IsGLB {w | ∃ g : OrderBoundedHom X Y,937 0 ≤ g ∧ g ≤ f ∧ w = g x + (f - g) y}938 (f (x ⊓ y)) := by939 -- Use x ⊓ y = x + y - x ⊔ y. The set is symmetric: replacing g by f - g sends940 -- g x + (f-g) y to (f-g) x + g y, and the sum (g x + (f-g) y) + ((f-g) x + g y)941 -- = f x + f y. So the inf set is the reflection of the sup set about (f x + f y)/2.942 set S : Set Y := {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = g x + (f - g) y}943 set c : Y := f x + f y with hcdef944 have hsym : ∀ w ∈ S, c - w ∈ S := by945 rintro _ ⟨g, hg0, hgf, rfl⟩946 refine ⟨f - g, sub_nonneg.mpr hgf, sub_le_self f hg0, ?_⟩947 rw [sub_sub_cancel, sub_apply, sub_apply]948 change f x + f y - (g x + (f y - g y)) = (f x - g x) + g y949 abel950 have hsup : IsLUB S (f (x ⊔ y)) := isLUB_apply_sup hf x y951 have hadd : f (x ⊓ y) + f (x ⊔ y) = c := by952 change f.toLinearMap (x ⊓ y) + f.toLinearMap (x ⊔ y) = f.toLinearMap x + f.toLinearMap y953 rw [← map_add f.toLinearMap, inf_add_sup, map_add]954 have hinf : f (x ⊓ y) = c - f (x ⊔ y) := eq_sub_of_add_eq hadd955 rw [hinf]956 refine ⟨?_, ?_⟩957 · intro w hw958 exact sub_le_comm.mp (hsup.1 (hsym w hw))959 · intro b hb960 have hub : ∀ w ∈ S, w ≤ c - b := fun w hw =>961 le_sub_comm.mp (hb (hsym w hw))962 exact le_sub_comm.mpr (hsup.2 hub)963964965private lemma sum_apply_finset {ι : Type*} (s : Finset ι)966 (g : ι → OrderBoundedHom X Y) (x : X) :967 (∑ i ∈ s, g i) x = ∑ i ∈ s, g i x := by968 induction s using Finset.cons_induction with969 | empty =>970 change (0 : X →ₗ[ℝ] Y) x = 0971 simp972 | cons a s ha ih =>973 rw [Finset.sum_cons, Finset.sum_cons, add_apply', ih]974975/-- **Dual Riesz-Kantorovich for finite suprema.** For a positive order bounded976operator `f` and a non-empty finite family `x`, `f` applied to the supremum of977the family is the supremum of the sums `∑ i ∈ s, g i (x i)`, where the positive978operators `g i` form a finite decomposition of `f`. -/979theorem isLUB_apply_finset_sup {ι : Type*} {s : Finset ι} (hs : s.Nonempty)980 {f : OrderBoundedHom X Y} (hf : (0 : OrderBoundedHom X Y) ≤ f) (x : ι → X) :981 IsLUB {w | ∃ g : ι → OrderBoundedHom X Y,982 (∀ i ∈ s, (0 : OrderBoundedHom X Y) ≤ g i) ∧983 (∑ i ∈ s, g i = f) ∧984 w = ∑ i ∈ s, g i (x i)}985 (f (s.sup' hs x)) := by986 classical987 revert f x988 induction hs using Finset.Nonempty.cons_induction with989 | singleton a =>990 intro f hf x991 refine ⟨?_, ?_⟩992 · rintro _ ⟨g, _hg0, hgsum, rfl⟩993 exact le_of_eq (by994 simpa using congrArg (fun h : OrderBoundedHom X Y => h (x a)) hgsum)995 · intro u hu996 exact hu ⟨fun _ => f, by simpa using hf, by simp, by simp⟩997 | cons a t ha ht ih =>998 intro f hf x999 refine ⟨?_, ?_⟩1000 · rintro _ ⟨g, hg0, hgsum, rfl⟩1001 let x₀ := (Finset.cons a t ha).sup' (Finset.cons_nonempty ha) x1002 calc1003 (∑ i ∈ Finset.cons a t ha, g i (x i)) ≤1004 ∑ i ∈ Finset.cons a t ha, g i x₀ := by1005 refine Finset.sum_le_sum fun i hi => ?_1006 exact f_mono_of_nonneg (hg0 i hi) (Finset.le_sup' (f := x) hi)1007 _ = f x₀ := by rw [← sum_apply_finset, hgsum]1008 · intro u hu1009 rw [Finset.sup'_cons ht x]1010 have hsup := isLUB_apply_sup hf (x a) (t.sup' ht x)1011 apply hsup.21012 rintro _ ⟨g, hg0, hgf, rfl⟩1013 have hrest := ih (f := f - g) (sub_nonneg.mpr hgf) x1014 have hle : (f - g) (t.sup' ht x) ≤ u - g (x a) := by1015 apply hrest.21016 rintro _ ⟨k, hk0, hksum, rfl⟩1017 rw [le_sub_iff_add_le]1018 let G : ι → OrderBoundedHom X Y := fun i => if i = a then g else k i1019 have hG0 : ∀ i ∈ Finset.cons a t ha, (0 : OrderBoundedHom X Y) ≤ G i := by1020 intro i hi1021 rcases Finset.mem_cons.mp hi with rfl | hit1022 · simp [G, hg0]1023 · have hia : i ≠ a := fun h => ha (h ▸ hit)1024 simp [G, hia, hk0 i hit]1025 have hGsum : ∑ i ∈ Finset.cons a t ha, G i = f := by1026 rw [Finset.sum_cons]1027 have hsum_t : ∑ i ∈ t, G i = f - g := by1028 rw [← hksum]1029 refine Finset.sum_congr rfl fun i hit => ?_1030 have hia : i ≠ a := fun h => ha (h ▸ hit)1031 simp [G, hia]1032 rw [hsum_t]1033 rw [show G a = g by simp [G]]1034 abel1035 have hfull : (∑ i ∈ Finset.cons a t ha, G i (x i)) ≤ u :=1036 hu ⟨G, hG0, hGsum, rfl⟩1037 rw [Finset.sum_cons] at hfull1038 have hsum_t : ∑ i ∈ t, G i (x i) = ∑ i ∈ t, k i (x i) := by1039 refine Finset.sum_congr rfl fun i hit => ?_1040 have hia : i ≠ a := fun h => ha (h ▸ hit)1041 simp [G, hia]1042 rw [hsum_t] at hfull1043 simpa [G, add_comm] using hfull1044 have := le_sub_iff_add_le.mp hle1045 rwa [add_comm] at this10461047/-- **Dual Riesz-Kantorovich for finite infima.** For a positive order bounded1048operator `f` and a non-empty finite family `x`, `f` applied to the infimum of1049the family is the infimum of the sums `∑ i ∈ s, g i (x i)`, where the positive1050operators `g i` form a finite decomposition of `f`. -/1051theorem isGLB_apply_finset_inf {ι : Type*} {s : Finset ι} (hs : s.Nonempty)1052 {f : OrderBoundedHom X Y} (hf : (0 : OrderBoundedHom X Y) ≤ f) (x : ι → X) :1053 IsGLB {w | ∃ g : ι → OrderBoundedHom X Y,1054 (∀ i ∈ s, (0 : OrderBoundedHom X Y) ≤ g i) ∧1055 (∑ i ∈ s, g i = f) ∧1056 w = ∑ i ∈ s, g i (x i)}1057 (f (s.inf' hs x)) := by1058 classical1059 revert f x1060 induction hs using Finset.Nonempty.cons_induction with1061 | singleton a =>1062 intro f hf x1063 refine ⟨?_, ?_⟩1064 · rintro _ ⟨g, _hg0, hgsum, rfl⟩1065 exact ge_of_eq (by1066 simpa using congrArg (fun h : OrderBoundedHom X Y => h (x a)) hgsum)1067 · intro b hb1068 exact hb ⟨fun _ => f, by simpa using hf, by simp, by simp⟩1069 | cons a t ha ht ih =>1070 intro f hf x1071 refine ⟨?_, ?_⟩1072 · rintro _ ⟨g, hg0, hgsum, rfl⟩1073 rw [Finset.inf'_cons ht x]1074 have hrest_nn : 0 ≤ ∑ i ∈ t, g i :=1075 Finset.sum_nonneg fun i hi => hg0 i (Finset.mem_cons.mpr (Or.inr hi))1076 have hgaf : g a ≤ f := by1077 rw [← hgsum, Finset.sum_cons]1078 exact le_add_of_nonneg_right hrest_nn1079 have hrest_sum : ∑ i ∈ t, g i = f - g a := by1080 have hsum := hgsum1081 rw [Finset.sum_cons] at hsum1082 rw [← hsum]1083 abel_nf1084 have hrest := ih (f := f - g a) (sub_nonneg.mpr hgaf) x1085 have hrest_le : (f - g a) (t.inf' ht x) ≤ ∑ i ∈ t, g i (x i) :=1086 hrest.1 ⟨g, fun i hi => hg0 i (Finset.mem_cons.mpr (Or.inr hi)), hrest_sum, rfl⟩1087 have hbin := isGLB_apply_inf hf (x a) (t.inf' ht x)1088 calc1089 f (x a ⊓ t.inf' ht x) ≤ g a (x a) + (f - g a) (t.inf' ht x) :=1090 hbin.1 ⟨g a, hg0 a (Finset.mem_cons_self a t), hgaf, rfl⟩1091 _ ≤ g a (x a) + ∑ i ∈ t, g i (x i) := by1092 gcongr1093 _ = ∑ i ∈ Finset.cons a t ha, g i (x i) := by rw [Finset.sum_cons]1094 · intro b hb1095 rw [Finset.inf'_cons ht x]1096 have hinf := isGLB_apply_inf hf (x a) (t.inf' ht x)1097 apply hinf.21098 rintro _ ⟨g, hg0, hgf, rfl⟩1099 have hrest := ih (f := f - g) (sub_nonneg.mpr hgf) x1100 have hle : b - g (x a) ≤ (f - g) (t.inf' ht x) := by1101 apply hrest.21102 rintro _ ⟨k, hk0, hksum, rfl⟩1103 let G : ι → OrderBoundedHom X Y := fun i => if i = a then g else k i1104 have hG0 : ∀ i ∈ Finset.cons a t ha, (0 : OrderBoundedHom X Y) ≤ G i := by1105 intro i hi1106 rcases Finset.mem_cons.mp hi with rfl | hit1107 · simp [G, hg0]1108 · have hia : i ≠ a := fun h => ha (h ▸ hit)1109 simp [G, hia, hk0 i hit]1110 have hGsum : ∑ i ∈ Finset.cons a t ha, G i = f := by1111 rw [Finset.sum_cons]1112 have hsum_t : ∑ i ∈ t, G i = f - g := by1113 rw [← hksum]1114 refine Finset.sum_congr rfl fun i hit => ?_1115 have hia : i ≠ a := fun h => ha (h ▸ hit)1116 simp [G, hia]1117 rw [hsum_t]1118 rw [show G a = g by simp [G]]1119 abel1120 have hfull : b ≤ ∑ i ∈ Finset.cons a t ha, G i (x i) :=1121 hb ⟨G, hG0, hGsum, rfl⟩1122 rw [Finset.sum_cons] at hfull1123 have hsum_t : ∑ i ∈ t, G i (x i) = ∑ i ∈ t, k i (x i) := by1124 refine Finset.sum_congr rfl fun i hit => ?_1125 have hia : i ≠ a := fun h => ha (h ▸ hit)1126 simp [G, hia]1127 rw [hsum_t] at hfull1128 exact sub_le_iff_le_add.mpr (by simpa [G, add_comm] using hfull)1129 have := sub_le_iff_le_add.mp hle1130 rwa [add_comm] at this11311132/-- **Dual Riesz-Kantorovich for the modulus.** For a positive order bounded1133operator `f` and `x : X`,1134`f |x| = sup {g x - (f - g) x | 0 ≤ g ≤ f}`. -/1135theorem isLUB_apply_abs {f : OrderBoundedHom X Y}1136 (hf : (0 : OrderBoundedHom X Y) ≤ f) (x : X) :1137 IsLUB {w | ∃ g : OrderBoundedHom X Y,1138 0 ≤ g ∧ g ≤ f ∧ w = g x - (f - g) x}1139 (f |x|) := by1140 -- |x| = x⁺ + x⁻ and g x - (f - g) x = 2 g x - f x. Reduce to posPart formula.1141 have habs : |x| = x⁺ + x⁻ := (posPart_add_negPart x).symm1142 -- Note: x = x⁺ - x⁻, so f x = f x⁺ - f x⁻, and 2 f x⁺ - f x = f x⁺ + f x⁻ = f |x|.1143 have hfabs : f |x| = 2 • f x⁺ - f x := by1144 rw [habs, map_add_val]1145 have : f x = f x⁺ - f x⁻ := by rw [← map_sub_val, posPart_sub_negPart]1146 rw [this]; abel1147 rw [hfabs]1148 have hpp := isLUB_apply_posPart hf x1149 refine ⟨?_, ?_⟩1150 · rintro _ ⟨g, hg0, hgf, rfl⟩1151 have heq : g x - (f - g) x = 2 • g x - f x := by1152 rw [sub_apply, two_smul]; abel1153 rw [heq]1154 have hgx : g x ≤ f x⁺ := hpp.1 ⟨g, hg0, hgf, rfl⟩1155 have h2 : 2 • g x ≤ 2 • f x⁺ := by1156 rw [two_smul, two_smul]; exact add_le_add hgx hgx1157 exact sub_le_sub_right h2 _1158 · intro u hu1159 set g := witOp hf (posPart_nonneg x) with hgdef1160 have hg0 : (0 : OrderBoundedHom X Y) ≤ g := witOp_nonneg hf _1161 have hgf : g ≤ f := witOp_le_f hf _1162 have hgx : g x = f x⁺ := witOp_apply_eq_posPart hf x1163 have hin : g x - (f - g) x ∈1164 {w | ∃ g : OrderBoundedHom X Y, 0 ≤ g ∧ g ≤ f ∧ w = g x - (f - g) x} :=1165 ⟨g, hg0, hgf, rfl⟩1166 have hub := hu hin1167 have heq : g x - (f - g) x = 2 • f x⁺ - f x := by1168 rw [sub_apply, hgx, two_smul]; abel1169 rw [heq] at hub; exact hub11701171/-- The supremum of a non-empty upward-directed bounded above set of order1172bounded operators exists and is computed pointwise on the positive cone:1173its value at any positive `x` is the supremum of `{g x | g ∈ S}`. -/1174theorem isLUB_of_directedOn1175 {S : Set (OrderBoundedHom X Y)} (hne : S.Nonempty)1176 (hdir : DirectedOn (· ≤ ·) S) (hbdd : BddAbove S) :1177 ∃ f : OrderBoundedHom X Y, IsLUB S f ∧1178 ∀ {x : X}, 0 ≤ x →1179 IsLUB ((fun g : OrderBoundedHom X Y => g x) '' S) (f x) := by1180 classical1181 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice1182 obtain ⟨g₀, hg₀⟩ := hne1183 obtain ⟨h, hh⟩ := hbdd1184 have aux : ∀ {x : X}, 0 ≤ x →1185 ∃ s : Y, IsLUB ((fun g : OrderBoundedHom X Y => g x - g₀ x) '' S) s := by1186 intro x hx1187 refine ⟨_, isLUB_csSup ⟨0, g₀, hg₀, sub_self _⟩ ⟨h x - g₀ x, ?_⟩⟩1188 rintro _ ⟨g, hg, rfl⟩1189 exact sub_le_sub_right (le_iff.mp (hh hg) x hx) _1190 let σ : X → Y := fun x => if hx : 0 ≤ x then (aux hx).choose else 01191 have σ_isLUB : ∀ {x : X} (hx : 0 ≤ x),1192 IsLUB ((fun g : OrderBoundedHom X Y => g x - g₀ x) '' S) (σ x) := by1193 intro x hx1194 change IsLUB _ (if hx : 0 ≤ x then (aux hx).choose else 0)1195 rw [dif_pos hx]1196 exact (aux hx).choose_spec1197 have σ_nn : ∀ x, 0 ≤ x → 0 ≤ σ x := fun x hx => by1198 have h1 := (σ_isLUB hx).1 ⟨g₀, hg₀, sub_self _⟩1199 simpa using h11200 have σ_add : ∀ x y, 0 ≤ x → 0 ≤ y → σ (x + y) = σ x + σ y := by1201 intro x y hx hy1202 refine le_antisymm ?_ ?_1203 · apply (σ_isLUB (add_nonneg hx hy)).21204 rintro _ ⟨g, hg, rfl⟩1205 change g (x + y) - g₀ (x + y) ≤ σ x + σ y1206 have hgxy : g (x + y) - g₀ (x + y) = (g x - g₀ x) + (g y - g₀ y) := by1207 rw [map_add_val g, map_add_val g₀]; abel1208 rw [hgxy]1209 exact add_le_add ((σ_isLUB hx).1 ⟨g, hg, rfl⟩)1210 ((σ_isLUB hy).1 ⟨g, hg, rfl⟩)1211 · have step1 : ∀ w₁ ∈ ((fun g : OrderBoundedHom X Y => g x - g₀ x) '' S),1212 ∀ w₂ ∈ ((fun g : OrderBoundedHom X Y => g y - g₀ y) '' S),1213 w₁ + w₂ ≤ σ (x + y) := by1214 rintro _ ⟨g₁, hg₁, rfl⟩ _ ⟨g₂, hg₂, rfl⟩1215 obtain ⟨g, hg, hg₁g, hg₂g⟩ := hdir g₁ hg₁ g₂ hg₂1216 have h1 : g₁ x - g₀ x ≤ g x - g₀ x :=1217 sub_le_sub_right (le_iff.mp hg₁g x hx) _1218 have h2 : g₂ y - g₀ y ≤ g y - g₀ y :=1219 sub_le_sub_right (le_iff.mp hg₂g y hy) _1220 have h3 : (g x - g₀ x) + (g y - g₀ y) = g (x + y) - g₀ (x + y) := by1221 rw [map_add_val g, map_add_val g₀]; abel1222 calc g₁ x - g₀ x + (g₂ y - g₀ y)1223 ≤ (g x - g₀ x) + (g y - g₀ y) := add_le_add h1 h21224 _ = g (x + y) - g₀ (x + y) := h31225 _ ≤ σ (x + y) :=1226 (σ_isLUB (add_nonneg hx hy)).1 ⟨g, hg, rfl⟩1227 have step2 : ∀ w₂ ∈ ((fun g : OrderBoundedHom X Y => g y - g₀ y) '' S),1228 σ x + w₂ ≤ σ (x + y) := by1229 intro w₂ hw₂1230 have hub : σ (x + y) - w₂ ∈ upperBounds1231 ((fun g : OrderBoundedHom X Y => g x - g₀ x) '' S) :=1232 fun w₁ hw₁ => le_sub_iff_add_le.mpr (step1 w₁ hw₁ w₂ hw₂)1233 exact le_sub_iff_add_le.mp ((σ_isLUB hx).2 hub)1234 have hub2 : σ (x + y) - σ x ∈ upperBounds1235 ((fun g : OrderBoundedHom X Y => g y - g₀ y) '' S) := by1236 intro w₂ hw₂1237 rw [le_sub_iff_add_le, add_comm]1238 exact step2 w₂ hw₂1239 have h3 := (σ_isLUB hy).2 hub21240 have := le_sub_iff_add_le.mp h31241 rwa [add_comm] at this1242 let T : X →ₗ[ℝ] Y := Positive.extension σ_nn σ_add1243 have hT_pos : Positive T := Positive.extension_positive σ_nn σ_add1244 have hT_apply : ∀ {x : X}, 0 ≤ x → T x = σ x :=1245 fun {x} hx => Positive.extension_nonneg σ_nn σ_add hx1246 let Tob : OrderBoundedHom X Y := ⟨T, hT_pos.isOrderBounded⟩1247 refine ⟨Tob + g₀, ?_, ?_⟩1248 · refine ⟨fun g hg => le_iff.mpr fun x hx => ?_,1249 fun k hk => le_iff.mpr fun x hx => ?_⟩1250 · rw [add_apply']1251 change g x ≤ T x + g₀ x1252 rw [hT_apply hx]1253 have : g x - g₀ x ≤ σ x := (σ_isLUB hx).1 ⟨g, hg, rfl⟩1254 exact sub_le_iff_le_add.mp this1255 · rw [add_apply']1256 change T x + g₀ x ≤ k x1257 rw [hT_apply hx]1258 have hub : k x - g₀ x ∈ upperBounds1259 ((fun g : OrderBoundedHom X Y => g x - g₀ x) '' S) := by1260 rintro _ ⟨g, hg, rfl⟩1261 exact sub_le_sub_right (le_iff.mp (hk hg) x hx) _1262 have h1 := (σ_isLUB hx).2 hub1263 exact le_sub_iff_add_le.mp h11264 · intro x hx1265 refine ⟨?_, ?_⟩1266 · rintro _ ⟨g, hg, rfl⟩1267 rw [add_apply']1268 change g x ≤ T x + g₀ x1269 rw [hT_apply hx]1270 have : g x - g₀ x ≤ σ x := (σ_isLUB hx).1 ⟨g, hg, rfl⟩1271 exact sub_le_iff_le_add.mp this1272 · intro u hu1273 rw [add_apply']1274 change T x + g₀ x ≤ u1275 rw [hT_apply hx]1276 have hub : u - g₀ x ∈ upperBounds1277 ((fun g : OrderBoundedHom X Y => g x - g₀ x) '' S) := by1278 rintro _ ⟨g, hg, rfl⟩1279 exact sub_le_sub_right (hu ⟨g, hg, rfl⟩) _1280 have h1 := (σ_isLUB hx).2 hub1281 exact le_sub_iff_add_le.mp h112821283/-- When the codomain is order complete, every non-empty bounded above set1284of order bounded operators admits a least upper bound. -/1285theorem exists_isLUB1286 {S : Set (OrderBoundedHom X Y)} (hne : S.Nonempty) (hbdd : BddAbove S) :1287 ∃ f : OrderBoundedHom X Y, IsLUB S f := by1288 classical1289 let S' : Set (OrderBoundedHom X Y) :=1290 {f | ∃ F : Finset (OrderBoundedHom X Y), ∃ hF : F.Nonempty,1291 ↑F ⊆ S ∧ f = F.sup' hF id}1292 have hS'_ne : S'.Nonempty := by1293 obtain ⟨g, hg⟩ := hne1294 refine ⟨g, {g}, Finset.singleton_nonempty g, ?_, ?_⟩1295 · simpa using hg1296 · simp1297 have hS'_bdd : BddAbove S' := by1298 obtain ⟨h, hh⟩ := hbdd1299 refine ⟨h, ?_⟩1300 rintro _ ⟨F, hF, hFS, rfl⟩1301 exact Finset.sup'_le hF id (fun g hgF => hh (hFS hgF))1302 have hS'_dir : DirectedOn (· ≤ ·) S' := by1303 rintro _ ⟨F₁, hF₁, hF₁S, rfl⟩ _ ⟨F₂, hF₂, hF₂S, rfl⟩1304 have hU : (F₁ ∪ F₂).Nonempty := hF₁.mono Finset.subset_union_left1305 refine ⟨(F₁ ∪ F₂).sup' hU id, ⟨F₁ ∪ F₂, hU, ?_, rfl⟩, ?_, ?_⟩1306 · intro g hg1307 rcases Finset.mem_union.mp hg with h | h1308 · exact hF₁S h1309 · exact hF₂S h1310 · exact Finset.sup'_le hF₁ id (fun g hg =>1311 Finset.le_sup' id (Finset.mem_union_left _ hg))1312 · exact Finset.sup'_le hF₂ id (fun g hg =>1313 Finset.le_sup' id (Finset.mem_union_right _ hg))1314 obtain ⟨f, hLUB, _⟩ := isLUB_of_directedOn hS'_ne hS'_dir hS'_bdd1315 refine ⟨f, ?_, ?_⟩1316 · intro g hg1317 exact hLUB.1 ⟨{g}, Finset.singleton_nonempty g,1318 by simpa using hg, by simp⟩1319 · intro k hk1320 apply hLUB.21321 rintro _ ⟨F, hF, hFS, rfl⟩1322 exact Finset.sup'_le hF id (fun g hgF => hk (hFS hgF))13231324/-- The Riesz-Kantorovich conditional completeness structure on order bounded1325operators. This packages `OrderBoundedHom.exists_isLUB`; files can opt into it1326locally as a typeclass instance. -/1327@[reducible]1328noncomputable def conditionallyCompleteLattice :1329 ConditionallyCompleteLattice (OrderBoundedHom X Y) := by1330 classical1331 letI : SupSet (OrderBoundedHom X Y) :=1332 ⟨fun S => if h : S.Nonempty ∧ BddAbove S then (exists_isLUB h.1 h.2).choose else 0⟩1333 have hsSup : ∀ (S : Set (OrderBoundedHom X Y)), BddAbove S → S.Nonempty →1334 IsLUB S (sSup S) := by1335 intro S hbdd hne1336 change IsLUB S1337 (if h : S.Nonempty ∧ BddAbove S then (exists_isLUB h.1 h.2).choose else 0)1338 rw [dif_pos ⟨hne, hbdd⟩]1339 exact (exists_isLUB hne hbdd).choose_spec1340 exact conditionallyCompleteLatticeOfLatticeOfsSup _ hsSup13411342end OrderBoundedHom13431344/-- When the codomain is order complete, every order bounded operator1345is regular. -/1346theorem IsOrderBounded.isRegularOp1347 {X Y : Type*} [AddCommGroup X] [AddCommGroup Y]1348 [Lattice X] [ConditionallyCompleteLattice Y]1349 [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]1350 [VectorLattice X] [VectorLattice Y]1351 {f : X →ₗ[ℝ] Y} (hf : IsOrderBounded f) :1352 IsRegularOp f := by1353 let F : OrderBoundedHom X Y := ⟨f, hf⟩1354 refine ⟨F⁺.toLinearMap, F⁻.toLinearMap, ?_, ?_, ?_⟩1355 · intro x hx1356 change (0 : Y) ≤ F⁺ x1357 have h := OrderBoundedHom.le_iff.mp (posPart_nonneg F) x hx1358 change (0 : Y) ≤ F⁺ x at h1359 exact h1360 · intro x hx1361 change (0 : Y) ≤ F⁻ x1362 have h := OrderBoundedHom.le_iff.mp (negPart_nonneg F) x hx1363 change (0 : Y) ≤ F⁻ x at h1364 exact h1365 · exact (congrArg OrderBoundedHom.toLinearMap (posPart_sub_negPart F)).symm1366