Nonnegative real numbers #
In this file we define NNReal
(notation: ℝ≥0
) to be the type of non-negative real numbers,
a.k.a. the interval [0, ∞)
. We also define the following operations and structures on ℝ≥0
:
the order on
ℝ≥0
is the restriction of the order onℝ
; these relations define a conditionally complete linear order with a bottom element,ConditionallyCompleteLinearOrderBot
;a + b
anda * b
are the restrictions of addition and multiplication of real numbers toℝ≥0
; these operations together with0 = ⟨0, _⟩
and1 = ⟨1, _⟩
turnℝ≥0
into a conditionally complete linear ordered archimedean commutative semifield; we have no typeclass for this inmathlib
yet, so we define the following instances instead:LinearOrderedSemiring ℝ≥0
;OrderedCommSemiring ℝ≥0
;CanonicallyOrderedCommSemiring ℝ≥0
;LinearOrderedCommGroupWithZero ℝ≥0
;CanonicallyLinearOrderedAddCommMonoid ℝ≥0
;Archimedean ℝ≥0
;ConditionallyCompleteLinearOrderBot ℝ≥0
.
These instances are derived from corresponding instances about the type
{x : α // 0 ≤ x}
in an appropriate ordered field/ring/group/monoidα
, seeMathlib.Algebra.Order.Nonneg.OrderedRing
.Real.toNNReal x
is defined as⟨max x 0, _⟩
, i.e.↑(Real.toNNReal x) = x
when0 ≤ x
and↑(Real.toNNReal x) = 0
otherwise.
We also define an instance CanLift ℝ ℝ≥0
. This instance can be used by the lift
tactic to
replace x : ℝ
and hx : 0 ≤ x
in the proof context with x : ℝ≥0
while replacing all occurrences
of x
with ↑x
. This tactic also works for a function f : α → ℝ
with a hypothesis
hf : ∀ x, 0 ≤ f x
.
Notations #
This file defines ℝ≥0
as a localized notation for NNReal
.
Equations
- NNReal.«termℝ≥0» = Lean.ParserDescr.node `NNReal.termℝ≥0 1024 (Lean.ParserDescr.symbol "ℝ≥0")
Instances For
Equations
- NNReal.instFloorSemiring = Nonneg.floorSemiring
Equations
Equations
Equations
Equations
- NNReal.instCanonicallyLinearOrderedSemifield = Nonneg.canonicallyLinearOrderedSemifield
Equations
- NNReal.instCoeReal = { coe := NNReal.toReal }
Equations
Alias of NNReal.coe_inj
.
Coercion ℝ≥0 → ℝ
as a RingHom
.
Porting note (#11215): TODO: what if we define Coe ℝ≥0 ℝ
using this function?
Equations
- NNReal.toRealHom = { toFun := NNReal.toReal, map_one' := NNReal.coe_one, map_mul' := NNReal.coe_mul, map_zero' := NNReal.coe_zero, map_add' := NNReal.coe_add }
Instances For
A MulAction
over ℝ
restricts to a MulAction
over ℝ≥0
.
Equations
- NNReal.instMulActionOfReal = MulAction.compHom M ↑NNReal.toRealHom
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A DistribMulAction
over ℝ
restricts to a DistribMulAction
over ℝ≥0
.
Equations
- NNReal.instDistribMulActionOfReal = DistribMulAction.compHom M ↑NNReal.toRealHom
A Module
over ℝ
restricts to a Module
over ℝ≥0
.
Equations
- NNReal.instModuleOfReal = Module.compHom M NNReal.toRealHom
An Algebra
over ℝ
restricts to an Algebra
over ℝ≥0
.
Equations
- NNReal.instAlgebraOfReal = Algebra.mk ((algebraMap ℝ A).comp NNReal.toRealHom) ⋯ ⋯
Alias of NNReal.coe_natCast
.
Alias of NNReal.mk_natCast
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
Equations
Equations
Equations
- ⋯ = ⋯
Alias of Real.toNNReal_eq_natCast
.
Alias of Real.toNNReal_le_natCast
.
Alias of Real.natCast_lt_toNNReal
.
Alias of Real.natCastle_toNNReal'
.
Alias of Real.toNNReal_lt_natCast'
.
Alias of Real.natCast_le_toNNReal
.
Alias of Real.toNNReal_lt_natCast
.
Lemmas about subtraction #
In this section we provide a few lemmas about subtraction that do not fit well into any other
typeclass. For lemmas about subtraction and addition see lemmas about OrderedSub
in the file
Mathlib.Algebra.Order.Sub.Basic
. See also mul_tsub
and tsub_mul
.
The absolute value on ℝ
as a map to ℝ≥0
.
Equations
- Real.nnabs = { toFun := fun (x : ℝ) => ⟨|x|, ⋯⟩, map_zero' := Real.nnabs.proof_2, map_one' := Real.nnabs.proof_3, map_mul' := Real.nnabs.proof_4 }
Instances For
If Γ₀ˣ
is nontrivial and f : Γ₀ →*₀ ℝ≥0
is strictly monotone, then for any positive
r : ℝ≥0
, there exists d : Γ₀ˣ
with f d < r
.
If Γ₀ˣ
is nontrivial and f : Γ₀ →*₀ ℝ≥0
is strictly monotone, then for any positive
real r
, there exists d : Γ₀ˣ
with f d < r
.
Extension for the positivity
tactic: cast from ℝ≥0
to ℝ
.