PL1/LatticeDisjointCountability.lean

All source files · Download exact source

SHA-256: 4d7e8e6228e2b9944edb614f64524b512b9bbaa7ed8ca8896a2d236f6b48e4e8

1import PL1.SchurLattice2import Mathlib.Topology.DiscreteSubset34/-!5# Countability of disjoint families in separable normed lattices67This is a structural preparation lemma. Atomicity of a Schur Banach lattice8is not assumed or concluded in this file.9-/1011noncomputable section12open scoped Topology1314namespace PL1.SchurLattice1516variable {E : Type*} [NormedAddCommGroup E] [Lattice E]17  [IsOrderedAddMonoid E] [NormedVectorLattice E]1819/-- Disjoint vectors are separated by at least the norm of either vector. -/20theorem norm_le_dist_of_isVLDisjoint {x y : E} (h : IsVLDisjoint x y) :21    ‖x‖ ≤ dist x y := by22  rw [dist_eq_norm]23  apply norm_le_norm_of_abs_le_abs24  have hneg : IsVLDisjoint x (-y) := by simpa only [IsVLDisjoint, abs_neg] using h25  rw [sub_eq_add_neg, abs_add_of_isVLDisjoint hneg, abs_neg]26  exact le_add_of_nonneg_right (abs_nonneg y)2728/-- A family of pairwise disjoint nonzero vectors is discrete in its inherited29norm topology, without a normalization hypothesis. -/30theorem isDiscrete_of_pairwise_isVLDisjoint (s : Set E)31    (hdisj : s.Pairwise IsVLDisjoint) (hzero : 0 ∉ s) : IsDiscrete s := by32  apply isDiscrete_iff_forall_mem_exists_isOpen.mpr33  intro x hx34  have hx0 : x ≠ 0 := fun h => hzero (h ▸ hx)35  refine ⟨Metric.ball x ‖x‖, Metric.isOpen_ball, ?_⟩36  ext y37  constructor38  · intro hy39    have hyx : y = x := by40      by_contra hne41      have hd := norm_le_dist_of_isVLDisjoint (hdisj hx hy.2 (fun h => hne h.symm))42      have hball := hy.143      rw [Metric.mem_ball, dist_comm] at hball44      exact (not_lt_of_ge hd) hball45    exact Set.mem_singleton_iff.mpr hyx46  · rintro rfl47    exact ⟨by simpa only [Metric.mem_ball, dist_self] using norm_pos_iff.mpr hx0, hx⟩4849/-- In a separable normed lattice every pairwise disjoint family of nonzero50vectors is countable. Positivity and normalization are unnecessary. -/51theorem countable_of_pairwise_isVLDisjoint [TopologicalSpace.SeparableSpace E]52    (s : Set E) (hdisj : s.Pairwise IsVLDisjoint) (hzero : 0 ∉ s) : s.Countable := by53  let : DiscreteTopology s :=54    isDiscrete_iff_discreteTopology.mp (isDiscrete_of_pairwise_isVLDisjoint s hdisj hzero)55  let : Countable s := TopologicalSpace.separableSpace_iff_countable.mp inferInstance56  exact Set.to_countable s5758/-- The requested normalized-family specialization. -/59theorem countable_of_pairwise_isVLDisjoint_norm_one [TopologicalSpace.SeparableSpace E]60    (s : Set E) (hdisj : s.Pairwise IsVLDisjoint) (hnorm : ∀ x ∈ s, ‖x‖ = 1) :61    s.Countable := by62  apply countable_of_pairwise_isVLDisjoint s hdisj63  intro hzero64  simpa using hnorm 0 hzero6566/-- The index type of a nonvanishing disjoint family is countable as well. -/67theorem countable_index_of_pairwise_isVLDisjoint [TopologicalSpace.SeparableSpace E]68    {ι : Type*} (x : ι → E) (hdisj : Pairwise (fun i j => IsVLDisjoint (x i) (x j)))69    (hne : ∀ i, x i ≠ 0) : Countable ι := by70  have hinj : Function.Injective x := by71    intro i j hij72    by_contra hneij73    have hd : IsVLDisjoint (x i) (x j) := hdisj hneij74    rw [hij, IsVLDisjoint, inf_idem] at hd75    exact hne j ((abs_eq_zero_iff_zero _).mp hd)76  have hs : (Set.range x).Countable := countable_of_pairwise_isVLDisjoint _ (by77    rintro _ ⟨i, rfl⟩ _ ⟨j, rfl⟩ hij78    exact hdisj (fun h => hij (congrArg x h))) (by79    rintro ⟨i, hi⟩80    exact hne i hi)81  let : Countable (Set.range x) := hs.to_subtype82  exact (show Function.Injective (fun i => (⟨x i, Set.mem_range_self i⟩ : Set.range x)) from83    fun _ _ h => hinj (congrArg Subtype.val h)).countable8485/-- The zero vector contributes at most one point to a set, so it can be86allowed in the set version of the countability theorem. -/87theorem countable_disjointSet [TopologicalSpace.SeparableSpace E]88    (s : Set E) (hdisj : s.Pairwise IsVLDisjoint) : s.Countable := by89  have hs : (s \ {0}).Countable := countable_of_pairwise_isVLDisjoint _90    (fun _ hx _ hy hne => hdisj hx.1 hy.1 hne) (by simp)91  apply (hs.union (Set.countable_singleton 0)).mono92  intro x hx93  by_cases h : x = 094  · exact Or.inr (Set.mem_singleton_iff.mpr h)95  · exact Or.inl ⟨hx, by simpa using h⟩9697/-- Separability makes the existing BanLat maximal positive disjoint family98countable. This theorem does not assert that its vectors are atoms. -/99theorem exists_countable_maximal_disjoint_positive_family100    [TopologicalSpace.SeparableSpace E] :101    ∃ s : Set E, s.Countable ∧ IsMaximalDisjoint s ∧ ∀ x ∈ s, 0 < x := by102  obtain ⟨s, hs, hpos⟩ := exists_isMaximalDisjoint_pos E103  exact ⟨s, countable_of_pairwise_isVLDisjoint s hs.prop.2 hs.prop.1, hs, hpos⟩104105end PL1.SchurLattice106