PL1/LatticeAtoms.lean
All source files · Download exact source
SHA-256: 7e5c5f2affd07335cf5cbfc8b5d8f63f388b20f101df237705578ba25e9519e9
1import PL1.LatticeDisjointCountability23/-!4# Positive vector-lattice atoms56These are vector-lattice atoms, not atoms of the underlying partial order.7Atomicity remains an explicit mathematical hypothesis in this development.8-/910noncomputable section11open scoped Topology1213namespace PL11415variable {E : Type*} [NormedAddCommGroup E] [Lattice E]16 [IsOrderedAddMonoid E] [NormedVectorLattice E]1718/-- A positive atom has a one-dimensional positive order interval. -/19def IsLatticeAtom (a : E) : Prop :=20 0 < a ∧ ∀ x : E, 0 ≤ x → x ≤ a → ∃ t : ℝ, 0 ≤ t ∧ x = t • a2122/-- Every nonzero positive vector dominates a positive vector-lattice atom. -/23def IsAtomicLattice (E : Type*) [NormedAddCommGroup E] [Lattice E]24 [IsOrderedAddMonoid E] [NormedVectorLattice E] : Prop :=25 ∀ u : E, 0 < u → ∃ a : E, IsLatticeAtom a ∧ a ≤ u2627namespace IsLatticeAtom2829theorem pos {a : E} (ha : IsLatticeAtom a) : 0 < a := ha.13031theorem nonneg {a : E} (ha : IsLatticeAtom a) : 0 ≤ a := ha.pos.le3233theorem ne_zero {a : E} (ha : IsLatticeAtom a) : a ≠ 0 := ha.pos.ne'3435/-- Positive scalar multiples preserve the actual atom property. -/36theorem smul_pos {a : E} (ha : IsLatticeAtom a) {c : ℝ} (hc : 0 < c) :37 IsLatticeAtom (c • a) := by38 refine ⟨lt_of_le_of_ne (smul_nonneg hc.le ha.nonneg)39 (smul_ne_zero hc.ne' ha.ne_zero).symm, ?_⟩40 intro x hx hxa41 have hdiv : c⁻¹ • x ≤ a := by42 simpa only [inv_smul_smul₀ hc.ne'] using43 smul_le_smul_of_nonneg_left hxa (inv_nonneg.mpr hc.le)44 obtain ⟨t, ht, heq⟩ := ha.2 _ (smul_nonneg (inv_nonneg.mpr hc.le) hx) hdiv45 refine ⟨t, ht, ?_⟩46 have heq' := congrArg (fun z : E => c • z) heq47 simpa only [smul_inv_smul₀ hc.ne', smul_smul, mul_comm c t] using heq'4849/-- The atom property applies to every bounded positive multiple interval. -/50theorem eq_smul_of_nonneg_le_smul {a x : E} (ha : IsLatticeAtom a)51 (hx : 0 ≤ x) {c : ℝ} (hc : 0 ≤ c) (hxc : x ≤ c • a) :52 ∃ t : ℝ, 0 ≤ t ∧ x = t • a := by53 rcases hc.eq_or_lt with rfl | hc54 · refine ⟨0, le_rfl, ?_⟩55 simp only [zero_smul] at hxc ⊢56 exact le_antisymm hxc hx57 · obtain ⟨t, ht, heq⟩ := (ha.smul_pos hc).2 x hx hxc58 exact ⟨t * c, mul_nonneg ht hc.le, by simpa only [smul_smul] using heq⟩5960theorem normalize {a : E} (ha : IsLatticeAtom a) :61 IsLatticeAtom (‖a‖⁻¹ • a) :=62 ha.smul_pos (inv_pos.mpr (norm_pos_iff.mpr ha.ne_zero))6364theorem norm_normalize {a : E} (ha : IsLatticeAtom a) : ‖‖a‖⁻¹ • a‖ = 1 := by65 rw [norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr (norm_nonneg _))]66 exact inv_mul_cancel₀ (norm_ne_zero_iff.mpr ha.ne_zero)6768/-- Atoms which overlap positively lie on the same positive ray. -/69theorem eq_pos_smul_of_not_isVLDisjoint {a b : E}70 (ha : IsLatticeAtom a) (hb : IsLatticeAtom b) (hd : ¬ IsVLDisjoint a b) :71 ∃ c : ℝ, 0 < c ∧ a = c • b := by72 have hinf : 0 ≤ a ⊓ b := le_inf ha.nonneg hb.nonneg73 have hne : a ⊓ b ≠ 0 := by74 simpa only [IsVLDisjoint, abs_of_nonneg ha.nonneg, abs_of_nonneg hb.nonneg] using hd75 obtain ⟨s, hs, hsa⟩ := ha.2 _ hinf inf_le_left76 obtain ⟨t, ht, htb⟩ := hb.2 _ hinf inf_le_right77 have hs0 : s ≠ 0 := by intro h; apply hne; simpa only [h, zero_smul] using hsa78 have ht0 : t ≠ 0 := by intro h; apply hne; simpa only [h, zero_smul] using htb79 refine ⟨s⁻¹ * t, mul_pos (inv_pos.mpr (lt_of_le_of_ne hs hs0.symm))80 (lt_of_le_of_ne ht ht0.symm), ?_⟩81 have heq := congrArg (fun z : E => s⁻¹ • z) (hsa.symm.trans htb)82 simpa only [inv_smul_smul₀ hs0, smul_smul] using heq8384/-- Distinct normalized atoms are lattice-disjoint. -/85theorem isVLDisjoint_of_norm_eq_one {a b : E}86 (ha : IsLatticeAtom a) (hb : IsLatticeAtom b)87 (hna : ‖a‖ = 1) (hnb : ‖b‖ = 1) (hne : a ≠ b) : IsVLDisjoint a b := by88 by_contra hd89 obtain ⟨c, hc, heq⟩ := ha.eq_pos_smul_of_not_isVLDisjoint hb hd90 have hnorm := congrArg norm heq91 rw [hna, norm_smul, hnb, Real.norm_of_nonneg hc.le, mul_one] at hnorm92 exact hne (by simpa only [← hnorm, one_smul] using heq)9394end IsLatticeAtom9596/-- The actual set of normalized positive atoms. -/97def normalizedLatticeAtoms (E : Type*) [NormedAddCommGroup E] [Lattice E]98 [IsOrderedAddMonoid E] [NormedVectorLattice E] : Set E :=99 {a | IsLatticeAtom a ∧ ‖a‖ = 1}100101theorem normalizedLatticeAtoms_pairwise :102 (normalizedLatticeAtoms E).Pairwise IsVLDisjoint := by103 intro a ha b hb hne104 exact ha.1.isVLDisjoint_of_norm_eq_one hb.1 ha.2 hb.2 hne105106theorem normalizedLatticeAtoms_countable [TopologicalSpace.SeparableSpace E] :107 (normalizedLatticeAtoms E).Countable :=108 SchurLattice.countable_of_pairwise_isVLDisjoint_norm_one _109 normalizedLatticeAtoms_pairwise (fun _ ha => ha.2)110111end PL1112