mathlib documentation

data.real.nnreal

source
def nnreal  :
Type

Nonnegative real numbers.

Equations
source
@[instance]
def nnreal.has_coe  :
has_coe ℝ≥0 ℝ

Equations
source
@[simp]
theorem nnreal.val_eq_coe (n : ℝ≥0) :
n.val = ↑n

source
@[instance]
def nnreal.can_lift  :
can_lift ℝ ℝ≥0

Equations
source
theorem nnreal.eq {n m : ℝ≥0} (a : ↑n = ↑m) :
n = m

source
theorem nnreal.eq_iff {n m : ℝ≥0} :
↑n = ↑m ↔ n = m

source
theorem nnreal.ne_iff {x y : ℝ≥0} :
↑x ≠ ↑y ↔ x ≠ y

source
def nnreal.of_real (r : ℝ) :
ℝ≥0

Equations
source
theorem nnreal.coe_of_real (r : ℝ) (hr : 0 ≤ r) :
↑(nnreal.of_real r) = r

source
theorem nnreal.le_coe_of_real (r : ℝ) :
r ≤ ↑(nnreal.of_real r)

source
theorem nnreal.coe_nonneg (r : ℝ≥0) :
0 ≤ ↑r

source
theorem nnreal.coe_mk (a : ℝ) (ha : 0 ≤ a) :
↑⟨a, ha⟩ = a

source
@[instance]
def nnreal.has_zero  :
has_zero ℝ≥0

Equations
source
@[instance]
def nnreal.has_one  :
has_one ℝ≥0

Equations
source
@[instance]
def nnreal.has_add  :
has_add ℝ≥0

Equations
source
@[instance]
def nnreal.has_sub  :
has_sub ℝ≥0

Equations
source
@[instance]
def nnreal.has_mul  :
has_mul ℝ≥0

Equations
source
@[instance]
def nnreal.has_inv  :
has_inv ℝ≥0

Equations
source
@[instance]
def nnreal.has_le  :
has_le ℝ≥0

Equations
source
@[instance]
def nnreal.has_bot  :
has_bot ℝ≥0

Equations
source
@[instance]
def nnreal.inhabited  :
inhabited ℝ≥0

Equations
source
@[simp]
theorem nnreal.coe_eq {r₁ r₂ : ℝ≥0} :
↑r₁ = ↑r₂ ↔ r₁ = r₂

source
@[simp]
theorem nnreal.coe_zero  :
↑0 = 0

source
@[simp]
theorem nnreal.coe_one  :
↑1 = 1

source
@[simp]
theorem nnreal.coe_add (r₁ r₂ : ℝ≥0) :
↑(r₁ + r₂) = ↑r₁ + ↑r₂

source
@[simp]
theorem nnreal.coe_mul (r₁ r₂ : ℝ≥0) :
↑r₁ * r₂ = (↑r₁) * ↑r₂

source
@[simp]
theorem nnreal.coe_inv (r : ℝ≥0) :
↑r⁻¹ = (↑r)⁻¹

source
@[simp]
theorem nnreal.coe_bit0 (r : ℝ≥0) :
↑(bit0 r) = bit0 ↑r

source
@[simp]
theorem nnreal.coe_bit1 (r : ℝ≥0) :
↑(bit1 r) = bit1 ↑r

source
@[simp]
theorem nnreal.coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) :
↑(r₁ - r₂) = ↑r₁ - ↑r₂

source
@[simp]
theorem nnreal.coe_eq_zero (r : ℝ≥0) :
↑r = 0 ↔ r = 0

source
theorem nnreal.coe_ne_zero {r : ℝ≥0} :
↑r ≠ 0 ↔ r ≠ 0

source
@[instance]
def nnreal.comm_semiring  :
comm_semiring ℝ≥0

Equations
source
def nnreal.to_real_hom  :
ℝ≥0 →+* ℝ

Coercion ℝ≥0 → ℝ as a ring_hom.

Equations
source
@[simp]
theorem nnreal.coe_to_real_hom  :
⇑nnreal.to_real_hom = coe

source
@[instance]
def nnreal.comm_group_with_zero  :
comm_group_with_zero ℝ≥0

Equations
source
@[simp]
theorem nnreal.coe_indicator {α : Type u_1} (s : set α) (f : α → ℝ≥0) (a : α) :
↑(s.indicator f a) = s.indicator (λ (x : α), ↑(f x)) a

