Nonnegative real numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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,conditionally_complete_linear_order_bot
; -
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:linear_ordered_semiring ℝ≥0
;ordered_comm_semiring ℝ≥0
;canonically_ordered_comm_semiring ℝ≥0
;linear_ordered_comm_group_with_zero ℝ≥0
;canonically_linear_ordered_add_monoid ℝ≥0
;archimedean ℝ≥0
;conditionally_complete_linear_order_bot ℝ≥0
.
These instances are derived from corresponding instances about the type
{x : α // 0 ≤ x}
in an appropriate ordered field/ring/group/monoidα
. Seealgebra/order/nonneg
. -
real.to_nnreal x
is defined as⟨max x 0, _⟩
, i.e.↑(real.to_nnreal x) = x
when0 ≤ x
and↑(real.to_nnreal x) = 0
otherwise.
We also define an instance can_lift ℝ ℝ≥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 occurences
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
.
Nonnegative real numbers.
Instances for nnreal
- nnreal.strict_ordered_semiring
- nnreal.comm_monoid_with_zero
- nnreal.floor_semiring
- nnreal.comm_semiring
- nnreal.semiring
- nnreal.semilattice_inf
- nnreal.semilattice_sup
- nnreal.distrib_lattice
- nnreal.densely_ordered
- nnreal.order_bot
- nnreal.canonically_linear_ordered_semifield
- nnreal.linear_ordered_comm_group_with_zero
- nnreal.archimedean
- nnreal.linear_ordered_semiring
- nnreal.ordered_comm_semiring
- nnreal.canonically_ordered_comm_semiring
- nnreal.has_sub
- nnreal.has_ordered_sub
- nnreal.has_div
- nnreal.inhabited
- nnreal.real.has_coe
- nnreal.can_lift
- nnreal.mul_action
- nnreal.is_scalar_tower
- nnreal.smul_comm_class_left
- nnreal.smul_comm_class_right
- nnreal.distrib_mul_action
- nnreal.module
- nnreal.algebra
- nnreal.conditionally_complete_linear_order_bot
- nnreal.covariant_add
- nnreal.contravariant_add
- nnreal.covariant_mul
- ennreal.has_coe
- ennreal.can_lift
- ennreal.mul_action
- ennreal.is_scalar_tower
- ennreal.smul_comm_class_left
- ennreal.smul_comm_class_right
- ennreal.distrib_mul_action
- ennreal.module
- ennreal.algebra
- nnreal.pseudo_metric_space
- nnreal.metric_space
- nnreal.topological_space
- nnreal.topological_semiring
- nnreal.topological_space.second_countable_topology
- nnreal.order_topology
- nnreal.has_continuous_sub
- nnreal.has_continuous_inv₀
- nnreal.has_continuous_smul
- nnreal.has_lipschitz_add
- nnreal.has_bounded_smul
- nnreal.measurable_space
- nnreal.borel_space
- nnreal.real.has_pow
- nnreal.has_measurable_pow
- measure_theory.jordan_decomposition.has_smul
- measure_theory.finite_measure.module
- convex_body.module
Equations
- nnreal.real.has_coe = {coe := subtype.val (λ (r : ℝ), 0 ≤ r)}
Equations
- nnreal.can_lift = subtype.can_lift (λ (r : ℝ), 0 ≤ r)
Reinterpret a real number r
as a non-negative real number. Returns 0
if r < 0
.
Equations
- r.to_nnreal = ⟨linear_order.max r 0, _⟩
Coercion ℝ≥0 → ℝ
as a ring_hom
.
Equations
A mul_action
over ℝ
restricts to a mul_action
over ℝ≥0
.
A distrib_mul_action
over ℝ
restricts to a distrib_mul_action
over ℝ≥0
.
An algebra
over ℝ
restricts to an algebra
over ℝ≥0
.
Equations
- nnreal.algebra = {to_has_smul := {smul := has_smul.smul smul_zero_class.to_has_smul}, to_ring_hom := (algebra_map ℝ A).comp nnreal.to_real_hom, commutes' := _, smul_def' := _}
real.to_nnreal
and coe : ℝ≥0 → ℝ
form a Galois insertion.
Equations
- nnreal.gi = galois_insertion.monotone_intro nnreal.coe_mono real.to_nnreal_mono real.le_coe_to_nnreal nnreal.gi._proof_1
If a
is a nonnegative real number, then the closed interval [0, a]
in ℝ
is order
isomorphic to the interval set.Iic a
.
Equations
- a.order_iso_Icc_zero_coe = {to_equiv := equiv.set.sep (set.Ici 0) (λ (x : ℝ), x ≤ ↑a), map_rel_iff' := _}
Equations
- nnreal.conditionally_complete_linear_order_bot = nonneg.conditionally_complete_linear_order_bot nnreal.conditionally_complete_linear_order_bot._proof_1
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 has_ordered_sub
in the file algebra.order.sub
. See also mul_tsub
and tsub_mul
.