BanLat/Substructures/Band/DisjointComplement.lean

All source files · Download exact source

SHA-256: fb0087e729830d65c7f668a28cb9273abf7d39d52b39c07122096843c46ae1c9

1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Disjoint6import BanLat.Substructures.Band.Basic78/-!9# Disjoint complements1011The **disjoint complement** `Aᵈ` of a set `A ⊆ X` consists of all elements of12`X` disjoint from every member of `A`. It is always a band, and behaves13naturally with respect to inclusion, union, and double complementation.1415In an Archimedean vector lattice, the double disjoint complement `Aᵈᵈ`16coincides with the band generated by `A`, providing a characterisation of17bands as those subsets which equal their double disjoint complement. As a18consequence, every band of a normed vector lattice is norm closed, since the19disjoint complement of any set is itself the intersection of the zero-sets20of the continuous maps `x ↦ |x| ⊓ |a|`.21-/2223variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]24  [VectorLattice X]2526/-! ### The disjoint complement as a set -/2728/-- The **disjoint complement** of a set `A ⊆ X` is the set of all elements29disjoint from every member of `A`. -/30def disjointComplement (A : Set X) : Set X :=31  {x : X | ∀ a ∈ A, IsVLDisjoint x a}3233@[inherit_doc]34postfix:max "ᵈ" => disjointComplement3536omit [IsOrderedAddMonoid X] [VectorLattice X] in37/-- Membership in the disjoint complement: `x ∈ Aᵈ` iff `x` is disjoint from38every member of `A`. -/39theorem mem_disjointComplement_iff {A : Set X} {x : X} :40    x ∈ Aᵈ ↔ ∀ a ∈ A, IsVLDisjoint x a := Iff.rfl4142omit [IsOrderedAddMonoid X] [VectorLattice X] in43/-- Disjoint complementation is anti-monotone: `A ⊆ B` implies `Bᵈ ⊆ Aᵈ`. -/44theorem disjointComplement_anti {A B : Set X} (h : A ⊆ B) :45    Bᵈ ⊆ Aᵈ := fun _ hx a ha => hx a (h ha)4647omit [VectorLattice X] in48/-- The intersection of a set with its disjoint complement is contained in49`{0}`. -/50theorem disjointComplement_inter_eq_zero (A : Set X) :51    A ∩ Aᵈ ⊆ {0} := by52  rintro a ⟨ha, had⟩53  have hd : |a| ⊓ |a| = 0 := had a ha54  rw [inf_idem] at hd55  exact (abs_eq_zero_iff_zero a).mp hd5657omit [IsOrderedAddMonoid X] [VectorLattice X] in58/-- Every set is contained in its double disjoint complement. -/59theorem subset_disjointComplement_disjointComplement (A : Set X) :60    A ⊆ Aᵈᵈ := fun a ha _ hy => isVLDisjoint_comm.mp (hy a ha)6162omit [IsOrderedAddMonoid X] [VectorLattice X] in63/-- The triple disjoint complement equals the single disjoint complement. -/64theorem disjointComplement_disjointComplement_disjointComplement (A : Set X) :65    Aᵈᵈᵈ = Aᵈ :=66  Set.Subset.antisymm67    (disjointComplement_anti (subset_disjointComplement_disjointComplement A))68    (subset_disjointComplement_disjointComplement Aᵈ)6970omit [IsOrderedAddMonoid X] [VectorLattice X] in71/-- The disjoint complement of a union is the intersection of the disjoint72complements. -/73theorem disjointComplement_union (A B : Set X) :74    (A ∪ B)ᵈ = Aᵈ ∩ Bᵈ := by75  ext x76  refine ⟨fun hx => ⟨fun a ha => hx a (Or.inl ha), fun b hb => hx b (Or.inr hb)⟩,77    fun ⟨hA, hB⟩ _ hy => ?_⟩78  rcases hy with hy | hy79  · exact hA _ hy80  · exact hB _ hy8182omit [VectorLattice X] in83/-- The disjoint complement of a set together with its disjoint complement is84the singleton `{0}`. -/85theorem disjointComplement_union_disjointComplement_eq_singleton (A : Set X) :86    (A ∪ Aᵈ)ᵈ = ({0} : Set X) := by87  apply Set.Subset.antisymm88  · intro x hx89    have hxA : x ∈ Aᵈ := fun a ha => hx a (Or.inl ha)90    have hxAd : x ∈ Aᵈᵈ := fun a ha => hx a (Or.inr ha)91    exact disjointComplement_inter_eq_zero Aᵈ ⟨hxA, hxAd⟩92  · rintro x rfl a _93    exact isVLDisjoint_zero_left a9495namespace Band9697/-! ### The disjoint complement is a band -/9899/-- The disjoint complement of any set is a band. -/100def disjointComplement (A : Set X) : Band X :=101  Band.ofPosDirectedSSupMem102    (.ofSolid103      { carrier := Aᵈ104        add_mem' := fun {_ _} hx hy a ha => (hx a ha).add_left (hy a ha)105        zero_mem' := fun a _ => isVLDisjoint_zero_left a106        smul_mem' := fun c {_} hx a ha => (hx a ha).smul_left c }107      (fun _ _ hx hxy a ha => (hx a ha).mono_left hxy))108    (by109      intro S hSJ hpos _ hne y hy a ha110      have hy_nn : 0 ≤ y := by111        obtain ⟨s, hs⟩ := hne112        exact (hpos s hs).trans (hy.1 hs)113      have key : IsLUB ((fun z => |a| ⊓ z) '' S) (|a| ⊓ y) := isLUB_inf_const _ hy114      have hzero : ∀ s ∈ S, |a| ⊓ s = 0 := by115        intro s hs116        have h : |s| ⊓ |a| = 0 := hSJ hs a ha117        rw [abs_of_nonneg (hpos s hs), inf_comm] at h118        exact h119      have h_le : |a| ⊓ y ≤ 0 :=120        key.2 (by rintro _ ⟨s, hs, rfl⟩; exact (hzero s hs).le)121      have h_ge : 0 ≤ |a| ⊓ y := le_inf (abs_nonneg _) hy_nn122      have hay : |a| ⊓ y = 0 := le_antisymm h_le h_ge123      change |y| ⊓ |a| = 0124      rw [abs_of_nonneg hy_nn, inf_comm]; exact hay)125126end Band127128/-! ### Closedness in normed vector lattices -/129130section Normed131132variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]133  [NormedVectorLattice X]134135/-- In a normed vector lattice, the disjoint complement of any set is norm136closed: it is the intersection of the zero-sets of the continuous maps137`x ↦ |x| ⊓ |a|`. -/138theorem isClosed_disjointComplement (A : Set X) : IsClosed (Aᵈ) := by139  have heq : (Aᵈ : Set X) = ⋂ a ∈ A, (fun x : X => |x| ⊓ |a|) ⁻¹' {0} := by140    ext x141    simp [disjointComplement, IsVLDisjoint]142  rw [heq]143  refine isClosed_iInter (fun a => isClosed_iInter (fun _ => ?_))144  exact isClosed_singleton.preimage145    (NormedVectorLattice.lipschitzWith_abs.continuous.inf continuous_const)146147end Normed148