source
@[simp]
theorem nnreal.coe_div (r₁ r₂ : ℝ≥0) :
↑(r₁ / r₂) = ↑r₁ / ↑r₂

source
theorem nnreal.coe_pow (r : ℝ≥0) (n : ℕ) :
↑(r ^ n) = ↑r ^ n

source
theorem nnreal.coe_list_sum (l : list ℝ≥0) :
↑(l.sum) = (list.map coe l).sum

source
theorem nnreal.coe_list_prod (l : list ℝ≥0) :
↑(l.prod) = (list.map coe l).prod

source
theorem nnreal.coe_multiset_sum (s : multiset ℝ≥0) :
↑(s.sum) = (multiset.map coe s).sum

source
theorem nnreal.coe_multiset_prod (s : multiset ℝ≥0) :
↑(s.prod) = (multiset.map coe s).prod

source
theorem nnreal.coe_sum {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
↑∑ (a : α) in s, f a = ∑ (a : α) in s, ↑(f a)

source
theorem nnreal.coe_prod {α : Type u_1} {s : finset α} {f : α → ℝ≥0} :
↑∏ (a : α) in s, f a = ∏ (a : α) in s, ↑(f a)

source
theorem nnreal.nsmul_coe (r : ℝ≥0) (n : ℕ) :
↑(n •ℕ r) = n •ℕ ↑r

source
@[simp]
theorem nnreal.coe_nat_cast (n : ℕ) :
↑↑n = ↑n

source
@[instance]
def nnreal.decidable_linear_order  :
decidable_linear_order ℝ≥0

Equations
source
theorem nnreal.coe_le_coe {r₁ r₂ : ℝ≥0} :
↑r₁ ≤ ↑r₂ ↔ r₁ ≤ r₂

source
theorem nnreal.coe_lt_coe {r₁ r₂ : ℝ≥0} :
↑r₁ < ↑r₂ ↔ r₁ < r₂

source
theorem nnreal.coe_pos {r : ℝ≥0} :
0 < ↑r ↔ 0 < r

source
theorem nnreal.coe_mono  :
monotone coe

source
theorem nnreal.of_real_mono  :
monotone nnreal.of_real

source
@[simp]
theorem nnreal.of_real_coe {r : ℝ≥0} :
nnreal.of_real ↑r = r

source
def nnreal.gi  :
galois_insertion nnreal.of_real coe

nnreal.of_real and coe : ℝ≥0 → ℝ form a Galois insertion.

Equations
source
@[instance]
def nnreal.order_bot  :
order_bot ℝ≥0

Equations
source
@[instance]
def nnreal.canonically_ordered_add_monoid  :
canonically_ordered_add_monoid ℝ≥0

Equations
source
@[instance]
def nnreal.distrib_lattice  :
distrib_lattice ℝ≥0

Equations
source
@[instance]
def nnreal.semilattice_inf_bot  :
semilattice_inf_bot ℝ≥0

Equations
source
@[instance]
def nnreal.semilattice_sup_bot  :
semilattice_sup_bot ℝ≥0

Equations
source
@[instance]
def nnreal.linear_ordered_semiring  :
linear_ordered_semiring ℝ≥0

Equations
source
@[instance]
def nnreal.linear_ordered_comm_group_with_zero  :
linear_ordered_comm_group_with_zero ℝ≥0

Equations
source
@[instance]
def nnreal.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring ℝ≥0

Equations
source
@[instance]
def nnreal.densely_ordered  :
densely_ordered ℝ≥0

source
@[instance]
def nnreal.no_top_order  :
no_top_order ℝ≥0

source
theorem nnreal.bdd_above_coe {s : set ℝ≥0} :
bdd_above (coe '' s) ↔ bdd_above s

source
theorem nnreal.bdd_below_coe (s : set ℝ≥0) :
bdd_below (coe '' s)

source
@[instance]
def nnreal.has_Sup  :
has_Sup ℝ≥0

Equations
source
@[instance]
def nnreal.has_Inf  :
has_Inf ℝ≥0

Equations
source
theorem nnreal.coe_Sup (s : set ℝ≥0) :
↑(Sup s) = Sup (coe '' s)

source
theorem nnreal.coe_Inf (s : set ℝ≥0) :
↑(Inf s) = Inf (coe '' s)

source
@[instance]
def nnreal.conditionally_complete_linear_order_bot  :
conditionally_complete_linear_order_bot ℝ≥0

Equations
source
@[instance]
def nnreal.archimedean  :
archimedean ℝ≥0

source
theorem nnreal.le_of_forall_epsilon_le {a b : ℝ≥0} (h : ∀ (ε : ℝ≥0), 0 < ε → a ≤ b + ε) :
a ≤ b

source
theorem nnreal.lt_iff_exists_rat_btwn (a b : ℝ≥0) :
a < b ↔ ∃ (q : ℚ), 0 ≤ q ∧ a < nnreal.of_real ↑q ∧ nnreal.of_real ↑q < b

source
theorem nnreal.bot_eq_zero  :
⊥ = 0

source
theorem nnreal.mul_sup (a b c : ℝ≥0) :
a * (b ⊔ c) = a * b ⊔ a * c

source
theorem nnreal.mul_finset_sup {α : Type u_1} {f : α → ℝ≥0} {s : finset α} (r : ℝ≥0) :
r * s.sup f = s.sup (λ (a : α), r * f a)

source
@[simp]
theorem nnreal.coe_max (x y : ℝ≥0) :
↑(max x y) = max ↑x ↑y

source
@[simp]
theorem nnreal.coe_min (x y : ℝ≥0) :
↑(min x y) = min ↑x ↑y

source
@[simp]
theorem nnreal.zero_le_coe {q : ℝ≥0} :
0 ≤ ↑q

source
@[simp]
theorem nnreal.of_real_zero  :
nnreal.of_real 0 = 0

source
@[simp]
theorem nnreal.of_real_one  :
nnreal.of_real 1 = 1

source
@[simp]
theorem nnreal.of_real_pos {r : ℝ} :
0 < nnreal.of_real r ↔ 0 < r

source
@[simp]
theorem nnreal.of_real_eq_zero {r : ℝ} :
nnreal.of_real r = 0 ↔ r ≤ 0

source
theorem nnreal.of_real_of_nonpos {r : ℝ} (a : r ≤ 0) :
nnreal.of_real r = 0

source
@[simp]
theorem nnreal.of_real_le_of_real_iff {r p : ℝ} (hp : 0 ≤ p) :
nnreal.of_real r ≤ nnreal.of_real p ↔ r ≤ p

source
@[simp]
theorem nnreal.of_real_lt_of_real_iff' {r p : ℝ} :
nnreal.of_real r < nnreal.of_real p ↔ r < p ∧ 0 < p

source
theorem nnreal.of_real_lt_of_real_iff {r p : ℝ} (h : 0 < p) :
nnreal.of_real r < nnreal.of_real p ↔ r < p

source
theorem nnreal.of_real_lt_of_real_iff_of_nonneg {r p : ℝ} (hr : 0 ≤ r) :
nnreal.of_real r < nnreal.of_real p ↔ r < p

source
@[simp]
theorem nnreal.of_real_add {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
nnreal.of_real (r + p) = nnreal.of_real r + nnreal.of_real p

source
theorem nnreal.of_real_add_of_real {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
nnreal.of_real r + nnreal.of_real p = nnreal.of_real (r + p)

source
theorem nnreal.of_real_le_of_real {r p : ℝ} (h : r ≤ p) :
nnreal.of_real r ≤ nnreal.of_real p

source
theorem nnreal.of_real_add_le {r p : ℝ} :
nnreal.of_real (r + p) ≤ nnreal.of_real r + nnreal.of_real p

source
theorem nnreal.of_real_le_iff_le_coe {r : ℝ} {p : ℝ≥0} :
nnreal.of_real r ≤ p ↔ r ≤ ↑p

source
theorem nnreal.le_of_real_iff_coe_le {r : ℝ≥0} {p : ℝ} (hp : 0 ≤ p) :
r ≤ nnreal.of_real p ↔ ↑r ≤ p

source
theorem nnreal.of_real_lt_iff_lt_coe {r : ℝ} {p : ℝ≥0} (ha : 0 ≤ r) :
nnreal.of_real r < p ↔ r < ↑p

source
theorem nnreal.lt_of_real_iff_coe_lt {r : ℝ≥0} {p : ℝ} :
r < nnreal.of_real p ↔ ↑r < p

source
theorem nnreal.mul_eq_mul_left {a b c : ℝ≥0} (h : a ≠ 0) :
a * b = a * c ↔ b = c

source
theorem nnreal.of_real_mul {p q : ℝ} (hp : 0 ≤ p) :
nnreal.of_real (p * q) = (nnreal.of_real p) * nnreal.of_real q

source
theorem nnreal.mul_ne_zero' {a b : ℝ≥0} (h₁ : a ≠ 0) (h₂ : b ≠ 0) :
a * b ≠ 0

source
theorem nnreal.sub_def {r p : ℝ≥0} :
r - p = nnreal.of_real (↑r - ↑p)

source
theorem nnreal.sub_eq_zero {r p : ℝ≥0} (h : r ≤ p) :
r - p = 0

source
@[simp]
theorem nnreal.sub_self {r : ℝ≥0} :
r - r = 0

source
@[simp]
theorem nnreal.sub_zero {r : ℝ≥0} :
r - 0 = r

source
theorem nnreal.sub_pos {r p : ℝ≥0} :
0 < r - p ↔ p < r

source
theorem nnreal.sub_lt_self {r p : ℝ≥0} (a : 0 < r) (a_1 : 0 < p) :
r - p < r

source
@[simp]
theorem nnreal.sub_le_iff_le_add {r p q : ℝ≥0} :
r - p ≤ q ↔ r ≤ q + p

source
@[simp]
theorem nnreal.sub_le_self {r p : ℝ≥0} :
r - p ≤ r

source
theorem nnreal.add_sub_cancel {r p : ℝ≥0} :
p + r - r = p

source
theorem nnreal.add_sub_cancel' {r p : ℝ≥0} :
r + p - r = p

source
@[simp]
theorem nnreal.sub_add_cancel_of_le {a b : ℝ≥0} (h : b ≤ a) :
a - b + b = a

source
theorem nnreal.sub_sub_cancel_of_le {r p : ℝ≥0} (h : r ≤ p) :
p - (p - r) = r

source
theorem nnreal.lt_sub_iff_add_lt {p q r : ℝ≥0} :
p < q - r ↔ p + r < q

source
theorem nnreal.sub_lt_iff_lt_add {a b c : ℝ≥0} (h : b ≤ a) :
a - b < c ↔ a < b + c

source
theorem nnreal.sub_eq_iff_eq_add {a b c : ℝ≥0} (h : b ≤ a) :
a - b = c ↔ a = c + b

source
theorem nnreal.div_def {r p : ℝ≥0} :
r / p = r * p⁻¹

source
theorem nnreal.sum_div {ι : Type u_1} (s : finset ι) (f : ι → ℝ≥0) (b : ℝ≥0) :
(∑ (i : ι) in s, f i) / b = ∑ (i : ι) in s, f i / b

source
@[simp]
theorem nnreal.inv_zero  :
0⁻¹ = 0

source
@[simp]
theorem nnreal.inv_eq_zero {r : ℝ≥0} :
r⁻¹ = 0 ↔ r = 0

source
@[simp]
theorem nnreal.inv_pos {r : ℝ≥0} :
0 < r⁻¹ ↔ 0 < r

source
theorem nnreal.div_pos {r p : ℝ≥0} (hr : 0 < r) (hp : 0 < p) :
0 < r / p

source
@[simp]
theorem nnreal.inv_one  :
1⁻¹ = 1

source
@[simp]
theorem nnreal.div_one {r : ℝ≥0} :
r / 1 = r

source
theorem nnreal.mul_inv {r p : ℝ≥0} :
(r * p)⁻¹ = p⁻¹ * r⁻¹

source
theorem nnreal.inv_pow {r : ℝ≥0} {n : ℕ} :
(r ^ n)⁻¹ = r⁻¹ ^ n

source
@[simp]
theorem nnreal.inv_mul_cancel {r : ℝ≥0} (h : r ≠ 0) :
r⁻¹ * r = 1

source
@[simp]
theorem nnreal.mul_inv_cancel {r : ℝ≥0} (h : r ≠ 0) :
r * r⁻¹ = 1

source
@[simp]
theorem nnreal.div_self {r : ℝ≥0} (h : r ≠ 0) :
r / r = 1

source
theorem nnreal.div_self_le (r : ℝ≥0) :
r / r ≤ 1

source
@[simp]
theorem nnreal.mul_div_cancel {r p : ℝ≥0} (h : p ≠ 0) :
r * p / p = r

source
@[simp]
theorem nnreal.mul_div_cancel' {r p : ℝ≥0} (h : r ≠ 0) :
r * (p / r) = p

source
@[simp]
theorem nnreal.inv_inv {r : ℝ≥0} :
r⁻¹⁻¹ = r

source
@[simp]
theorem nnreal.inv_le {r p : ℝ≥0} (h : r ≠ 0) :
r⁻¹ ≤ p ↔ 1 ≤ r * p

source
theorem nnreal.inv_le_of_le_mul {r p : ℝ≥0} (h : 1 ≤ r * p) :
r⁻¹ ≤ p

source
@[simp]
theorem nnreal.le_inv_iff_mul_le {r p : ℝ≥0} (h : p ≠ 0) :
r ≤ p⁻¹ ↔ r * p ≤ 1

source
@[simp]
theorem nnreal.lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) :
r < p⁻¹ ↔ r * p < 1

source
theorem nnreal.mul_le_iff_le_inv {a b r : ℝ≥0} (hr : r ≠ 0) :
r * a ≤ b ↔ a ≤ r⁻¹ * b

source
theorem nnreal.le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) :
a ≤ b / r ↔ a * r ≤ b

source
theorem nnreal.div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) :
a / r ≤ b ↔ a ≤ b * r

source
theorem nnreal.le_of_forall_lt_one_mul_lt {x y : ℝ≥0} (h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y) :
x ≤ y

source
theorem nnreal.div_add_div_same (a b c : ℝ≥0) :
a / c + b / c = (a + b) / c

source
theorem nnreal.half_pos {a : ℝ≥0} (h : 0 < a) :
0 < a / 2

source
theorem nnreal.add_halves (a : ℝ≥0) :
a / 2 + a / 2 = a

source
theorem nnreal.half_lt_self {a : ℝ≥0} (h : a ≠ 0) :
a / 2 < a

source
theorem nnreal.two_inv_lt_one  :
2⁻¹ < 1

source
theorem nnreal.div_lt_iff {a b c : ℝ≥0} (hc : c ≠ 0) :
b / c < a ↔ b < a * c

source
theorem nnreal.div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) :
a / b < 1

source
theorem nnreal.div_pow {a b : ℝ≥0} (n : ℕ) :
(a / b) ^ n = a ^ n / b ^ n

source
theorem nnreal.mul_div_assoc' (a b c : ℝ≥0) :
a * (b / c) = a * b / c

source
theorem nnreal.div_add_div (a : ℝ≥0) {b : ℝ≥0} (c : ℝ≥0) {d : ℝ≥0} (hb : b ≠ 0) (hd : d ≠ 0) :
a / b + c / d = (a * d + b * c) / b * d

source
theorem nnreal.inv_eq_one_div (a : ℝ≥0) :
a⁻¹ = 1 / a

source
theorem nnreal.div_mul_eq_mul_div (a b c : ℝ≥0) :
(a / b) * c = a * c / b

source
theorem nnreal.add_div' (a b c : ℝ≥0) (hc : c ≠ 0) :
b + a / c = (b * c + a) / c

source
theorem nnreal.div_add' (a b c : ℝ≥0) (hc : c ≠ 0) :
a / c + b = (a + b * c) / c

source
theorem nnreal.one_div (a : ℝ≥0) :
1 / a = a⁻¹

source
theorem nnreal.one_div_div (a b : ℝ≥0) :
1 / (a / b) = b / a

source
theorem nnreal.div_eq_mul_one_div (a b : ℝ≥0) :
a / b = a * (1 / b)

source
theorem nnreal.div_div_eq_mul_div (a b c : ℝ≥0) :
a / (b / c) = a * c / b

source
theorem nnreal.div_div_eq_div_mul (a b c : ℝ≥0) :
a / b / c = a / b * c

source
theorem nnreal.div_eq_div_iff {a b c d : ℝ≥0} (hb : b ≠ 0) (hd : d ≠ 0) :
a / b = c / d ↔ a * d = c * b

source
theorem nnreal.div_eq_iff {a b c : ℝ≥0} (hb : b ≠ 0) :
a / b = c ↔ a = c * b

source
theorem nnreal.eq_div_iff {a b c : ℝ≥0} (hb : b ≠ 0) :
c = a / b ↔ c * b = a

source
theorem nnreal.pow_eq_zero {a : ℝ≥0} {n : ℕ} (h : a ^ n = 0) :
a = 0

source
theorem nnreal.pow_ne_zero {a : ℝ≥0} (n : ℕ) (h : a ≠ 0) :
a ^ n ≠ 0

source
@[simp]
theorem nnreal.abs_eq (x : ℝ≥0) :
abs ↑x = ↑x

source
def real.nnabs (x : ℝ) :
ℝ≥0

The absolute value on ℝ as a map to ℝ≥0.

Equations
source
@[simp]
theorem nnreal.coe_nnabs (x : ℝ) :
↑(real.nnabs x) = abs x