Absolute values #
This file defines a bundled type of absolute values AbsoluteValue R S
.
Main definitions #
AbsoluteValue R S
is the type of absolute values onR
mapping toS
.AbsoluteValue.abs
is the "standard" absolute value onS
, mapping negativex
to-x
.AbsoluteValue.toMonoidWithZeroHom
: absolute values mapping to a linear ordered field preserve0
,*
and1
IsAbsoluteValue
: a type class stating thatf : β → α→ α
satisfies the axioms of an absolute value
The absolute value is nonnegative
nonneg' : ∀ (x : R), 0 ≤ MulHom.toFun toMulHom xThe absolute value is positive definitive
eq_zero' : ∀ (x : R), MulHom.toFun toMulHom x = 0 ↔ x = 0The absolute value satisfies the triangle inequality
add_le' : ∀ (x y : R), MulHom.toFun toMulHom (x + y) ≤ MulHom.toFun toMulHom x + MulHom.toFun toMulHom y
AbsoluteValue R S
is the type of absolute values on R
mapping to S
:
the maps that preserve *
, are nonnegative, positive definite and satisfy the triangle equality.
Instances For
Equations
- AbsoluteValue.zeroHomClass = ZeroHomClass.mk (_ : ∀ (f : AbsoluteValue R S), MulHom.toFun f.toMulHom 0 = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- AbsoluteValue.nonnegHomClass = let src := AbsoluteValue.zeroHomClass; NonnegHomClass.mk (_ : ∀ (f : AbsoluteValue R S) (x : R), 0 ≤ MulHom.toFun f.toMulHom x)
Equations
- One or more equations did not get rendered due to their size.
See Note [custom simps projection].
Equations
Equations
- One or more equations did not get rendered due to their size.
Absolute values from a nontrivial R
to a linear ordered ring preserve *
, 0
and 1
.
Equations
- AbsoluteValue.toMonoidWithZeroHom abv = ↑abv
Absolute values from a nontrivial R
to a linear ordered ring preserve *
and 1
.
Equations
- AbsoluteValue.toMonoidHom abv = ↑abv
AbsoluteValue.abs
is abs
as a bundled AbsoluteValue
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AbsoluteValue.instInhabitedAbsoluteValueToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToOrderedSemiring = { default := AbsoluteValue.abs }
The absolute value is nonnegative
abv_nonneg' : ∀ (x : R), 0 ≤ f xThe absolute value is positive definitive
The absolute value satisfies the triangle inequality
The absolute value is multiplicative
A function f
is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.
See also the type AbsoluteValue
which represents a bundled version of absolute values.
Instances
A bundled absolute value is an absolute value.
Convert an unbundled IsAbsoluteValue
to a bundled AbsoluteValue
.
Equations
- One or more equations did not get rendered due to their size.
abv
as a MonoidWithZeroHom
.
Equations
An absolute value as a monoid with zero homomorphism, assuming the target is a semifield.