mathlib documentation

data.real.nnreal

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:

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.

def nnreal  :
Type

Nonnegative real numbers.

Equations
@[instance]

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

@[instance]

Equations
theorem nnreal.eq {n m : ℝ≥0} :
n = mn = m

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

theorem nnreal.ne_iff {x y : ℝ≥0} :
x y x y

def nnreal.of_real  :

Reinterpret a real number r as a non-negative real number. Returns 0 if r < 0.

Equations
theorem nnreal.coe_of_real (r : ) :
0 r(nnreal.of_real r) = r

theorem nnreal.coe_nonneg (r : ℝ≥0) :
0 r

theorem nnreal.coe_mk (a : ) (ha : 0 a) :
a, ha⟩ = a

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

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

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

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

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

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

@[simp]
theorem nnreal.coe_inv (r : ℝ≥0) :

@[simp]
theorem nnreal.coe_bit0 (r : ℝ≥0) :

@[simp]
theorem nnreal.coe_bit1 (r : ℝ≥0) :

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

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

theorem nnreal.coe_ne_zero {r : ℝ≥0} :
r 0 r 0

@[instance]

Equations
@[instance]

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

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

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

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

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

theorem nnreal.nsmul_coe (r : ℝ≥0) (n : ) :

@[simp]
theorem nnreal.coe_nat_cast (n : ) :

theorem nnreal.coe_le_coe {r₁ r₂ : ℝ≥0} :
r₁ r₂ r₁ r₂

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

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

@[simp]

@[instance]

Equations
@[instance]

Equations
@[instance]

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

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

@[instance]

Equations
theorem nnreal.le_of_forall_epsilon_le {a b : ℝ≥0} :
(∀ (ε : ℝ≥0), 0 < εa b + ε)a b

theorem nnreal.bot_eq_zero  :
= 0

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

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

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

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

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

@[simp]

@[simp]

@[simp]
theorem nnreal.of_real_pos {r : } :

@[simp]
theorem nnreal.of_real_eq_zero {r : } :

theorem nnreal.of_real_of_nonpos {r : } :
r 0nnreal.of_real r = 0

@[simp]

@[simp]
theorem nnreal.of_real_add {r p : } :

theorem nnreal.le_of_real_iff_coe_le {r : ℝ≥0} {p : } :
0 p(r nnreal.of_real p r p)

theorem nnreal.of_real_lt_iff_lt_coe {r : } {p : ℝ≥0} :
0 r(nnreal.of_real r < p r < p)

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

theorem nnreal.of_real_mul {p q : } :

theorem nnreal.mul_ne_zero' {a b : ℝ≥0} :
a 0b 0a * b 0

theorem nnreal.sub_def {r p : ℝ≥0} :

theorem nnreal.sub_eq_zero {r p : ℝ≥0} :
r pr - p = 0

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

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

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

theorem nnreal.sub_lt_self {r p : ℝ≥0} :
0 < r0 < pr - p < r

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

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

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

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

@[simp]
theorem nnreal.sub_add_cancel_of_le {a b : ℝ≥0} :
b aa - b + b = a

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

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

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

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

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

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

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

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

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

theorem nnreal.div_pos {r p : ℝ≥0} :
0 < r0 < p0 < r / p

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

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

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

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

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

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

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

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

@[simp]
theorem nnreal.mul_div_cancel {r p : ℝ≥0} :
p 0r * p / p = r

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

@[simp]
theorem nnreal.inv_inv {r : ℝ≥0} :

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

theorem nnreal.inv_le_of_le_mul {r p : ℝ≥0} :
1 r * pr⁻¹ p

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

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

theorem nnreal.mul_le_iff_le_inv {a b r : ℝ≥0} :
r 0(r * a b a r⁻¹ * b)

theorem nnreal.le_div_iff_mul_le {a b r : ℝ≥0} :
r 0(a b / r a * r b)

theorem nnreal.div_le_iff {a b r : ℝ≥0} :
r 0(a / r b a b * r)

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

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

theorem nnreal.half_pos {a : ℝ≥0} :
0 < a0 < a / 2

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

theorem nnreal.half_lt_self {a : ℝ≥0} :
a 0a / 2 < a

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

theorem nnreal.div_lt_one_of_lt {a b : ℝ≥0} :
a < ba / b < 1

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

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

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

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

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

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

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

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

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

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

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

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

theorem nnreal.div_eq_div_iff {a b c d : ℝ≥0} :
b 0d 0(a / b = c / d a * d = c * b)

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

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

theorem nnreal.pow_eq_zero {a : ℝ≥0} {n : } :
a ^ n = 0a = 0

theorem nnreal.pow_ne_zero {a : ℝ≥0} (n : ) :
a 0a ^ n 0

@[simp]
theorem nnreal.abs_eq (x : ℝ≥0) :

def real.nnabs  :

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

Equations
@[simp]
theorem nnreal.coe_nnabs (x : ) :