Documentation

VecLat.UnitalAMSpace.Basic

class IsUnitalAMSpace (X : Type u_1) (e : outParam X) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] :

pos : 0 ≤ e
unit (x : X) : ∃ (s : ℝ), 0 ≤ s ∧ |x| ≤ s • e

Instances

theorem UnitalAMSpace.unit_pos {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] :

0 ≤ e

theorem UnitalAMSpace.unit_def {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (x : X) :

∃ (s : ℝ), 0 ≤ s ∧ |x| ≤ s • e

def UnitalAMSpace.S {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e x : X) :

Equations

UnitalAMSpace.S e x = {s : ℝ | 0 ≤ s ∧ |x| ≤ s • e}

Instances For

theorem UnitalAMSpace.S_nonempty {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (x : X) :

(S e x).Nonempty

theorem UnitalAMSpace.S_bddbelow {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e x : X) :

BddBelow (S e x)

def UnitalAMSpace.norm {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) :

X → ℝ

Equations

UnitalAMSpace.norm e x = sInf (UnitalAMSpace.S e x)

Instances For

theorem UnitalAMSpace.norm_def {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e x : X) :

norm e x = sInf (S e x)

theorem UnitalAMSpace.norm_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e x : X) :

0 ≤ norm e x

theorem UnitalAMSpace.norm_unit {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (nonzero : e ≠ 0) :

norm e e = 1

theorem UnitalAMSpace.gt_norm {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (x : X) (t : ℝ) (h : norm e x < t) :

|x| ≤ t • e

theorem UnitalAMSpace.norm_smul {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] (x : X) (r : ℝ) :

norm e (r • x) = |r| • norm e x

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

|x| ≤ norm e x • e

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

norm e x = 0 ↔ x = 0

theorem UnitalAMSpace.norm_add {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] [Archimedean X] (x y : X) :

norm e (x + y) ≤ norm e x + norm e y

theorem UnitalAMSpace.abs_le_abs_norm {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] [Archimedean X] (x y : X) (hxy : |x| ≤ |y|) :

norm e x ≤ norm e y

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

norm e x = norm e |x|

theorem UnitalAMSpace.AMnorm {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] [Archimedean X] (x y : X) (xpos : 0 ≤ x) (ypos : 0 ≤ y) :

norm e (x ⊔ y) = max (norm e x) (norm e y)

instance UnitalAMSpace.instNormedAddCommGroup {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] [Archimedean X] :

NormedAddCommGroup X

Equations

One or more equations did not get rendered due to their size.

instance UnitalAMSpace.instNormedSpace {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] [Archimedean X] :

NormedSpace ℝ X

Equations

UnitalAMSpace.instNormedSpace e = { toModule := inst✝².toModule, norm_smul_le := ⋯ }

instance UnitalAMSpace.instTopologicalSpace {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) [IsUnitalAMSpace X e] [Archimedean X] :

TopologicalSpace X

Equations

UnitalAMSpace.instTopologicalSpace e = inferInstance