On complemented subspaces of L1[0,1]L_1[0,1]

BanLat/Substructures/Band/PPP.lean

All source files · Download exact source

SHA-256: d7d5fa1abe3602a7d56333de5818d4c2c1aa232047e95b4bc756e63b78328779

1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Substructures.Band.Projection6import BanLat.OrderComplete78/-!9# The (principal) projection property1011A vector lattice has the **Projection Property** (PP) when every band is a12projection band, and the **Principal Projection Property** (PPP) when every13principal band is a projection band. Clearly PP implies PPP.1415The two main sources of these properties come from order completeness: order16complete vector lattices have PP, and σ-order complete vector lattices have17PPP. Under PPP, two positive elements admit a positive disjoint refinement of18their sum with controlled summands. Finally, PP and PPP both imply the19Archimedean property.20-/2122/-! ### The projection properties -/2324section Defs2526variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]27  [VectorLattice X]2829/-- A vector lattice has the **Projection Property** (PP) when every band in30`X` is a projection band. -/31class HasProjectionProperty (X : Type*) [AddCommGroup X] [Lattice X]32    [IsOrderedAddMonoid X] [VectorLattice X] : Prop where33  exists_projectionBand : ∀ B : Band X, ∃ P : ProjectionBand X,34    (P : Set X) = (B : Set X)3536/-- A vector lattice has the **Principal Projection Property** (PPP) when every37principal band in `X` is a projection band. -/38class HasPrincipalProjectionProperty (X : Type*) [AddCommGroup X] [Lattice X]39    [IsOrderedAddMonoid X] [VectorLattice X] : Prop where40  exists_projectionBand : ∀ a : X, ∃ P : ProjectionBand X,41    (P : Set X) = (Band.generated ({a} : Set X) : Set X)4243/-- PP implies PPP. -/44instance (priority := 100) HasPrincipalProjectionProperty.of_hasProjectionProperty45    [HasProjectionProperty X] : HasPrincipalProjectionProperty X where46  exists_projectionBand a :=47    HasProjectionProperty.exists_projectionBand (Band.generated ({a} : Set X))4849end Defs5051/-! ### Order completeness implies the projection properties -/5253section OrderComplete5455/-- An order complete vector lattice has the Projection Property. -/56instance (priority := 100) HasProjectionProperty.of_isOrderComplete57    {X : Type*} [AddCommGroup X] [ConditionallyCompleteLattice X]58    [IsOrderedAddMonoid X] [VectorLattice X] :59    HasProjectionProperty X := by60  haveI : IsVLArchimedean X := IsVLArchimedean_of_sigmaConditionallyCompleteLattice61  refine ⟨fun B => ?_⟩62  apply (ProjectionBand.projectionBand_iff_isLUB_inter_Icc B).mpr63  intro x hx64  refine ⟨sSup ((B : Set X) ∩ Set.Icc 0 x),65    isLUB_csSup ⟨0, B.toOrderIdeal.toSubmodule.zero_mem, le_refl 0, hx⟩66      ⟨x, fun _ hy => hy.2.2⟩⟩6768/-- A σ-order complete vector lattice has the Principal Projection Property. -/69instance (priority := 100)70    HasPrincipalProjectionProperty.of_isSigmaOrderComplete71    {X : Type*} [AddCommGroup X] [SigmaConditionallyCompleteLattice X]72    [IsOrderedAddMonoid X] [VectorLattice X] :73    HasPrincipalProjectionProperty X := by74  haveI : IsVLArchimedean X := IsVLArchimedean_of_sigmaConditionallyCompleteLattice75  refine ⟨fun a => ?_⟩76  have hband_eq : (Band.generated ({a} : Set X) : Set X)77      = (Band.generated ({|a|} : Set X) : Set X) := by78    apply le_antisymm <;> apply Band.generated_le <;> rintro y rfl79    · refine (Band.generated _).mem_of_abs_le_abs80        (Band.subset_generated _ rfl) ?_81      rw [abs_abs]82    · exact (Band.generated _).abs_mem (Band.subset_generated _ rfl)83  have habs_nn : (0 : X) ≤ |a| := abs_nonneg a84  have hLUB : ∀ x : X, 0 ≤ x →85      ∃ s, IsLUB (Set.range fun n : ℕ => x ⊓ (n : ℕ) • |a|) s := by86    intro x hx87    have hcount : (Set.range fun n : ℕ => x ⊓ (n : ℕ) • |a|).Countable :=88      Set.countable_range _89    have hne : (Set.range fun n : ℕ => x ⊓ (n : ℕ) • |a|).Nonempty :=90      Set.range_nonempty _91    have hbdd : BddAbove (Set.range fun n : ℕ => x ⊓ (n : ℕ) • |a|) :=92      ⟨x, by rintro _ ⟨n, rfl⟩; exact inf_le_left⟩93    refine ⟨sSup _,94      fun _ hy => SigmaConditionallyCompleteLattice.le_csSup _ _ hcount hbdd hy,95      fun _ hy => SigmaConditionallyCompleteLattice.csSup_le _ _ hcount hne hy⟩96  obtain ⟨P, hP⟩ :=97    (ProjectionBand.principalBand_projectionBand_iff_isLUB_range habs_nn).mpr hLUB98  exact ⟨P, hP.trans hband_eq.symm⟩99100end OrderComplete101102section Rest103104variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]105  [VectorLattice X]106107/-! ### Disjoint refinement of finite positive families108109Under PPP, any finite family of positive vectors may be replaced by a110pairwise disjoint family of positive vectors, dominated termwise by the111original family, whose sum equals the supremum of the original family. -/112113/-- For two positive elements in a vector lattice with PPP, their sum can be114rewritten as a sum of two positive disjoint elements, with the new summands115dominated by `2 • x` and `2 • y` respectively. -/116theorem exists_disjoint_add_eq_add_of_hasPrincipalProjectionProperty117    [HasPrincipalProjectionProperty X] {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y) :118    ∃ u v : X, IsVLDisjoint u v ∧ 0 ≤ u ∧ 0 ≤ v ∧119      u ≤ (2 : ℕ) • x ∧ v ≤ (2 : ℕ) • y ∧ u + v = x + y := by120  obtain ⟨P, hP⟩ := HasPrincipalProjectionProperty.exists_projectionBand ((x - y)⁺)121  set a := x + y122  set u := P.bandProjection a123  set v := a - u124  have ha : 0 ≤ a := by simp [a, add_nonneg hx hy]125  have hu_mem : u ∈ (P : Set X) := by126    exact P.bandProjection_mem a127  have hv_mem : v ∈ disjointComplement (P : Set X) := by128    simpa [u, v] using P.id_sub_bandProjection_mem a129  have huv : IsVLDisjoint u v :=130    isVLDisjoint_comm.mp (hv_mem _ hu_mem)131  have hu0 : 0 ≤ u := by132    simpa [u] using Positive.zero_le_iff.mp P.bandProjection_nonneg a ha133  have hv0 : 0 ≤ v := by134    have hu_le_a : u ≤ a := by135      simpa [u] using Positive.le_iff.mp P.bandProjection_le_id a ha136    simpa [v] using sub_nonneg.mpr hu_le_a137  have hmono : Monotone P.bandProjection :=138    Positive.monotone_iff.mpr (Positive.zero_le_iff.mp P.bandProjection_nonneg)139  have hgen_sub :140      (Band.generated ({(x - y)⁺} : Set X) : Set X) ⊆141        disjointComplement ({(x - y)⁻} : Set X) := by142    refine Band.generated_le (B := Band.disjointComplement ({(x - y)⁻} : Set X)) ?_143    intro z hz144    rw [Set.mem_singleton_iff] at hz145    subst z146    change (x - y)⁺ ∈ disjointComplement ({(x - y)⁻} : Set X)147    rw [mem_disjointComplement_iff]148    intro w hw149    rw [Set.mem_singleton_iff] at hw150    subst w151    exact isVLDisjoint_posPart_negPart (x - y)152  have hneg_mem : (x - y)⁻ ∈ disjointComplement (P : Set X) := by153    intro z hz154    have hz_gen : z ∈ (Band.generated ({(x - y)⁺} : Set X) : Set X) := by155      simpa [hP] using hz156    have hz_dc : z ∈ disjointComplement ({(x - y)⁻} : Set X) :=157      hgen_sub hz_gen158    exact isVLDisjoint_comm.mp (hz_dc _ (Set.mem_singleton _))159  have hPneg_zero : P.bandProjection ((x - y)⁻) = 0 :=160    P.bandProjection_eq_zero_of_mem_dc hneg_mem161  have ha_le_x : a ≤ (2 : ℕ) • x + (x - y)⁻ := by162    have hyx_le : y - x ≤ (x - y)⁻ := by163      rw [show y - x = -(x - y) by abel, negPart_def]164      exact le_sup_left165    calc166      a = (2 : ℕ) • x + (y - x) := by167        simp [a]168        abel169      _ ≤ (2 : ℕ) • x + (x - y)⁻ := by gcongr170  have hu_le : u ≤ (2 : ℕ) • x := by171    calc172      u ≤ P.bandProjection ((2 : ℕ) • x + (x - y)⁻) := by173        simpa [u] using hmono ha_le_x174      _ = P.bandProjection ((2 : ℕ) • x) + P.bandProjection ((x - y)⁻) := by175        rw [map_add]176      _ = P.bandProjection ((2 : ℕ) • x) := by rw [hPneg_zero, add_zero]177      _ ≤ (2 : ℕ) • x := by178        exact Positive.le_iff.mp P.bandProjection_le_id _ (nsmul_nonneg hx 2)179  have hpos_mem : (x - y)⁺ ∈ (P : Set X) := by180    rw [hP]181    exact Band.subset_generated _ rfl182  have hpos_mem_comp :183      (x - y)⁺ ∈ disjointComplement ((Pᶜ : ProjectionBand X) : Set X) := by184    intro z hz185    exact isVLDisjoint_comm.mp (hz _ hpos_mem)186  have hPcpos_zero : (Pᶜ : ProjectionBand X).bandProjection ((x - y)⁺) = 0 :=187    (Pᶜ : ProjectionBand X).bandProjection_eq_zero_of_mem_dc hpos_mem_comp188  have hmono_comp : Monotone (Pᶜ : ProjectionBand X).bandProjection :=189    Positive.monotone_iff.mpr190      (Positive.zero_le_iff.mp (Pᶜ : ProjectionBand X).bandProjection_nonneg)191  have ha_le_y : a ≤ (2 : ℕ) • y + (x - y)⁺ := by192    have hxy_le : x - y ≤ (x - y)⁺ := by193      rw [posPart_def]194      exact le_sup_left195    calc196      a = (2 : ℕ) • y + (x - y) := by197        simp [a]198        abel199      _ ≤ (2 : ℕ) • y + (x - y)⁺ := by gcongr200  have hv_eq : (Pᶜ : ProjectionBand X).bandProjection a = v := by201    rw [ProjectionBand.bandProjection_compl]202    simp [u, v]203  have hv_le : v ≤ (2 : ℕ) • y := by204    calc205      v = (Pᶜ : ProjectionBand X).bandProjection a := hv_eq.symm206      _ ≤ (Pᶜ : ProjectionBand X).bandProjection ((2 : ℕ) • y + (x - y)⁺) :=207        hmono_comp ha_le_y208      _ = (Pᶜ : ProjectionBand X).bandProjection ((2 : ℕ) • y) +209          (Pᶜ : ProjectionBand X).bandProjection ((x - y)⁺) := by210            rw [map_add]211      _ = (Pᶜ : ProjectionBand X).bandProjection ((2 : ℕ) • y) := by212        rw [hPcpos_zero, add_zero]213      _ ≤ (2 : ℕ) • y := by214        exact Positive.le_iff.mp (Pᶜ : ProjectionBand X).bandProjection_le_id _215          (nsmul_nonneg hy 2)216  refine ⟨u, v, huv, hu0, hv0, hu_le, hv_le, ?_⟩217  calc218    u + v = a := by219      simp [v]220    _ = x + y := by simp [a]221222/-! ### The Archimedean property -/223224private def IsPosSupFromIdeal (J : OrderIdeal X) (x : X) : Prop :=225  ∃ S : Set X, S.Nonempty ∧ S ⊆ (J : Set X) ∧ (∀ s ∈ S, 0 ≤ s) ∧ IsLUB S x226227private lemma IsPosSupFromIdeal.zero (J : OrderIdeal X) :228    IsPosSupFromIdeal J (0 : X) :=229  ⟨{0}, Set.singleton_nonempty 0, by rintro _ rfl; exact J.toSubmodule.zero_mem,230    by rintro _ rfl; rfl,231    isLUB_singleton⟩232233private lemma IsPosSupFromIdeal.of_mem {J : OrderIdeal X} {x : X}234    (hx0 : 0 ≤ x) (hxJ : x ∈ J) : IsPosSupFromIdeal J x :=235  ⟨{x}, Set.singleton_nonempty x, by rintro _ rfl; exact hxJ, by rintro _ rfl; exact hx0,236    isLUB_singleton⟩237238private lemma IsPosSupFromIdeal.mono {J : OrderIdeal X} {x y : X}239    (hx : IsPosSupFromIdeal J x) (hy0 : 0 ≤ y) (hyx : y ≤ x) :240    IsPosSupFromIdeal J y := by241  obtain ⟨S, hSne, hSJ, hS0, hSx⟩ := hx242  refine ⟨(fun s => y ⊓ s) '' S, hSne.image _, ?_, ?_, ?_⟩243  · rintro _ ⟨s, hs, rfl⟩244    exact J.solid (hSJ hs) (le_inf hy0 (hS0 s hs)) inf_le_right245  · rintro _ ⟨s, hs, rfl⟩246    exact le_inf hy0 (hS0 s hs)247  · simpa [inf_eq_left.mpr hyx] using isLUB_inf_const y hSx248249private lemma IsPosSupFromIdeal.add {J : OrderIdeal X} {x y : X}250    (hx : IsPosSupFromIdeal J x) (hy : IsPosSupFromIdeal J y) :251    IsPosSupFromIdeal J (x + y) := by252  obtain ⟨S, hSne, hSJ, hS0, hSx⟩ := hx253  obtain ⟨T, hTne, hTJ, hT0, hTy⟩ := hy254  have hLUB : IsLUB ((fun p : X × X => p.1 + p.2) '' (S ×ˢ T)) (x + y) := by255    refine ⟨?_, ?_⟩256    · rintro _ ⟨⟨s, t⟩, ⟨hs, ht⟩, rfl⟩257      exact add_le_add (hSx.1 hs) (hTy.1 ht)258    · intro u hu259      have hy_le_sub : ∀ s ∈ S, y ≤ u - s := by260        intro s hs261        apply hTy.2262        intro t ht263        exact le_sub_iff_add_le.mpr (by264          rw [add_comm]265          exact hu ⟨(s, t), ⟨hs, ht⟩, rfl⟩)266      exact le_sub_iff_add_le.mp <| hSx.2 fun s hs =>267        le_sub_iff_add_le.mpr <| by268          rw [add_comm]269          exact le_sub_iff_add_le.mp (hy_le_sub s hs)270  refine ⟨(fun p : X × X => p.1 + p.2) '' (S ×ˢ T), hSne.prod hTne |>.image _, ?_, ?_,271    hLUB⟩272  · rintro _ ⟨⟨s, t⟩, ⟨hs, ht⟩, rfl⟩273    exact J.toSubmodule.add_mem (hSJ hs) (hTJ ht)274  · rintro _ ⟨⟨s, t⟩, ⟨hs, ht⟩, rfl⟩275    exact add_nonneg (hS0 s hs) (hT0 t ht)276277private lemma IsPosSupFromIdeal.smul_nonneg {J : OrderIdeal X} {x : X} {c : ℝ}278    (hc : 0 ≤ c) (hx : IsPosSupFromIdeal J x) :279    IsPosSupFromIdeal J (c • x) := by280  obtain ⟨S, hSne, hSJ, hS0, hSx⟩ := hx281  refine ⟨(fun s => c • s) '' S, hSne.image _, ?_, ?_, isLUB_smul_of_nonneg hc hSx⟩282  · rintro _ ⟨s, hs, rfl⟩283    exact J.toSubmodule.smul_mem c (hSJ hs)284  · rintro _ ⟨s, hs, rfl⟩285    exact _root_.smul_nonneg hc (hS0 s hs)286287private lemma IsPosSupFromIdeal.sSup {J : OrderIdeal X} {S : Set X} {x : X}288    (hSne : S.Nonempty) (hS : ∀ s ∈ S, IsPosSupFromIdeal J s) (hSx : IsLUB S x) :289    IsPosSupFromIdeal J x := by290  classical291  refine ⟨{a | ∃ s, ∃ hs : s ∈ S, a ∈ (hS s hs).choose}, ?_, ?_, ?_, ?_⟩292  · obtain ⟨s, hs⟩ := hSne293    exact ⟨(hS s hs).choose_spec.1.choose, s, hs, (hS s hs).choose_spec.1.choose_spec⟩294  · rintro a ⟨s, hs, ha⟩295    exact (hS s hs).choose_spec.2.1 ha296  · rintro a ⟨s, hs, ha⟩297    exact (hS s hs).choose_spec.2.2.1 a ha298  · refine ⟨?_, ?_⟩299    · rintro a ⟨s, hs, ha⟩300      exact (((hS s hs).choose_spec.2.2.2).1 ha).trans (hSx.1 hs)301    · intro u hu302      apply hSx.2303      intro s hs304      exact ((hS s hs).choose_spec.2.2.2).2 (fun a ha => hu ⟨s, hs, ha⟩)305306private lemma isPosSupFromIdeal_of_mem_bandGenerated307    (J : OrderIdeal X) {x : X} (hx0 : 0 ≤ x)308    (hxG : x ∈ Band.generated (J : Set X)) :309    IsPosSupFromIdeal J x := by310  let M : Submodule ℝ X :=311    { carrier := {z : X | IsPosSupFromIdeal J |z|}312      add_mem' := fun {a b} ha hb =>313        IsPosSupFromIdeal.mono (IsPosSupFromIdeal.add ha hb) (abs_nonneg _)314          (abs_add_le a b)315      zero_mem' := by simpa using IsPosSupFromIdeal.zero J316      smul_mem' := fun c a ha => by317        change IsPosSupFromIdeal J |c • a|318        rw [abs_smul']319        exact IsPosSupFromIdeal.smul_nonneg (abs_nonneg c) ha }320  let K : OrderIdeal X := OrderIdeal.ofSolid M fun _ b ha hba =>321    IsPosSupFromIdeal.mono ha (abs_nonneg b) hba322  let B : Band X := Band.ofPosDirectedSSupMem K (by323    intro S hSK hS0 _ hSne y hSy324    change IsPosSupFromIdeal J |y|325    have hy0 : 0 ≤ y := by326      obtain ⟨s, hs⟩ := hSne327      exact (hS0 s hs).trans (hSy.1 hs)328    rw [abs_of_nonneg hy0]329    refine IsPosSupFromIdeal.sSup (J := J) hSne ?_ hSy330    intro s hs331    have hsK : s ∈ K := hSK hs332    change IsPosSupFromIdeal J |s| at hsK333    simpa [abs_of_nonneg (hS0 s hs)] using hsK)334  have hle : Band.generated (J : Set X) ≤ B := Band.generated_le (B := B) fun z hz => by335    change IsPosSupFromIdeal J |z|336    exact IsPosSupFromIdeal.of_mem (abs_nonneg z) (J.abs_mem hz)337  have hxB : x ∈ B := hle hxG338  change IsPosSupFromIdeal J |x| at hxB339  simpa [abs_of_nonneg hx0] using hxB340341/-- A vector lattice with the Principal Projection Property is Archimedean. -/342theorem isVLArchimedean_of_hasPrincipalProjectionProperty343    [HasPrincipalProjectionProperty X] : IsVLArchimedean X := by344  apply isVLArchimedean_of_eq_zero_of_nonneg_of_forall_nsmul_le345  intro x y hx hxy346  obtain ⟨P, hP⟩ := HasPrincipalProjectionProperty.exists_projectionBand x347  have hy0 : 0 ≤ y := by simpa using hxy 0348  have hxP : x ∈ (P : Set X) := by349    rw [hP]350    exact Band.subset_generated _ rfl351  have hPx : P.bandProjection x = x :=352    P.bandProjection_eq_of_mem hxP353  have hmono : Monotone P.bandProjection :=354    Positive.monotone_iff.mpr (Positive.zero_le_iff.mp P.bandProjection_nonneg)355  have hbound : ∀ n : ℕ, n • x ≤ P.bandProjection y := by356    intro n357    calc358      n • x = P.bandProjection (n • x) := by359        rw [map_nsmul, hPx]360      _ ≤ P.bandProjection y := hmono (hxy n)361  have hPy0 : 0 ≤ P.bandProjection y :=362    Positive.zero_le_iff.mp P.bandProjection_nonneg y hy0363  let J : OrderIdeal X := OrderIdeal.principal x364  have hPy_mem_generated_principal :365      P.bandProjection y ∈ Band.generated (J : Set X) := by366    have hsub : Band.generated ({x} : Set X) ≤ Band.generated (J : Set X) :=367      Band.generated_le (B := Band.generated (J : Set X)) (by368        intro z hz369        rw [Set.mem_singleton_iff] at hz370        subst z371        exact Band.subset_generated _ (show x ∈ (J : Set X) from372          OrderIdeal.self_mem_principal x))373    have hPy_gen_x : P.bandProjection y ∈ Band.generated ({x} : Set X) := by374      change P.bandProjection y ∈ ((Band.generated ({x} : Set X)) : Set X)375      rw [← hP]376      exact P.bandProjection_mem y377    exact hsub hPy_gen_x378  obtain ⟨S, _hSne, hSJ, _hS0, hLUB⟩ :=379    isPosSupFromIdeal_of_mem_bandGenerated J hPy0 hPy_mem_generated_principal380  have hupper : P.bandProjection y - x ∈ upperBounds S := by381    intro s hs382    have hsJ : s ∈ OrderIdeal.principal x := hSJ hs383    obtain ⟨c, hc, hs_abs_le⟩ := OrderIdeal.mem_principal.mp hsJ384    have hs_le_cx : s ≤ c • x := by385      calc386        s ≤ |s| := le_abs_self s387        _ ≤ c • |x| := hs_abs_le388        _ = c • x := by rw [abs_of_nonneg hx]389    obtain ⟨n, hn⟩ := exists_nat_gt (c + 1)390    refine le_sub_iff_add_le.mpr ?_391    calc392      s + x ≤ c • x + x := by simpa [add_comm] using add_le_add_right hs_le_cx x393      _ = (c + 1) • x := by rw [add_smul, one_smul]394      _ ≤ (n : ℝ) • x := smul_le_smul_of_nonneg_right (le_of_lt hn) hx395      _ = n • x := Nat.cast_smul_eq_nsmul ℝ n x396      _ ≤ P.bandProjection y := hbound n397  have hPy_le : P.bandProjection y ≤ P.bandProjection y - x := hLUB.2 hupper398  have hx_nonpos : x ≤ 0 := by399    have hle : P.bandProjection y + x ≤ P.bandProjection y := le_sub_iff_add_le.mp hPy_le400    have hle' : P.bandProjection y + x ≤ P.bandProjection y + 0 := by simpa using hle401    simpa using (add_le_add_iff_left (P.bandProjection y)).mp hle'402  exact le_antisymm hx_nonpos hx403404/-- A vector lattice with the Projection Property is Archimedean. -/405theorem isVLArchimedean_of_hasProjectionProperty406    [HasProjectionProperty X] : IsVLArchimedean X :=407  isVLArchimedean_of_hasPrincipalProjectionProperty408409end Rest410