theorem UnitalAMSpace.Maximal.exist {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (x : X) (h : 1 < norm e x) : ∃ (φ : VecLatHom X ℝ), φ e = 1 ∧ φ |x| ≥ 1

def UnitalAMSpace.Maximal.Characters {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : Set (WeakDual ℝ X)

Equations

• UnitalAMSpace.Maximal.Characters e = {φ : WeakDual ℝ X | IsVecLatHom ⇑φ ∧ φ e = 1}

theorem UnitalAMSpace.Maximal.character_contractive {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (φ : VecLatHom X ℝ) (h : φ e = 1) (x : X) : |φ x| ≤ norm e x

def UnitalAMSpace.Maximal.toStrongDual {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (φ : VecLatHom X ℝ) (h : φ e = 1) : StrongDual ℝ X

Equations

• UnitalAMSpace.Maximal.toStrongDual e φ h = (↑φ).mkContinuousOfExistsBound ⋯

def UnitalAMSpace.Maximal.character_ofVecLatHom {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (φ : VecLatHom X ℝ) (h : φ e = 1) : ↑(Characters e)

Equations

• UnitalAMSpace.Maximal.character_ofVecLatHom e φ h = ⟨UnitalAMSpace.Maximal.toStrongDual e φ h, ⋯⟩

theorem UnitalAMSpace.Maximal.characters_nonempty {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (nonzero : e ≠ 0) : (Characters e).Nonempty

theorem UnitalAMSpace.Maximal.eval_characters_nonempty {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (nonzero : e ≠ 0) (x : X) : {x_1 : ℝ | ∃ φ ∈ Characters e, |φ x| = x_1}.Nonempty

theorem UnitalAMSpace.Maximal.eval_characters_bddabove {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (x : X) : BddAbove {x_1 : ℝ | ∃ φ ∈ Characters e, |φ x| = x_1}

theorem UnitalAMSpace.Maximal.attains_norm_at_characters {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (nonzero : e ≠ 0) (x : X) : norm e x = sSup {x_1 : ℝ | ∃ φ ∈ Characters e, |φ x| = x_1}

def UnitalAMSpace.Maximal.map_abs_set {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (x : X) : Set (WeakDual ℝ X)

Equations

• UnitalAMSpace.Maximal.map_abs_set e x = {φ : WeakDual ℝ X | φ |x| = |φ x|}

theorem UnitalAMSpace.Maximal.map_abs_set_closed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] (x : X) : IsClosed (map_abs_set e x)

theorem UnitalAMSpace.Maximal.inter_map_abs_set {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : ⨅ (x : X), map_abs_set e x = {φ : WeakDual ℝ X | IsVecLatHom ⇑φ}

theorem UnitalAMSpace.Maximal.isVecLatHom_closed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : IsClosed {φ : WeakDual ℝ X | IsVecLatHom ⇑φ}

theorem UnitalAMSpace.Maximal.closed {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : IsClosed (Characters e)

theorem UnitalAMSpace.Maximal.bounded {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : Bornology.IsBounded (⇑StrongDual.toWeakDual ⁻¹' Characters e)

theorem UnitalAMSpace.Maximal.compact {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : IsCompact (Characters e)

instance UnitalAMSpace.Maximal.instCompactSpace {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [Archimedean X] (e : X) [IsUnitalAMSpace X e] : CompactSpace ↑(Characters e)