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
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.
- toFun : R → S
- nonneg' (x : R) : 0 ≤ self.toFun x
The absolute value is nonnegative
The absolute value is positive definitive
The absolute value satisfies the triangle inequality
Instances For
Equations
- AbsoluteValue.funLike = { coe := fun (f : AbsoluteValue R S) => f.toFun, coe_injective' := ⋯ }
See Note [custom simps projection].
Equations
Instances For
Absolute values from a nontrivial R
to a linear ordered ring preserve *
, 0
and 1
.
Equations
- abv.toMonoidWithZeroHom = ↑abv
Instances For
Absolute values from a nontrivial R
to a linear ordered ring preserve *
and 1
.
Equations
- abv.toMonoidHom = ↑abv
Instances For
Bound abv (a + b)
from below
Bound abv (a - b)
from above
AbsoluteValue.abs
is abs
as a bundled AbsoluteValue
.
Equations
- AbsoluteValue.abs = { toFun := abs, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }
Instances For
Equations
- AbsoluteValue.instInhabited = { default := AbsoluteValue.abs }
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.
- abv_nonneg' (x : R) : 0 ≤ f x
The absolute value is nonnegative
The absolute value is positive definitive
The absolute value satisfies the triangle inequality
The absolute value is multiplicative
Instances
The positivity
extension which identifies expressions of the form abv a
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A bundled absolute value is an absolute value.
Convert an unbundled IsAbsoluteValue
to a bundled AbsoluteValue
.
Equations
- IsAbsoluteValue.toAbsoluteValue abv = { toFun := abv, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }
Instances For
abv
as a MonoidWithZeroHom
.
Equations
- IsAbsoluteValue.abvHom abv = (IsAbsoluteValue.toAbsoluteValue abv).toMonoidWithZeroHom
Instances For
An absolute value as a monoid with zero homomorphism, assuming the target is a semifield.
Equations
- IsAbsoluteValue.abvHom' abv = { toFun := abv, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }