PL1/LatticeDefinitions.lean

All source files · Download exact source

SHA-256: 3007a7906e5e8ca773ba81863ba82e796aab0e96b9c3a87b1682aebc11376604

1import Mathlib.Analysis.Normed.Module.Seminorm.Basic2import Mathlib.Analysis.Normed.Module.Basic3import Mathlib.Algebra.Order.Module.Defs4import Mathlib.Algebra.Order.Group.Lattice56/-!7# Equivalent real lattice norms89This predicate allows BOTH an arbitrary lattice order AND an equivalent norm.10It keeps the original vector-space addition and real scalar multiplication.11It does not merely ask whether the current norm is a lattice norm.1213On a complete space the positive lower bound makes the seminorm a genuine14complete norm. The intended meaning is therefore existence of an equivalent15Banach-lattice norm. LatticeBridge.lean verifies the implication from a bounded16linear isomorphism to an arbitrary BanLat Banach lattice (in any universe).17-/1819noncomputable section20universe u2122namespace PL12324/-- An arbitrary compatible real lattice order and solid norm equivalent to the25original norm. Positivity of a,b is explicit, including for the zero space. -/26def HasEquivalentRealLatticeNorm (E : Type u) [NormedAddCommGroup E]27    [NormedSpace ℝ E] : Prop :=28  ∃ latticeOrder : Lattice E,29    letI := latticeOrder30    IsOrderedAddMonoid E ∧ PosSMulMono ℝ E ∧31      ∃ p : Seminorm ℝ E,32        (∀ x y : E, |x| ≤ |y| → p x ≤ p y) ∧33        ∃ a b : ℝ, 0 < a ∧ 0 < b ∧34          ∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖3536end PL137