BanLat/OrderUnit.lean

All source files · Download exact source

SHA-256: 93ed97cca155d8bf0a69bed4cffe229e0cb9183a809d8088855f1ccf399fdd30

1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Disjoint67/-!8# Order units910This file introduces the two standard notions of order unit in a vector11lattice. A **weak order unit** is a non-negative element disjoint only from12zero, while a **strong order unit** is a non-negative element which dominates13every other element up to a positive scalar multiple. Every strong order unit14is a weak order unit.15-/1617variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]18  [VectorLattice X]1920/-- An element `e` of a vector lattice is a **weak order unit** if it is21non-negative and the only element disjoint from `e` is `0`. -/22def WeakOrderUnit (e : X) : Prop :=23  0 ≤ e ∧ ∀ x : X, IsVLDisjoint x e → x = 02425/-- An element `e` of a vector lattice is a **strong order unit** if it is26non-negative and every element of `X` is dominated, in absolute value, by some27non-negative real multiple of `e`. -/28def StrongOrderUnit (e : X) : Prop :=29  0 ≤ e ∧ ∀ x : X, ∃ c : ℝ, 0 ≤ c ∧ |x| ≤ c • e3031/-- For a non-negative element `e`, disjointness from `e` implies disjointness32from every natural scalar multiple of `e`. -/33private lemma abs_inf_natCast_smul_eq_zero {x e : X} (he : 0 ≤ e)34    (hxe : |x| ⊓ e = 0) : ∀ k : ℕ, |x| ⊓ ((k : ℝ) • e) = 035  | 0 => by simp36  | k + 1 => by37      have ih := abs_inf_natCast_smul_eq_zero he hxe k38      have hke : 0 ≤ ((k : ℝ) • e) :=39        smul_nonneg (Nat.cast_nonneg k) he40      have hsucc : ((k + 1 : ℕ) : ℝ) • e = (k : ℝ) • e + e := by41        push_cast; rw [add_smul, one_smul]42      rw [hsucc]43      refine le_antisymm ?_44        (le_inf (abs_nonneg _) (add_nonneg hke he))45      calc |x| ⊓ ((k : ℝ) • e + e)46          ≤ |x| ⊓ ((k : ℝ) • e) + |x| ⊓ e :=47            inf_le_inf_add_inf_of_nonneg |x| ((k : ℝ) • e) e (abs_nonneg x) hke he48        _ = 0 := by rw [ih, hxe, add_zero]4950/-- Every strong order unit is a weak order unit. -/51theorem WeakOrderUnit.of_strongOrderUnit {e : X} (he : StrongOrderUnit e) :52    WeakOrderUnit e := by53  refine ⟨he.1, fun x hxe => ?_⟩54  rw [IsVLDisjoint, abs_of_nonneg he.1] at hxe55  obtain ⟨c, hc, hxc⟩ := he.2 x56  obtain ⟨n, hn⟩ := exists_nat_ge c57  have hxn : |x| ≤ (n : ℝ) • e :=58    hxc.trans (smul_le_smul_of_nonneg_right hn he.1)59  have hkey := abs_inf_natCast_smul_eq_zero he.1 hxe n60  have habs : |x| = 0 := by rw [← inf_eq_left.mpr hxn, hkey]61  exact (abs_eq_zero_iff_zero x).mp habs62