Documentation

Mathlib.Data.Real.ENNReal

Extended non-negative reals #

We define ENNReal = ℝ≥0∞ := WithTop ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a MeasureTheory.Measure, and of the extended distance edist in an EMetricSpace. In this file we define some algebraic operations and a linear order on ℝ≥0∞ and prove basic properties of these operations, order, and conversions to/from ℝ, ℝ≥0, and ℕ.

Main definitions #

ℝ≥0∞: the extended nonnegative real numbers [0, ∞]; defined as WithTop ℝ≥0; it is equipped with the following structures:
- coercion from ℝ≥0 defined in the natural way;
- the natural structure of a complete dense linear order: ↑p ≤ ↑q ↔ p ≤ q and ∀ a, a ≤ ∞;
- a + b is defined so that ↑p + ↑q = ↑(p + q) for (p q : ℝ≥0) and a + ∞ = ∞ + a = ∞;
- a * b is defined so that ↑p * ↑q = ↑(p * q) for (p q : ℝ≥0), 0 * ∞ = ∞ * 0 = 0, and a * ∞ = ∞ * a = ∞ for a ≠ 0;
- a - b is defined as the minimal d such that a ≤ d + b; this way we have ↑p - ↑q = ↑(p - q), ∞ - ↑p = ∞, ↑p - ∞ = ∞ - ∞ = 0; note that there is no negation, only subtraction;
- a⁻¹ is defined as Inf {b | 1 ≤ a * b}. This way we have (↑p)⁻¹ = ↑(p⁻¹) for p : ℝ≥0, p ≠ 0, 0⁻¹ = ∞, and ∞⁻¹ = 0.
- a / b is defined as a * b⁻¹.
The addition and multiplication defined this way together with 0 = ↑0 and 1 = ↑1 turn ℝ≥0∞ into a canonically ordered commutative semiring of characteristic zero.
Coercions to/from other types:
- coercion ℝ≥0 → ℝ≥0∞ is defined as Coe, so one can use (p : ℝ≥0) in a context that expects a : ℝ≥0∞, and Lean will apply coe automatically;
- ENNReal.toNNReal sends ↑p to p and ∞ to 0;
- ENNReal.toReal := coe ∘ ENNReal.toNNReal sends ↑p, p : ℝ≥0 to (↑p : ℝ) and ∞ to 0;
- ENNReal.ofReal := coe ∘ Real.toNNReal sends x : ℝ to ↑⟨max x 0, _⟩
- ENNReal.neTopEquivNNReal is an equivalence between {a : ℝ≥0∞ // a ≠ 0} and ℝ≥0.

Implementation notes #

We define a CanLift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

Notations #

ℝ≥0∞: the type of the extended nonnegative real numbers;
ℝ≥0: the type of nonnegative real numbers [0, ∞); defined in data.real.nnreal;
∞: a localized notation in ℝ≥0∞ for ⊤ : ℝ≥0∞.

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations

ENNReal = WithTop NNReal

Instances For

def ENNReal.«termℝ≥0∞» :

Lean.ParserDescr

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations

ENNReal.«termℝ≥0∞» = Lean.ParserDescr.node `ENNReal.termℝ≥0∞ 1024 (Lean.ParserDescr.symbol "ℝ≥0∞")

Instances For

def ENNReal.«term∞» :

Lean.ParserDescr

Notation for infinity as an ENNReal number.

Equations

ENNReal.«term∞» = Lean.ParserDescr.node `ENNReal.term∞ 1024 (Lean.ParserDescr.symbol "∞")

Instances For

instance ENNReal.instOrderBotENNRealToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstENNRealDistribLattice :

OrderBot ENNReal

Equations

ENNReal.instOrderBotENNRealToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstENNRealDistribLattice = inferInstanceAs (OrderBot (WithTop NNReal))

instance ENNReal.instBoundedOrderENNRealToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstENNRealDistribLattice :

BoundedOrder ENNReal

Equations

ENNReal.instBoundedOrderENNRealToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstENNRealDistribLattice = inferInstanceAs (BoundedOrder (WithTop NNReal))

instance ENNReal.instCharZeroENNRealToAddMonoidWithOneInstENNRealAddCommMonoidWithOne :

CharZero ENNReal

Equations

ENNReal.instCharZeroENNRealToAddMonoidWithOneInstENNRealAddCommMonoidWithOne = (_ : CharZero (WithTop NNReal))

noncomputable instance ENNReal.instCanonicallyOrderedCommSemiringENNReal :

CanonicallyOrderedCommSemiring ENNReal

Equations

ENNReal.instCanonicallyOrderedCommSemiringENNReal = inferInstanceAs (CanonicallyOrderedCommSemiring (WithTop NNReal))

noncomputable instance ENNReal.instCompleteLinearOrderENNReal :

CompleteLinearOrder ENNReal

Equations

ENNReal.instCompleteLinearOrderENNReal = inferInstanceAs (CompleteLinearOrder (WithTop NNReal))

instance ENNReal.instDenselyOrderedENNRealToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstCanonicallyOrderedCommSemiringENNReal :

DenselyOrdered ENNReal

Equations

ENNReal.instDenselyOrderedENNRealToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstCanonicallyOrderedCommSemiringENNReal = (_ : DenselyOrdered (WithTop NNReal))

noncomputable instance ENNReal.instCanonicallyLinearOrderedAddCommMonoidENNReal :

CanonicallyLinearOrderedAddCommMonoid ENNReal

Equations

ENNReal.instCanonicallyLinearOrderedAddCommMonoidENNReal = inferInstanceAs (CanonicallyLinearOrderedAddCommMonoid (WithTop NNReal))

noncomputable instance ENNReal.instSub :

Equations

ENNReal.instSub = inferInstanceAs (Sub (WithTop NNReal))

noncomputable instance ENNReal.instOrderedSubENNRealToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstCanonicallyOrderedCommSemiringENNRealToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringInstSub :

OrderedSub ENNReal

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ENNReal.instLinearOrderedAddCommMonoidWithTopENNReal :

LinearOrderedAddCommMonoidWithTop ENNReal

Equations

ENNReal.instLinearOrderedAddCommMonoidWithTopENNReal = inferInstanceAs (LinearOrderedAddCommMonoidWithTop (WithTop NNReal))

instance ENNReal.covariantClass_mul_le :

CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x * x_1) fun (x x_1 : ENNReal) => x ≤ x_1

Equations

ENNReal.covariantClass_mul_le = (_ : CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x * x_1) fun (x x_1 : ENNReal) => x ≤ x_1)

instance ENNReal.covariantClass_add_le :

CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x ≤ x_1

Equations

ENNReal.covariantClass_add_le = (_ : CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x ≤ x_1)

noncomputable instance ENNReal.instLinearOrderedCommMonoidWithZeroENNReal :

LinearOrderedCommMonoidWithZero ENNReal

Equations

One or more equations did not get rendered due to their size.

noncomputable instance ENNReal.instUniqueAddUnitsENNRealToAddMonoidToAddMonoidWithOneInstENNRealAddCommMonoidWithOne :

Unique (AddUnits ENNReal)

Equations

One or more equations did not get rendered due to their size.

instance ENNReal.instInhabitedENNReal :

Inhabited ENNReal

Equations

ENNReal.instInhabitedENNReal = { default := 0 }

@[match_pattern]

def ENNReal.ofNNReal :

NNReal → ENNReal

Coercion from ℝ≥0 to ℝ≥0∞.

Equations

ENNReal.ofNNReal = WithTop.some

Instances For

instance ENNReal.instCoeNNRealENNReal :

Coe NNReal ENNReal

Equations

ENNReal.instCoeNNRealENNReal = { coe := ENNReal.ofNNReal }

def ENNReal.recTopCoe {C : ENNReal → Sort u_3} (top : C ⊤) (coe : (x : NNReal) → C ↑x) (x : ENNReal) :

C x

A version of WithTop.recTopCoe that uses ENNReal.ofNNReal.

Equations

ENNReal.recTopCoe top coe x = WithTop.recTopCoe top coe x

Instances For

instance ENNReal.canLift :

CanLift ENNReal NNReal ENNReal.ofNNReal fun (x : ENNReal) => x ≠ ⊤

Equations

ENNReal.canLift = (_ : CanLift (WithTop NNReal) NNReal WithTop.some fun (r : WithTop NNReal) => r ≠ ⊤)

@[simp]

theorem ENNReal.none_eq_top :

none = ⊤

@[simp]

theorem ENNReal.some_eq_coe (a : NNReal) :

some a = ↑a

@[simp]

theorem ENNReal.some_eq_coe' (a : NNReal) :

↑a = ↑a

theorem ENNReal.coe_injective :

Function.Injective ENNReal.ofNNReal

theorem ENNReal.range_coe' :

Set.range ENNReal.ofNNReal = Set.Iio ⊤

theorem ENNReal.range_coe :

Set.range ENNReal.ofNNReal = {⊤}ᶜ

def ENNReal.toNNReal :

ENNReal → NNReal

toNNReal x returns x if it is real, otherwise 0.

Equations

ENNReal.toNNReal = WithTop.untop' 0

Instances For

def ENNReal.toReal (a : ENNReal) :

toReal x returns x if it is real, 0 otherwise.

Equations

ENNReal.toReal a = ↑(ENNReal.toNNReal a)

Instances For

noncomputable def ENNReal.ofReal (r : ℝ) :

ofReal x returns x if it is nonnegative, 0 otherwise.

Equations

ENNReal.ofReal r = ↑(Real.toNNReal r)

Instances For

@[simp]

theorem ENNReal.toNNReal_coe {r : NNReal} :

ENNReal.toNNReal ↑r = r

@[simp]

theorem ENNReal.coe_toNNReal {a : ENNReal} :

a ≠ ⊤ → ↑(ENNReal.toNNReal a) = a

@[simp]

theorem ENNReal.ofReal_toReal {a : ENNReal} (h : a ≠ ⊤) :

ENNReal.ofReal (ENNReal.toReal a) = a

@[simp]

theorem ENNReal.toReal_ofReal {r : ℝ} (h : 0 ≤ r) :

ENNReal.toReal (ENNReal.ofReal r) = r

theorem ENNReal.toReal_ofReal' {r : ℝ} :

ENNReal.toReal (ENNReal.ofReal r) = max r 0

theorem ENNReal.coe_toNNReal_le_self {a : ENNReal} :

↑(ENNReal.toNNReal a) ≤ a

theorem ENNReal.coe_nnreal_eq (r : NNReal) :

↑r = ENNReal.ofReal ↑r

theorem ENNReal.ofReal_eq_coe_nnreal {x : ℝ} (h : 0 ≤ x) :

ENNReal.ofReal x = ↑{ val := x, property := h }

@[simp]

theorem ENNReal.ofReal_coe_nnreal {p : NNReal} :

ENNReal.ofReal ↑p = ↑p

@[simp]

theorem ENNReal.coe_zero :

↑0 = 0

@[simp]

theorem ENNReal.coe_one :

↑1 = 1

@[simp]

theorem ENNReal.toReal_nonneg {a : ENNReal} :

0 ≤ ENNReal.toReal a

@[simp]

theorem ENNReal.top_toNNReal :

ENNReal.toNNReal ⊤ = 0

@[simp]

theorem ENNReal.top_toReal :

ENNReal.toReal ⊤ = 0

@[simp]

theorem ENNReal.one_toReal :

ENNReal.toReal 1 = 1

@[simp]

theorem ENNReal.one_toNNReal :

ENNReal.toNNReal 1 = 1

@[simp]

theorem ENNReal.coe_toReal (r : NNReal) :

ENNReal.toReal ↑r = ↑r

@[simp]

theorem ENNReal.zero_toNNReal :

ENNReal.toNNReal 0 = 0

@[simp]

theorem ENNReal.zero_toReal :

ENNReal.toReal 0 = 0

@[simp]

theorem ENNReal.ofReal_zero :

ENNReal.ofReal 0 = 0

@[simp]

theorem ENNReal.ofReal_one :

ENNReal.ofReal 1 = 1

theorem ENNReal.ofReal_toReal_le {a : ENNReal} :

ENNReal.ofReal (ENNReal.toReal a) ≤ a

theorem ENNReal.forall_ennreal {p : ENNReal → Prop} :

(∀ (a : ENNReal), p a) ↔ (∀ (r : NNReal), p ↑r) ∧ p ⊤

theorem ENNReal.forall_ne_top {p : ENNReal → Prop} :

(∀ (a : ENNReal), a ≠ ⊤ → p a) ↔ ∀ (r : NNReal), p ↑r

theorem ENNReal.exists_ne_top' {p : ENNReal → Prop} :

(∃ (a : ENNReal) (_ : a ≠ ⊤), p a) ↔ ∃ (r : NNReal), p ↑r

theorem ENNReal.exists_ne_top {p : ENNReal → Prop} :

(∃ (a : ENNReal), a ≠ ⊤ ∧ p a) ↔ ∃ (r : NNReal), p ↑r

theorem ENNReal.toNNReal_eq_zero_iff (x : ENNReal) :

ENNReal.toNNReal x = 0 ↔ x = 0 ∨ x = ⊤

theorem ENNReal.toReal_eq_zero_iff (x : ENNReal) :

ENNReal.toReal x = 0 ↔ x = 0 ∨ x = ⊤

theorem ENNReal.toNNReal_ne_zero {a : ENNReal} :

ENNReal.toNNReal a ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤

theorem ENNReal.toReal_ne_zero {a : ENNReal} :

ENNReal.toReal a ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤

theorem ENNReal.toNNReal_eq_one_iff (x : ENNReal) :

ENNReal.toNNReal x = 1 ↔ x = 1

theorem ENNReal.toReal_eq_one_iff (x : ENNReal) :

ENNReal.toReal x = 1 ↔ x = 1

theorem ENNReal.toNNReal_ne_one {a : ENNReal} :

ENNReal.toNNReal a ≠ 1 ↔ a ≠ 1

theorem ENNReal.toReal_ne_one {a : ENNReal} :

ENNReal.toReal a ≠ 1 ↔ a ≠ 1

@[simp]

theorem ENNReal.coe_ne_top {r : NNReal} :

↑r ≠ ⊤

@[simp]

theorem ENNReal.top_ne_coe {r : NNReal} :

⊤ ≠ ↑r

@[simp]

theorem ENNReal.coe_lt_top {r : NNReal} :

↑r < ⊤

@[simp]

theorem ENNReal.ofReal_ne_top {r : ℝ} :

ENNReal.ofReal r ≠ ⊤

@[simp]

theorem ENNReal.ofReal_lt_top {r : ℝ} :

ENNReal.ofReal r < ⊤

@[simp]

theorem ENNReal.top_ne_ofReal {r : ℝ} :

⊤ ≠ ENNReal.ofReal r

@[simp]

theorem ENNReal.ofReal_toReal_eq_iff {a : ENNReal} :

ENNReal.ofReal (ENNReal.toReal a) = a ↔ a ≠ ⊤

@[simp]

theorem ENNReal.toReal_ofReal_eq_iff {a : ℝ} :

ENNReal.toReal (ENNReal.ofReal a) = a ↔ 0 ≤ a

@[simp]

theorem ENNReal.zero_ne_top :

@[simp]

theorem ENNReal.top_ne_zero :

@[simp]

theorem ENNReal.one_ne_top :

@[simp]

theorem ENNReal.top_ne_one :

@[simp]

theorem ENNReal.zero_lt_top :

@[simp]

theorem ENNReal.coe_eq_coe {r : NNReal} {q : NNReal} :

↑r = ↑q ↔ r = q

@[simp]

theorem ENNReal.coe_le_coe {r : NNReal} {q : NNReal} :

↑r ≤ ↑q ↔ r ≤ q

@[simp]

theorem ENNReal.coe_lt_coe {r : NNReal} {q : NNReal} :

↑r < ↑q ↔ r < q

theorem ENNReal.coe_le_coe_of_le {r : NNReal} {q : NNReal} :

r ≤ q → ↑r ≤ ↑q

Alias of the reverse direction of ENNReal.coe_le_coe.

theorem ENNReal.coe_lt_coe_of_le {r : NNReal} {q : NNReal} :

r < q → ↑r < ↑q

Alias of the reverse direction of ENNReal.coe_lt_coe.

theorem ENNReal.coe_mono :

Monotone ENNReal.ofNNReal

theorem ENNReal.coe_strictMono :

StrictMono ENNReal.ofNNReal

@[simp]

theorem ENNReal.coe_eq_zero {r : NNReal} :

↑r = 0 ↔ r = 0

@[simp]

theorem ENNReal.zero_eq_coe {r : NNReal} :

0 = ↑r ↔ 0 = r

@[simp]

theorem ENNReal.coe_eq_one {r : NNReal} :

↑r = 1 ↔ r = 1

@[simp]

theorem ENNReal.one_eq_coe {r : NNReal} :

1 = ↑r ↔ 1 = r

@[simp]

theorem ENNReal.coe_pos {r : NNReal} :

0 < ↑r ↔ 0 < r

theorem ENNReal.coe_ne_zero {r : NNReal} :

↑r ≠ 0 ↔ r ≠ 0

@[simp]

theorem ENNReal.coe_add {r : NNReal} {p : NNReal} :

↑(r + p) = ↑r + ↑p

@[simp]

theorem ENNReal.coe_mul {r : NNReal} {p : NNReal} :

↑(r * p) = ↑r * ↑p

@[simp]

theorem ENNReal.coe_ofNat (n : ℕ) [Nat.AtLeastTwo n] :

↑(OfNat.ofNat n) = OfNat.ofNat n

theorem ENNReal.coe_two :

↑2 = 2

theorem ENNReal.toNNReal_eq_toNNReal_iff (x : ENNReal) (y : ENNReal) :

ENNReal.toNNReal x = ENNReal.toNNReal y ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

theorem ENNReal.toReal_eq_toReal_iff (x : ENNReal) (y : ENNReal) :

ENNReal.toReal x = ENNReal.toReal y ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

theorem ENNReal.toNNReal_eq_toNNReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

ENNReal.toNNReal x = ENNReal.toNNReal y ↔ x = y

theorem ENNReal.toReal_eq_toReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :

ENNReal.toReal x = ENNReal.toReal y ↔ x = y

@[simp]

theorem ENNReal.one_lt_two :

1 < 2

@[simp]

theorem ENNReal.two_ne_top :

@[simp]

theorem ENNReal.two_lt_top :

instance fact_one_le_one_ennreal :

Fact (1 ≤ 1)

(1 : ℝ≥0∞) ≤ 1, recorded as a Fact for use with Lp spaces.

Equations

fact_one_le_one_ennreal = (_ : Fact (1 ≤ 1))

instance fact_one_le_two_ennreal :

Fact (1 ≤ 2)

(1 : ℝ≥0∞) ≤ 2, recorded as a Fact for use with Lp spaces.

Equations

fact_one_le_two_ennreal = (_ : Fact (1 ≤ 2))

instance fact_one_le_top_ennreal :

Fact (1 ≤ ⊤)

(1 : ℝ≥0∞) ≤ ∞, recorded as a Fact for use with Lp spaces.

Equations

fact_one_le_top_ennreal = (_ : Fact (1 ≤ ⊤))

def ENNReal.neTopEquivNNReal :

↑{a : ENNReal | a ≠ ⊤} ≃ NNReal

The set of numbers in ℝ≥0∞ that are not equal to ∞ is equivalent to ℝ≥0.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ENNReal.cinfi_ne_top {α : Type u_1} [InfSet α] (f : ENNReal → α) :

⨅ (x : { x : ENNReal // x ≠ ⊤ }), f ↑x = ⨅ (x : NNReal), f ↑x

theorem ENNReal.iInf_ne_top {α : Type u_1} [CompleteLattice α] (f : ENNReal → α) :

⨅ (x : ENNReal), ⨅ (_ : x ≠ ⊤), f x = ⨅ (x : NNReal), f ↑x

theorem ENNReal.csupr_ne_top {α : Type u_1} [SupSet α] (f : ENNReal → α) :

⨆ (x : { x : ENNReal // x ≠ ⊤ }), f ↑x = ⨆ (x : NNReal), f ↑x

theorem ENNReal.iSup_ne_top {α : Type u_1} [CompleteLattice α] (f : ENNReal → α) :

⨆ (x : ENNReal), ⨆ (_ : x ≠ ⊤), f x = ⨆ (x : NNReal), f ↑x

theorem ENNReal.iInf_ennreal {α : Type u_3} [CompleteLattice α] {f : ENNReal → α} :

⨅ (n : ENNReal), f n = (⨅ (n : NNReal), f ↑n) ⊓ f ⊤

theorem ENNReal.iSup_ennreal {α : Type u_3} [CompleteLattice α] {f : ENNReal → α} :

⨆ (n : ENNReal), f n = (⨆ (n : NNReal), f ↑n) ⊔ f ⊤

def ENNReal.ofNNRealHom :

NNReal →+* ENNReal

Coercion ℝ≥0 → ℝ≥0∞ as a RingHom.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ENNReal.coe_ofNNRealHom :

⇑ENNReal.ofNNRealHom = some

noncomputable instance ENNReal.instMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_3} [MulAction ENNReal M] :

MulAction NNReal M

A MulAction over ℝ≥0∞ restricts to a MulAction over ℝ≥0.

Equations

ENNReal.instMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring = MulAction.compHom M ↑ENNReal.ofNNRealHom

theorem ENNReal.smul_def {M : Type u_3} [MulAction ENNReal M] (c : NNReal) (x : M) :

c • x = ↑c • x

instance ENNReal.instIsScalarTowerNNRealToSMulToMonoidToMonoidWithZeroInstNNRealSemiringInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiringToSMulInstMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_3} {N : Type u_4} [MulAction ENNReal M] [MulAction ENNReal N] [SMul M N] [IsScalarTower ENNReal M N] :

IsScalarTower NNReal M N

Equations

(_ : IsScalarTower NNReal M N) = (_ : IsScalarTower NNReal M N)

instance ENNReal.smulCommClass_left {M : Type u_3} {N : Type u_4} [MulAction ENNReal N] [SMul M N] [SMulCommClass ENNReal M N] :

SMulCommClass NNReal M N

Equations

(_ : SMulCommClass NNReal M N) = (_ : SMulCommClass NNReal M N)

instance ENNReal.smulCommClass_right {M : Type u_3} {N : Type u_4} [MulAction ENNReal N] [SMul M N] [SMulCommClass M ENNReal N] :

SMulCommClass M NNReal N

Equations

(_ : SMulCommClass M NNReal N) = (_ : SMulCommClass M NNReal N)

noncomputable instance ENNReal.instDistribMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring {M : Type u_3} [AddMonoid M] [DistribMulAction ENNReal M] :

DistribMulAction NNReal M

A DistribMulAction over ℝ≥0∞ restricts to a DistribMulAction over ℝ≥0.

Equations

ENNReal.instDistribMulActionNNRealToMonoidToMonoidWithZeroInstNNRealSemiring = DistribMulAction.compHom M ↑ENNReal.ofNNRealHom

noncomputable instance ENNReal.instModuleNNRealInstNNRealSemiring {M : Type u_3} [AddCommMonoid M] [Module ENNReal M] :

Module NNReal M

A Module over ℝ≥0∞ restricts to a Module over ℝ≥0.

Equations

ENNReal.instModuleNNRealInstNNRealSemiring = Module.compHom M ENNReal.ofNNRealHom

noncomputable instance ENNReal.instAlgebraNNRealInstNNRealCommSemiring {A : Type u_3} [Semiring A] [Algebra ENNReal A] :

Algebra NNReal A

An Algebra over ℝ≥0∞ restricts to an Algebra over ℝ≥0.

Equations

One or more equations did not get rendered due to their size.

theorem ENNReal.coe_smul {R : Type u_3} (r : R) (s : NNReal) [SMul R NNReal] [SMul R ENNReal] [IsScalarTower R NNReal NNReal] [IsScalarTower R NNReal ENNReal] :

↑(r • s) = r • ↑s

@[simp]

theorem ENNReal.coe_indicator {α : Type u_3} (s : Set α) (f : α → NNReal) (a : α) :

↑(Set.indicator s f a) = Set.indicator s (fun (x : α) => ↑(f x)) a

@[simp]

theorem ENNReal.coe_pow {r : NNReal} (n : ℕ) :

↑(r ^ n) = ↑r ^ n

@[simp]

theorem ENNReal.add_eq_top {a : ENNReal} {b : ENNReal} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

@[simp]

theorem ENNReal.add_lt_top {a : ENNReal} {b : ENNReal} :

a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

theorem ENNReal.toNNReal_add {r₁ : ENNReal} {r₂ : ENNReal} (h₁ : r₁ ≠ ⊤) (h₂ : r₂ ≠ ⊤) :

ENNReal.toNNReal (r₁ + r₂) = ENNReal.toNNReal r₁ + ENNReal.toNNReal r₂

theorem ENNReal.not_lt_top {x : ENNReal} :

¬x < ⊤ ↔ x = ⊤

theorem ENNReal.add_ne_top {a : ENNReal} {b : ENNReal} :

a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

theorem ENNReal.mul_top' {a : ENNReal} :

a * ⊤ = if a = 0 then 0 else ⊤

@[simp]

theorem ENNReal.mul_top {a : ENNReal} (h : a ≠ 0) :

theorem ENNReal.top_mul' {a : ENNReal} :

⊤ * a = if a = 0 then 0 else ⊤

@[simp]

theorem ENNReal.top_mul {a : ENNReal} (h : a ≠ 0) :

theorem ENNReal.top_mul_top :

⊤ * ⊤ = ⊤

theorem ENNReal.smul_top {R : Type u_3} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] [DecidableEq R] (c : R) :

c • ⊤ = if c = 0 then 0 else ⊤

theorem ENNReal.top_pow {n : ℕ} (h : 0 < n) :

theorem ENNReal.mul_eq_top {a : ENNReal} {b : ENNReal} :

a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

theorem ENNReal.mul_lt_top {a : ENNReal} {b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → a * b < ⊤

theorem ENNReal.mul_ne_top {a : ENNReal} {b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤

theorem ENNReal.lt_top_of_mul_ne_top_left {a : ENNReal} {b : ENNReal} (h : a * b ≠ ⊤) (hb : b ≠ 0) :

theorem ENNReal.lt_top_of_mul_ne_top_right {a : ENNReal} {b : ENNReal} (h : a * b ≠ ⊤) (ha : a ≠ 0) :

theorem ENNReal.mul_lt_top_iff {a : ENNReal} {b : ENNReal} :

a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

theorem ENNReal.mul_self_lt_top_iff {a : ENNReal} :

a * a < ⊤ ↔ a < ⊤

theorem ENNReal.mul_pos_iff {a : ENNReal} {b : ENNReal} :

0 < a * b ↔ 0 < a ∧ 0 < b

theorem ENNReal.mul_pos {a : ENNReal} {b : ENNReal} (ha : a ≠ 0) (hb : b ≠ 0) :

0 < a * b

@[simp]

theorem ENNReal.pow_eq_top_iff {a : ENNReal} {n : ℕ} :

a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

theorem ENNReal.pow_eq_top {a : ENNReal} (n : ℕ) (h : a ^ n = ⊤) :

theorem ENNReal.pow_ne_top {a : ENNReal} (h : a ≠ ⊤) {n : ℕ} :

theorem ENNReal.pow_lt_top {a : ENNReal} :

a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤

@[simp]

theorem ENNReal.coe_finset_sum {α : Type u_1} {s : Finset α} {f : α → NNReal} :

↑(Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => ↑(f a)

@[simp]

theorem ENNReal.coe_finset_prod {α : Type u_1} {s : Finset α} {f : α → NNReal} :

↑(Finset.prod s fun (a : α) => f a) = Finset.prod s fun (a : α) => ↑(f a)

theorem ENNReal.bot_eq_zero :

theorem ENNReal.not_top_le_coe {r : NNReal} :

@[simp]

theorem ENNReal.one_le_coe_iff {r : NNReal} :

1 ≤ ↑r ↔ 1 ≤ r

@[simp]

theorem ENNReal.coe_le_one_iff {r : NNReal} :

↑r ≤ 1 ↔ r ≤ 1

@[simp]

theorem ENNReal.coe_lt_one_iff {p : NNReal} :

↑p < 1 ↔ p < 1

@[simp]

theorem ENNReal.one_lt_coe_iff {p : NNReal} :

1 < ↑p ↔ 1 < p

@[simp]

theorem ENNReal.coe_nat (n : ℕ) :

↑↑n = ↑n

@[simp]

theorem ENNReal.ofReal_coe_nat (n : ℕ) :

ENNReal.ofReal ↑n = ↑n

@[simp]

theorem ENNReal.ofReal_ofNat (n : ℕ) [Nat.AtLeastTwo n] :

ENNReal.ofReal (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem ENNReal.nat_ne_top (n : ℕ) :

↑n ≠ ⊤

@[simp]

theorem ENNReal.top_ne_nat (n : ℕ) :

⊤ ≠ ↑n

@[simp]

theorem ENNReal.one_lt_top :

@[simp]

theorem ENNReal.toNNReal_nat (n : ℕ) :

ENNReal.toNNReal ↑n = ↑n

@[simp]

theorem ENNReal.toReal_nat (n : ℕ) :

ENNReal.toReal ↑n = ↑n

@[simp]

theorem ENNReal.toReal_ofNat (n : ℕ) [Nat.AtLeastTwo n] :

ENNReal.toReal (OfNat.ofNat n) = OfNat.ofNat n

theorem ENNReal.le_coe_iff {a : ENNReal} {r : NNReal} :

a ≤ ↑r ↔ ∃ (p : NNReal), a = ↑p ∧ p ≤ r

theorem ENNReal.coe_le_iff {a : ENNReal} {r : NNReal} :

↑r ≤ a ↔ ∀ (p : NNReal), a = ↑p → r ≤ p

theorem ENNReal.lt_iff_exists_coe {a : ENNReal} {b : ENNReal} :

a < b ↔ ∃ (p : NNReal), a = ↑p ∧ ↑p < b

theorem ENNReal.toReal_le_coe_of_le_coe {a : ENNReal} {b : NNReal} (h : a ≤ ↑b) :

ENNReal.toReal a ≤ ↑b

@[simp]

theorem ENNReal.coe_finset_sup {α : Type u_1} {s : Finset α} {f : α → NNReal} :

↑(Finset.sup s f) = Finset.sup s fun (x : α) => ↑(f x)

@[simp]

theorem ENNReal.max_eq_zero_iff {a : ENNReal} {b : ENNReal} :

max a b = 0 ↔ a = 0 ∧ b = 0

theorem ENNReal.max_zero_left {a : ENNReal} :

max 0 a = a

theorem ENNReal.max_zero_right {a : ENNReal} :

max a 0 = a

@[simp]

theorem ENNReal.sup_eq_max {a : ENNReal} {b : ENNReal} :

a ⊔ b = max a b

theorem ENNReal.pow_pos {a : ENNReal} :

0 < a → ∀ (n : ℕ), 0 < a ^ n

theorem ENNReal.pow_ne_zero {a : ENNReal} :

a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0

theorem ENNReal.not_lt_zero {a : ENNReal} :

¬a < 0

theorem ENNReal.le_of_add_le_add_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → a + b ≤ a + c → b ≤ c

theorem ENNReal.le_of_add_le_add_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → b + a ≤ c + a → b ≤ c

theorem ENNReal.add_lt_add_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → b < c → a + b < a + c

theorem ENNReal.add_lt_add_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → b < c → b + a < c + a

theorem ENNReal.add_le_add_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → (a + b ≤ a + c ↔ b ≤ c)

theorem ENNReal.add_le_add_iff_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → (b + a ≤ c + a ↔ b ≤ c)

theorem ENNReal.add_lt_add_iff_left {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → (a + b < a + c ↔ b < c)

theorem ENNReal.add_lt_add_iff_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a ≠ ⊤ → (b + a < c + a ↔ b < c)

theorem ENNReal.add_lt_add_of_le_of_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} :

a ≠ ⊤ → a ≤ b → c < d → a + c < b + d

theorem ENNReal.add_lt_add_of_lt_of_le {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} :

c ≠ ⊤ → a < b → c ≤ d → a + c < b + d

instance ENNReal.contravariantClass_add_lt :

ContravariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x < x_1

Equations

ENNReal.contravariantClass_add_lt = (_ : ContravariantClass (WithTop NNReal) (WithTop NNReal) (fun (x x_1 : WithTop NNReal) => x + x_1) fun (x x_1 : WithTop NNReal) => x < x_1)

theorem ENNReal.lt_add_right {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) :

a < a + b

theorem ENNReal.lt_iff_exists_rat_btwn {a : ENNReal} {b : ENNReal} :

a < b ↔ ∃ (q : ℚ), 0 ≤ q ∧ a < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b

theorem ENNReal.lt_iff_exists_real_btwn {a : ENNReal} {b : ENNReal} :

a < b ↔ ∃ (r : ℝ), 0 ≤ r ∧ a < ENNReal.ofReal r ∧ ENNReal.ofReal r < b

theorem ENNReal.lt_iff_exists_nnreal_btwn {a : ENNReal} {b : ENNReal} :

a < b ↔ ∃ (r : NNReal), a < ↑r ∧ ↑r < b

theorem ENNReal.lt_iff_exists_add_pos_lt {a : ENNReal} {b : ENNReal} :

a < b ↔ ∃ (r : NNReal), 0 < r ∧ a + ↑r < b

theorem ENNReal.le_of_forall_pos_le_add {a : ENNReal} {b : ENNReal} (h : ∀ (ε : NNReal), 0 < ε → b < ⊤ → a ≤ b + ↑ε) :

a ≤ b

theorem ENNReal.coe_nat_lt_coe {r : NNReal} {n : ℕ} :

↑n < ↑r ↔ ↑n < r

theorem ENNReal.coe_lt_coe_nat {r : NNReal} {n : ℕ} :

↑r < ↑n ↔ r < ↑n

theorem ENNReal.exists_nat_gt {r : ENNReal} (h : r ≠ ⊤) :

∃ (n : ℕ), r < ↑n

@[simp]

theorem ENNReal.iUnion_Iio_coe_nat :

⋃ (n : ℕ), Set.Iio ↑n = {⊤}ᶜ

@[simp]

theorem ENNReal.iUnion_Iic_coe_nat :

⋃ (n : ℕ), Set.Iic ↑n = {⊤}ᶜ

@[simp]

theorem ENNReal.iUnion_Ioc_coe_nat {a : ENNReal} :

⋃ (n : ℕ), Set.Ioc a ↑n = Set.Ioi a \ {⊤}

@[simp]

theorem ENNReal.iUnion_Ioo_coe_nat {a : ENNReal} :

⋃ (n : ℕ), Set.Ioo a ↑n = Set.Ioi a \ {⊤}

@[simp]

theorem ENNReal.iUnion_Icc_coe_nat {a : ENNReal} :

⋃ (n : ℕ), Set.Icc a ↑n = Set.Ici a \ {⊤}

@[simp]

theorem ENNReal.iUnion_Ico_coe_nat {a : ENNReal} :

⋃ (n : ℕ), Set.Ico a ↑n = Set.Ici a \ {⊤}

@[simp]

theorem ENNReal.iInter_Ici_coe_nat :

⋂ (n : ℕ), Set.Ici ↑n = {⊤}

@[simp]

theorem ENNReal.iInter_Ioi_coe_nat :

⋂ (n : ℕ), Set.Ioi ↑n = {⊤}

theorem ENNReal.add_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :

a + b < c + d

@[simp]

theorem ENNReal.coe_min (r : NNReal) (p : NNReal) :

↑(min r p) = min ↑r ↑p

@[simp]

theorem ENNReal.coe_max (r : NNReal) (p : NNReal) :

↑(max r p) = max ↑r ↑p

theorem ENNReal.le_of_top_imp_top_of_toNNReal_le {a : ENNReal} {b : ENNReal} (h : a = ⊤ → b = ⊤) (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal b) :

a ≤ b

@[simp]

theorem ENNReal.abs_toReal {x : ENNReal} :

|ENNReal.toReal x| = ENNReal.toReal x

theorem ENNReal.coe_sSup {s : Set NNReal} :

BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a

theorem ENNReal.coe_sInf {s : Set NNReal} :

Set.Nonempty s → ↑(sInf s) = ⨅ a ∈ s, ↑a

theorem ENNReal.coe_iSup {ι : Sort u_4} {f : ι → NNReal} (hf : BddAbove (Set.range f)) :

↑(iSup f) = ⨆ (a : ι), ↑(f a)

theorem ENNReal.coe_iInf {ι : Sort u_4} [Nonempty ι] (f : ι → NNReal) :

↑(iInf f) = ⨅ (a : ι), ↑(f a)

theorem ENNReal.coe_mem_upperBounds {r : NNReal} {s : Set NNReal} :

↑r ∈ upperBounds (ENNReal.ofNNReal '' s) ↔ r ∈ upperBounds s

theorem ENNReal.iSup_coe_eq_top {ι : Sort u_3} {f : ι → NNReal} :

⨆ (i : ι), ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)

theorem ENNReal.iSup_coe_lt_top {ι : Sort u_3} {f : ι → NNReal} :

⨆ (i : ι), ↑(f i) < ⊤ ↔ BddAbove (Set.range f)

theorem ENNReal.iInf_coe_eq_top {ι : Sort u_3} {f : ι → NNReal} :

⨅ (i : ι), ↑(f i) = ⊤ ↔ IsEmpty ι

theorem ENNReal.iInf_coe_lt_top {ι : Sort u_3} {f : ι → NNReal} :

⨅ (i : ι), ↑(f i) < ⊤ ↔ Nonempty ι

theorem ENNReal.mul_lt_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ac : a < c) (bd : b < d) :

a * b < c * d

theorem ENNReal.mul_left_mono {a : ENNReal} :

Monotone fun (x : ENNReal) => a * x

theorem ENNReal.mul_right_mono {a : ENNReal} :

Monotone fun (x : ENNReal) => x * a

theorem ENNReal.pow_strictMono {n : ℕ} :

n ≠ 0 → StrictMono fun (x : ENNReal) => x ^ n

theorem ENNReal.pow_lt_pow_of_lt_left {a : ENNReal} {b : ENNReal} (h : a < b) {n : ℕ} (hn : n ≠ 0) :

a ^ n < b ^ n

theorem ENNReal.max_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} :

max a b * c = max (a * c) (b * c)

theorem ENNReal.mul_max {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a * max b c = max (a * b) (a * c)

theorem ENNReal.mul_left_strictMono {a : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

StrictMono fun (x : ENNReal) => a * x

theorem ENNReal.mul_lt_mul_left' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) :

a * b < a * c

theorem ENNReal.mul_lt_mul_right' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) :

b * a < c * a

theorem ENNReal.mul_eq_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

a * b = a * c ↔ b = c

theorem ENNReal.mul_eq_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

c ≠ 0 → c ≠ ⊤ → (a * c = b * c ↔ a = b)

theorem ENNReal.mul_le_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

a * b ≤ a * c ↔ b ≤ c

theorem ENNReal.mul_le_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

c ≠ 0 → c ≠ ⊤ → (a * c ≤ b * c ↔ a ≤ b)

theorem ENNReal.mul_lt_mul_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : a ≠ 0) (hinf : a ≠ ⊤) :

a * b < a * c ↔ b < c

theorem ENNReal.mul_lt_mul_right {a : ENNReal} {b : ENNReal} {c : ENNReal} :

c ≠ 0 → c ≠ ⊤ → (a * c < b * c ↔ a < b)

theorem ENNReal.addLECancellable_iff_ne {a : ENNReal} :

AddLECancellable a ↔ a ≠ ⊤

An element a is AddLECancellable if a + b ≤ a + c implies b ≤ c for all b and c. This is true in ℝ≥0∞ for all elements except ∞.

theorem ENNReal.cancel_of_ne {a : ENNReal} (h : a ≠ ⊤) :

AddLECancellable a

This lemma has an abbreviated name because it is used frequently.

theorem ENNReal.cancel_of_lt {a : ENNReal} (h : a < ⊤) :

AddLECancellable a

This lemma has an abbreviated name because it is used frequently.

theorem ENNReal.cancel_of_lt' {a : ENNReal} {b : ENNReal} (h : a < b) :

AddLECancellable a

This lemma has an abbreviated name because it is used frequently.

theorem ENNReal.cancel_coe {a : NNReal} :

AddLECancellable ↑a

This lemma has an abbreviated name because it is used frequently.

theorem ENNReal.add_right_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤) :

a + b = a + c ↔ b = c

theorem ENNReal.add_left_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤) :

b + a = c + a ↔ b = c

theorem ENNReal.sub_eq_sInf {a : ENNReal} {b : ENNReal} :

a - b = sInf {d : ENNReal | a ≤ d + b}

@[simp]

theorem ENNReal.coe_sub {r : NNReal} {p : NNReal} :

↑(r - p) = ↑r - ↑p

This is a special case of WithTop.coe_sub in the ENNReal namespace

@[simp]

theorem ENNReal.top_sub_coe {r : NNReal} :

⊤ - ↑r = ⊤

This is a special case of WithTop.top_sub_coe in the ENNReal namespace

theorem ENNReal.sub_top {a : ENNReal} :

a - ⊤ = 0

This is a special case of WithTop.sub_top in the ENNReal namespace

@[simp]

theorem ENNReal.sub_eq_top_iff {a : ENNReal} {b : ENNReal} :

a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem ENNReal.sub_ne_top {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) :

@[simp]

theorem ENNReal.nat_cast_sub (m : ℕ) (n : ℕ) :

↑(m - n) = ↑m - ↑n

theorem ENNReal.sub_eq_of_eq_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) :

a = c + b → a - b = c

theorem ENNReal.eq_sub_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hc : c ≠ ⊤) :

a + c = b → a = b - c

theorem ENNReal.sub_eq_of_eq_add_rev {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) :

a = b + c → a - b = c

theorem ENNReal.sub_eq_of_add_eq {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) (hc : a + b = c) :

c - b = a

@[simp]

theorem ENNReal.add_sub_cancel_left {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) :

a + b - a = b

@[simp]

theorem ENNReal.add_sub_cancel_right {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) :

a + b - b = a

theorem ENNReal.lt_add_of_sub_lt_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤ ∨ b ≠ ⊤) :

a - b < c → a < b + c

theorem ENNReal.lt_add_of_sub_lt_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≠ ⊤ ∨ c ≠ ⊤) :

a - c < b → a < b + c

theorem ENNReal.le_sub_of_add_le_left {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ≠ ⊤) :

a + b ≤ c → b ≤ c - a

theorem ENNReal.le_sub_of_add_le_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) :

a + b ≤ c → a ≤ c - b

theorem ENNReal.sub_lt_of_lt_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hac : c ≤ a) (h : a < b + c) :

a - c < b

theorem ENNReal.sub_lt_iff_lt_right {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb : b ≠ ⊤) (hab : b ≤ a) :

a - b < c ↔ a < c + b

theorem ENNReal.sub_lt_self {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (ha₀ : a ≠ 0) (hb : b ≠ 0) :

a - b < a

theorem ENNReal.sub_lt_self_iff {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) :

a - b < a ↔ 0 < a ∧ 0 < b

theorem ENNReal.sub_lt_of_sub_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} (h₂ : c ≤ a) (h₃ : a ≠ ⊤ ∨ b ≠ ⊤) (h₁ : a - b < c) :

a - c < b

theorem ENNReal.sub_sub_cancel {a : ENNReal} {b : ENNReal} (h : a ≠ ⊤) (h2 : b ≤ a) :

a - (a - b) = b

theorem ENNReal.sub_right_inj {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ≠ ⊤) (hb : b ≤ a) (hc : c ≤ a) :

a - b = a - c ↔ b = c

theorem ENNReal.sub_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < b → b < a → c ≠ ⊤) :

(a - b) * c = a * c - b * c

theorem ENNReal.mul_sub {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < c → c < b → a ≠ ⊤) :

a * (b - c) = a * b - a * c

theorem ENNReal.prod_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a ≠ ⊤) :

(Finset.prod s fun (a : α) => f a) < ⊤

A product of finite numbers is still finite

theorem ENNReal.sum_lt_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : ∀ a ∈ s, f a ≠ ⊤) :

(Finset.sum s fun (a : α) => f a) < ⊤

A sum of finite numbers is still finite

theorem ENNReal.sum_lt_top_iff {α : Type u_1} {s : Finset α} {f : α → ENNReal} :

(Finset.sum s fun (a : α) => f a) < ⊤ ↔ ∀ a ∈ s, f a < ⊤

A sum of finite numbers is still finite

theorem ENNReal.sum_eq_top_iff {α : Type u_1} {s : Finset α} {f : α → ENNReal} :

(Finset.sum s fun (x : α) => f x) = ⊤ ↔ ∃ a ∈ s, f a = ⊤

A sum of numbers is infinite iff one of them is infinite

theorem ENNReal.lt_top_of_sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ENNReal} (h : (Finset.sum s fun (x : α) => f x) ≠ ⊤) {a : α} (ha : a ∈ s) :

f a < ⊤

theorem ENNReal.toNNReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) :

ENNReal.toNNReal (Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => ENNReal.toNNReal (f a)

Seeing ℝ≥0∞ as ℝ≥0 does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ENNReal.toReal_sum {α : Type u_1} {s : Finset α} {f : α → ENNReal} (hf : ∀ a ∈ s, f a ≠ ⊤) :

ENNReal.toReal (Finset.sum s fun (a : α) => f a) = Finset.sum s fun (a : α) => ENNReal.toReal (f a)

seeing ℝ≥0∞ as Real does not change their sum, unless one of the ℝ≥0∞ is infinity

theorem ENNReal.ofReal_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :

ENNReal.ofReal (Finset.sum s fun (i : α) => f i) = Finset.sum s fun (i : α) => ENNReal.ofReal (f i)

theorem ENNReal.sum_lt_sum_of_nonempty {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) {f : α → ENNReal} {g : α → ENNReal} (Hlt : ∀ i ∈ s, f i < g i) :

(Finset.sum s fun (i : α) => f i) < Finset.sum s fun (i : α) => g i

theorem ENNReal.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : Finset.Nonempty s) {f : α → ENNReal} {g : α → ENNReal} (Hle : (Finset.sum s fun (i : α) => f i) ≤ Finset.sum s fun (i : α) => g i) :

∃ i ∈ s, f i ≤ g i

theorem ENNReal.Ico_eq_Iio {y : ENNReal} :

Set.Ico 0 y = Set.Iio y

theorem ENNReal.mem_Iio_self_add {x : ENNReal} {ε : ENNReal} :

x ≠ ⊤ → ε ≠ 0 → x ∈ Set.Iio (x + ε)

theorem ENNReal.mem_Ioo_self_sub_add {x : ENNReal} {ε₁ : ENNReal} {ε₂ : ENNReal} :

x ≠ ⊤ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Set.Ioo (x - ε₁) (x + ε₂)

instance ENNReal.instInvENNReal :

Equations

ENNReal.instInvENNReal = { inv := fun (a : ENNReal) => sInf {b : ENNReal | 1 ≤ a * b} }

instance ENNReal.instDivInvMonoidENNReal :

DivInvMonoid ENNReal

Equations

ENNReal.instDivInvMonoidENNReal = DivInvMonoid.mk zpowRec

theorem ENNReal.div_eq_inv_mul {a : ENNReal} {b : ENNReal} :

a / b = b⁻¹ * a

@[simp]

theorem ENNReal.inv_zero :

@[simp]

theorem ENNReal.inv_top :

theorem ENNReal.coe_inv_le {r : NNReal} :

↑r⁻¹ ≤ (↑r)⁻¹

@[simp]

theorem ENNReal.coe_inv {r : NNReal} (hr : r ≠ 0) :

↑r⁻¹ = (↑r)⁻¹

theorem ENNReal.coe_inv_two :

↑2⁻¹ = 2⁻¹

@[simp]

theorem ENNReal.coe_div {r : NNReal} {p : NNReal} (hr : r ≠ 0) :

↑(p / r) = ↑p / ↑r

theorem ENNReal.div_zero {a : ENNReal} (h : a ≠ 0) :

a / 0 = ⊤

instance ENNReal.instDivInvOneMonoidENNReal :

DivInvOneMonoid ENNReal

Equations

ENNReal.instDivInvOneMonoidENNReal = let src := inferInstanceAs (DivInvMonoid ENNReal); DivInvOneMonoid.mk ENNReal.instDivInvOneMonoidENNReal.proof_1

theorem ENNReal.inv_pow {a : ENNReal} {n : ℕ} :

(a ^ n)⁻¹ = a⁻¹ ^ n

theorem ENNReal.mul_inv_cancel {a : ENNReal} (h0 : a ≠ 0) (ht : a ≠ ⊤) :

a * a⁻¹ = 1

theorem ENNReal.inv_mul_cancel {a : ENNReal} (h0 : a ≠ 0) (ht : a ≠ ⊤) :

a⁻¹ * a = 1

theorem ENNReal.div_mul_cancel {a : ENNReal} {b : ENNReal} (h0 : a ≠ 0) (hI : a ≠ ⊤) :

b / a * a = b

theorem ENNReal.mul_div_cancel' {a : ENNReal} {b : ENNReal} (h0 : a ≠ 0) (hI : a ≠ ⊤) :

a * (b / a) = b

theorem ENNReal.mul_comm_div {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a / b * c = a * (c / b)

theorem ENNReal.mul_div_right_comm {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a * b / c = a / c * b

instance ENNReal.instInvolutiveInvENNReal :

InvolutiveInv ENNReal

Equations

ENNReal.instInvolutiveInvENNReal = InvolutiveInv.mk ENNReal.instInvolutiveInvENNReal.proof_1

@[simp]

theorem ENNReal.inv_eq_top {a : ENNReal} :

a⁻¹ = ⊤ ↔ a = 0

theorem ENNReal.inv_ne_top {a : ENNReal} :

a⁻¹ ≠ ⊤ ↔ a ≠ 0

@[simp]

theorem ENNReal.inv_lt_top {x : ENNReal} :

x⁻¹ < ⊤ ↔ 0 < x

theorem ENNReal.div_lt_top {x : ENNReal} {y : ENNReal} (h1 : x ≠ ⊤) (h2 : y ≠ 0) :

x / y < ⊤

@[simp]

theorem ENNReal.inv_eq_zero {a : ENNReal} :

a⁻¹ = 0 ↔ a = ⊤

theorem ENNReal.inv_ne_zero {a : ENNReal} :

a⁻¹ ≠ 0 ↔ a ≠ ⊤

theorem ENNReal.div_pos {a : ENNReal} {b : ENNReal} (ha : a ≠ 0) (hb : b ≠ ⊤) :

0 < a / b

theorem ENNReal.mul_inv {a : ENNReal} {b : ENNReal} (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : a ≠ ⊤ ∨ b ≠ 0) :

(a * b)⁻¹ = a⁻¹ * b⁻¹

theorem ENNReal.mul_div_mul_left {c : ENNReal} (a : ENNReal) (b : ENNReal) (hc : c ≠ 0) (hc' : c ≠ ⊤) :

c * a / (c * b) = a / b

theorem ENNReal.mul_div_mul_right {c : ENNReal} (a : ENNReal) (b : ENNReal) (hc : c ≠ 0) (hc' : c ≠ ⊤) :

a * c / (b * c) = a / b

theorem ENNReal.sub_div {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : 0 < b → b < a → c ≠ 0) :

(a - b) / c = a / c - b / c

@[simp]

theorem ENNReal.inv_pos {a : ENNReal} :

0 < a⁻¹ ↔ a ≠ ⊤

theorem ENNReal.inv_strictAnti :

StrictAnti Inv.inv

@[simp]

theorem ENNReal.inv_lt_inv {a : ENNReal} {b : ENNReal} :

a⁻¹ < b⁻¹ ↔ b < a

theorem ENNReal.inv_lt_iff_inv_lt {a : ENNReal} {b : ENNReal} :

a⁻¹ < b ↔ b⁻¹ < a

theorem ENNReal.lt_inv_iff_lt_inv {a : ENNReal} {b : ENNReal} :

a < b⁻¹ ↔ b < a⁻¹

@[simp]

theorem ENNReal.inv_le_inv {a : ENNReal} {b : ENNReal} :

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem ENNReal.inv_le_iff_inv_le {a : ENNReal} {b : ENNReal} :

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

theorem ENNReal.le_inv_iff_le_inv {a : ENNReal} {b : ENNReal} :

a ≤ b⁻¹ ↔ b ≤ a⁻¹

theorem ENNReal.inv_le_inv' {a : ENNReal} {b : ENNReal} (h : a ≤ b) :

b⁻¹ ≤ a⁻¹

theorem ENNReal.inv_lt_inv' {a : ENNReal} {b : ENNReal} (h : a < b) :

b⁻¹ < a⁻¹

@[simp]

theorem ENNReal.inv_le_one {a : ENNReal} :

a⁻¹ ≤ 1 ↔ 1 ≤ a

theorem ENNReal.one_le_inv {a : ENNReal} :

1 ≤ a⁻¹ ↔ a ≤ 1

@[simp]

theorem ENNReal.inv_lt_one {a : ENNReal} :

a⁻¹ < 1 ↔ 1 < a

@[simp]

theorem ENNReal.one_lt_inv {a : ENNReal} :

1 < a⁻¹ ↔ a < 1

@[simp]

theorem OrderIso.invENNReal_apply :

∀ (a : ENNReal), OrderIso.invENNReal a = (OrderDual.toDual a)⁻¹

def OrderIso.invENNReal :

ENNReal ≃o ENNReal ᵒᵈ

The inverse map fun x ↦ x⁻¹ is an order isomorphism between ℝ≥0∞ and its OrderDual

Equations

OrderIso.invENNReal = { toEquiv := (Equiv.inv ENNReal).trans OrderDual.toDual, map_rel_iff' := (_ : ∀ {a b : ENNReal}, b⁻¹ ≤ a⁻¹ ↔ a ≤ b) }

Instances For

@[simp]

theorem OrderIso.invENNReal_symm_apply (a : ENNReal ᵒᵈ) :

(OrderIso.symm OrderIso.invENNReal) a = (OrderDual.ofDual a)⁻¹

@[simp]

theorem ENNReal.div_top {a : ENNReal} :

a / ⊤ = 0

theorem ENNReal.top_div {a : ENNReal} :

⊤ / a = if a = ⊤ then 0 else ⊤

theorem ENNReal.top_div_of_ne_top {a : ENNReal} (h : a ≠ ⊤) :

@[simp]

theorem ENNReal.top_div_coe {p : NNReal} :

⊤ / ↑p = ⊤

theorem ENNReal.top_div_of_lt_top {a : ENNReal} (h : a < ⊤) :

@[simp]

theorem ENNReal.zero_div {a : ENNReal} :

0 / a = 0

theorem ENNReal.div_eq_top {a : ENNReal} {b : ENNReal} :

a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤

theorem ENNReal.le_div_iff_mul_le {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ⊤ ∨ c ≠ ⊤) :

a ≤ c / b ↔ a * b ≤ c

theorem ENNReal.div_le_iff_le_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb0 : b ≠ 0 ∨ c ≠ ⊤) (hbt : b ≠ ⊤ ∨ c ≠ 0) :

a / b ≤ c ↔ a ≤ c * b

theorem ENNReal.lt_div_iff_mul_lt {a : ENNReal} {b : ENNReal} {c : ENNReal} (hb0 : b ≠ 0 ∨ c ≠ ⊤) (hbt : b ≠ ⊤ ∨ c ≠ 0) :

c < a / b ↔ c * b < a

theorem ENNReal.div_le_of_le_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≤ b * c) :

a / c ≤ b

theorem ENNReal.div_le_of_le_mul' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≤ b * c) :

a / b ≤ c

theorem ENNReal.div_self_le_one {a : ENNReal} :

a / a ≤ 1

theorem ENNReal.mul_le_of_le_div {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≤ b / c) :

a * c ≤ b

theorem ENNReal.mul_le_of_le_div' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a ≤ b / c) :

c * a ≤ b

theorem ENNReal.div_lt_iff {a : ENNReal} {b : ENNReal} {c : ENNReal} (h0 : b ≠ 0 ∨ c ≠ 0) (ht : b ≠ ⊤ ∨ c ≠ ⊤) :

c / b < a ↔ c < a * b

theorem ENNReal.mul_lt_of_lt_div {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b / c) :

a * c < b

theorem ENNReal.mul_lt_of_lt_div' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b / c) :

c * a < b

theorem ENNReal.div_lt_of_lt_mul {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b * c) :

a / c < b

theorem ENNReal.div_lt_of_lt_mul' {a : ENNReal} {b : ENNReal} {c : ENNReal} (h : a < b * c) :

a / b < c

theorem ENNReal.inv_le_iff_le_mul {a : ENNReal} {b : ENNReal} (h₁ : b = ⊤ → a ≠ 0) (h₂ : a = ⊤ → b ≠ 0) :

a⁻¹ ≤ b ↔ 1 ≤ a * b

@[simp]

theorem ENNReal.le_inv_iff_mul_le {a : ENNReal} {b : ENNReal} :

a ≤ b⁻¹ ↔ a * b ≤ 1

theorem ENNReal.div_le_div {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (hab : a ≤ b) (hdc : d ≤ c) :

a / c ≤ b / d

theorem ENNReal.div_le_div_left {a : ENNReal} {b : ENNReal} (h : a ≤ b) (c : ENNReal) :

c / b ≤ c / a

theorem ENNReal.div_le_div_right {a : ENNReal} {b : ENNReal} (h : a ≤ b) (c : ENNReal) :

a / c ≤ b / c

theorem ENNReal.eq_inv_of_mul_eq_one_left {a : ENNReal} {b : ENNReal} (h : a * b = 1) :

theorem ENNReal.mul_le_iff_le_inv {a : ENNReal} {b : ENNReal} {r : ENNReal} (hr₀ : r ≠ 0) (hr₁ : r ≠ ⊤) :

r * a ≤ b ↔ a ≤ r⁻¹ * b

theorem ENNReal.le_inv_smul_iff {a : ENNReal} {b : ENNReal} {r : NNReal} (hr₀ : r ≠ 0) :

a ≤ r⁻¹ • b ↔ r • a ≤ b

A variant of le_inv_smul_iff that holds for ENNReal.

theorem ENNReal.inv_smul_le_iff {a : ENNReal} {b : ENNReal} {r : NNReal} (hr₀ : r ≠ 0) :

r⁻¹ • a ≤ b ↔ a ≤ r • b

A variant of inv_smul_le_iff that holds for ENNReal.

theorem ENNReal.le_of_forall_nnreal_lt {x : ENNReal} {y : ENNReal} (h : ∀ (r : NNReal), ↑r < x → ↑r ≤ y) :

x ≤ y

theorem ENNReal.le_of_forall_pos_nnreal_lt {x : ENNReal} {y : ENNReal} (h : ∀ (r : NNReal), 0 < r → ↑r < x → ↑r ≤ y) :

x ≤ y

theorem ENNReal.eq_top_of_forall_nnreal_le {x : ENNReal} (h : ∀ (r : NNReal), ↑r ≤ x) :

theorem ENNReal.add_div {a : ENNReal} {b : ENNReal} {c : ENNReal} :

(a + b) / c = a / c + b / c

theorem ENNReal.div_add_div_same {a : ENNReal} {b : ENNReal} {c : ENNReal} :

a / c + b / c = (a + b) / c

theorem ENNReal.div_self {a : ENNReal} (h0 : a ≠ 0) (hI : a ≠ ⊤) :

a / a = 1

theorem ENNReal.mul_div_le {a : ENNReal} {b : ENNReal} :

a * (b / a) ≤ b

theorem ENNReal.eq_div_iff {a : ENNReal} {b : ENNReal} {c : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) :

b = c / a ↔ a * b = c

theorem ENNReal.div_eq_div_iff {a : ENNReal} {b : ENNReal} {c : ENNReal} {d : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) (hb : b ≠ 0) (hb' : b ≠ ⊤) :

c / b = d / a ↔ a * c = b * d

theorem ENNReal.div_eq_one_iff {a : ENNReal} {b : ENNReal} (hb₀ : b ≠ 0) (hb₁ : b ≠ ⊤) :

a / b = 1 ↔ a = b

theorem ENNReal.inv_two_add_inv_two :

2⁻¹ + 2⁻¹ = 1

theorem ENNReal.inv_three_add_inv_three :

3⁻¹ + 3⁻¹ + 3⁻¹ = 1

@[simp]

theorem ENNReal.add_halves (a : ENNReal) :

a / 2 + a / 2 = a

@[simp]

theorem ENNReal.add_thirds (a : ENNReal) :

a / 3 + a / 3 + a / 3 = a

@[simp]

theorem ENNReal.div_eq_zero_iff {a : ENNReal} {b : ENNReal} :

a / b = 0 ↔ a = 0 ∨ b = ⊤

@[simp]

theorem ENNReal.div_pos_iff {a : ENNReal} {b : ENNReal} :

0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤

theorem ENNReal.half_pos {a : ENNReal} (h : a ≠ 0) :

0 < a / 2

theorem ENNReal.one_half_lt_one :

theorem ENNReal.half_lt_self {a : ENNReal} (hz : a ≠ 0) (ht : a ≠ ⊤) :

a / 2 < a

theorem ENNReal.half_le_self {a : ENNReal} :

a / 2 ≤ a

theorem ENNReal.sub_half {a : ENNReal} (h : a ≠ ⊤) :

a - a / 2 = a / 2

@[simp]

theorem ENNReal.one_sub_inv_two :

1 - 2⁻¹ = 2⁻¹

@[simp]

theorem ENNReal.orderIsoIicOneBirational_apply_coe (x : ENNReal) :

↑(ENNReal.orderIsoIicOneBirational x) = (x⁻¹ + 1)⁻¹

def ENNReal.orderIsoIicOneBirational :

ENNReal ≃o ↑(Set.Iic 1)

The birational order isomorphism between ℝ≥0∞ and the unit interval Set.Iic (1 : ℝ≥0∞).

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ENNReal.orderIsoIicOneBirational_symm_apply (x : ↑(Set.Iic 1)) :

(OrderIso.symm ENNReal.orderIsoIicOneBirational) x = ((↑x)⁻¹ - 1)⁻¹

@[simp]

theorem ENNReal.orderIsoIicCoe_apply_coe (a : NNReal) :

∀ (a_1 : ↑(Set.Iic ↑a)), ↑((ENNReal.orderIsoIicCoe a) a_1) = ENNReal.toNNReal ↑a_1

def ENNReal.orderIsoIicCoe (a : NNReal) :

↑(Set.Iic ↑a) ≃o ↑(Set.Iic a)

Order isomorphism between an initial interval in ℝ≥0∞ and an initial interval in ℝ≥0.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ENNReal.orderIsoIicCoe_symm_apply_coe (a : NNReal) (b : ↑(Set.Iic a)) :

↑((OrderIso.symm (ENNReal.orderIsoIicCoe a)) b) = ↑↑b

def ENNReal.orderIsoUnitIntervalBirational :

ENNReal ≃o ↑(Set.Icc 0 1)

An order isomorphism between the extended nonnegative real numbers and the unit interval.

Equations

ENNReal.orderIsoUnitIntervalBirational = OrderIso.trans ENNReal.orderIsoIicOneBirational (OrderIso.trans (ENNReal.orderIsoIicCoe 1) (OrderIso.symm (NNReal.orderIsoIccZeroCoe 1)))

Instances For

@[simp]

theorem ENNReal.orderIsoUnitIntervalBirational_apply_coe (x : ENNReal) :

↑(ENNReal.orderIsoUnitIntervalBirational x) = ENNReal.toReal (x⁻¹ + 1)⁻¹

theorem ENNReal.exists_inv_nat_lt {a : ENNReal} (h : a ≠ 0) :

∃ (n : ℕ), (↑n)⁻¹ < a

theorem ENNReal.exists_nat_pos_mul_gt {a : ENNReal} {b : ENNReal} (ha : a ≠ 0) (hb : b ≠ ⊤) :

∃ n > 0, b < ↑n * a

theorem ENNReal.exists_nat_mul_gt {a : ENNReal} {b : ENNReal} (ha : a ≠ 0) (hb : b ≠ ⊤) :

∃ (n : ℕ), b < ↑n * a

theorem ENNReal.exists_nat_pos_inv_mul_lt {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) :

∃ n > 0, (↑n)⁻¹ * a < b

theorem ENNReal.exists_nnreal_pos_mul_lt {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ 0) :

∃ n > 0, ↑n * a < b

theorem ENNReal.exists_inv_two_pow_lt {a : ENNReal} (ha : a ≠ 0) :

∃ (n : ℕ), 2⁻¹ ^ n < a

@[simp]

theorem ENNReal.coe_zpow {r : NNReal} (hr : r ≠ 0) (n : ℤ) :

↑(r ^ n) = ↑r ^ n

theorem ENNReal.zpow_pos {a : ENNReal} (ha : a ≠ 0) (h'a : a ≠ ⊤) (n : ℤ) :

0 < a ^ n

theorem ENNReal.zpow_lt_top {a : ENNReal} (ha : a ≠ 0) (h'a : a ≠ ⊤) (n : ℤ) :

a ^ n < ⊤

theorem ENNReal.exists_mem_Ico_zpow {x : ENNReal} {y : ENNReal} (hx : x ≠ 0) (h'x : x ≠ ⊤) (hy : 1 < y) (h'y : y ≠ ⊤) :

∃ (n : ℤ), x ∈ Set.Ico (y ^ n) (y ^ (n + 1))

theorem ENNReal.exists_mem_Ioc_zpow {x : ENNReal} {y : ENNReal} (hx : x ≠ 0) (h'x : x ≠ ⊤) (hy : 1 < y) (h'y : y ≠ ⊤) :

∃ (n : ℤ), x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))

theorem ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow {y : ENNReal} (hy : 1 < y) (h'y : y ≠ ⊤) :

Set.Ioo 0 ⊤ = ⋃ (n : ℤ), Set.Ico (y ^ n) (y ^ (n + 1))

theorem ENNReal.zpow_le_of_le {x : ENNReal} (hx : 1 ≤ x) {a : ℤ} {b : ℤ} (h : a ≤ b) :

x ^ a ≤ x ^ b

theorem ENNReal.monotone_zpow {x : ENNReal} (hx : 1 ≤ x) :

Monotone fun (x_1 : ℤ) => x ^ x_1

theorem ENNReal.zpow_add {x : ENNReal} (hx : x ≠ 0) (h'x : x ≠ ⊤) (m : ℤ) (n : ℤ) :

x ^ (m + n) = x ^ m * x ^ n

theorem ENNReal.toReal_add {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal (a + b) = ENNReal.toReal a + ENNReal.toReal b

theorem ENNReal.toReal_sub_of_le {a : ENNReal} {b : ENNReal} (h : b ≤ a) (ha : a ≠ ⊤) :

ENNReal.toReal (a - b) = ENNReal.toReal a - ENNReal.toReal b

theorem ENNReal.le_toReal_sub {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) :

ENNReal.toReal a - ENNReal.toReal b ≤ ENNReal.toReal (a - b)

theorem ENNReal.toReal_add_le {a : ENNReal} {b : ENNReal} :

ENNReal.toReal (a + b) ≤ ENNReal.toReal a + ENNReal.toReal b

theorem ENNReal.ofReal_add {p : ℝ} {q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

theorem ENNReal.ofReal_add_le {p : ℝ} {q : ℝ} :

ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q

@[simp]

theorem ENNReal.toReal_le_toReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b ↔ a ≤ b

theorem ENNReal.toReal_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :

ENNReal.toReal a ≤ ENNReal.toReal b

theorem ENNReal.toReal_mono' {a : ENNReal} {b : ENNReal} (h : a ≤ b) (ht : b = ⊤ → a = ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b

@[simp]

theorem ENNReal.toReal_lt_toReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal a < ENNReal.toReal b ↔ a < b

theorem ENNReal.toReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :

ENNReal.toReal a < ENNReal.toReal b

theorem ENNReal.toNNReal_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a ≤ b) :

ENNReal.toNNReal a ≤ ENNReal.toNNReal b

theorem ENNReal.toReal_le_add' {a : ENNReal} {b : ENNReal} {c : ENNReal} (hle : a ≤ b + c) (hb : b = ⊤ → a = ⊤) (hc : c = ⊤ → a = ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c

If a ≤ b + c and a = ∞ whenever b = ∞ or c = ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

theorem ENNReal.toReal_le_add {a : ENNReal} {b : ENNReal} {c : ENNReal} (hle : a ≤ b + c) (hb : b ≠ ⊤) (hc : c ≠ ⊤) :

ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c

If a ≤ b + c, b ≠ ∞, and c ≠ ∞, then ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c. This lemma is useful to transfer triangle-like inequalities from ENNReals to Reals.

@[simp]

theorem ENNReal.toNNReal_le_toNNReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toNNReal a ≤ ENNReal.toNNReal b ↔ a ≤ b

theorem ENNReal.toNNReal_strict_mono {a : ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : a < b) :

ENNReal.toNNReal a < ENNReal.toNNReal b

@[simp]

theorem ENNReal.toNNReal_lt_toNNReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toNNReal a < ENNReal.toNNReal b ↔ a < b

theorem ENNReal.toReal_max {a : ENNReal} {b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)

theorem ENNReal.toReal_min {a : ENNReal} {b : ENNReal} (hr : a ≠ ⊤) (hp : b ≠ ⊤) :

ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)

theorem ENNReal.toReal_sup {a : ENNReal} {b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → ENNReal.toReal (a ⊔ b) = ENNReal.toReal a ⊔ ENNReal.toReal b

theorem ENNReal.toReal_inf {a : ENNReal} {b : ENNReal} :

a ≠ ⊤ → b ≠ ⊤ → ENNReal.toReal (a ⊓ b) = ENNReal.toReal a ⊓ ENNReal.toReal b

theorem ENNReal.toNNReal_pos_iff {a : ENNReal} :

0 < ENNReal.toNNReal a ↔ 0 < a ∧ a < ⊤

theorem ENNReal.toNNReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

0 < ENNReal.toNNReal a

theorem ENNReal.toReal_pos_iff {a : ENNReal} :

0 < ENNReal.toReal a ↔ 0 < a ∧ a < ⊤

theorem ENNReal.toReal_pos {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) :

0 < ENNReal.toReal a

theorem ENNReal.ofReal_le_ofReal {p : ℝ} {q : ℝ} (h : p ≤ q) :

ENNReal.ofReal p ≤ ENNReal.ofReal q

theorem ENNReal.ofReal_le_of_le_toReal {a : ℝ} {b : ENNReal} (h : a ≤ ENNReal.toReal b) :

ENNReal.ofReal a ≤ b

@[simp]

theorem ENNReal.ofReal_le_ofReal_iff {p : ℝ} {q : ℝ} (h : 0 ≤ q) :

ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q

theorem ENNReal.ofReal_le_ofReal_iff' {p : ℝ} {q : ℝ} :

ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0

theorem ENNReal.ofReal_lt_ofReal_iff' {p : ℝ} {q : ℝ} :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q ∧ 0 < q

@[simp]

theorem ENNReal.ofReal_eq_ofReal_iff {p : ℝ} {q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :

ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

@[simp]

theorem ENNReal.ofReal_lt_ofReal_iff {p : ℝ} {q : ℝ} (h : 0 < q) :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

theorem ENNReal.ofReal_lt_ofReal_iff_of_nonneg {p : ℝ} {q : ℝ} (hp : 0 ≤ p) :

ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

@[simp]

theorem ENNReal.ofReal_pos {p : ℝ} :

0 < ENNReal.ofReal p ↔ 0 < p

@[simp]

theorem ENNReal.ofReal_eq_zero {p : ℝ} :

ENNReal.ofReal p = 0 ↔ p ≤ 0

@[simp]

theorem ENNReal.zero_eq_ofReal {p : ℝ} :

0 = ENNReal.ofReal p ↔ p ≤ 0

theorem ENNReal.ofReal_of_nonpos {p : ℝ} :

p ≤ 0 → ENNReal.ofReal p = 0

Alias of the reverse direction of ENNReal.ofReal_eq_zero.

@[simp]

theorem ENNReal.ofReal_lt_nat_cast {p : ℝ} {n : ℕ} (hn : n ≠ 0) :

ENNReal.ofReal p < ↑n ↔ p < ↑n

@[simp]

theorem ENNReal.ofReal_lt_one {p : ℝ} :

ENNReal.ofReal p < 1 ↔ p < 1

@[simp]

theorem ENNReal.ofReal_lt_ofNat {p : ℝ} {n : ℕ} [h : Nat.AtLeastTwo n] :

ENNReal.ofReal p < OfNat.ofNat n ↔ p < OfNat.ofNat n

@[simp]

theorem ENNReal.nat_cast_le_ofReal {n : ℕ} {p : ℝ} (hn : n ≠ 0) :

↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p

@[simp]

theorem ENNReal.one_le_ofReal {p : ℝ} :

1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

@[simp]

theorem ENNReal.ofNat_le_ofReal {n : ℕ} [h : Nat.AtLeastTwo n] {p : ℝ} :

OfNat.ofNat n ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p

@[simp]

theorem ENNReal.ofReal_le_nat_cast {r : ℝ} {n : ℕ} :

ENNReal.ofReal r ≤ ↑n ↔ r ≤ ↑n

@[simp]

theorem ENNReal.ofReal_le_one {r : ℝ} :

ENNReal.ofReal r ≤ 1 ↔ r ≤ 1

@[simp]

theorem ENNReal.ofReal_le_ofNat {r : ℝ} {n : ℕ} [Nat.AtLeastTwo n] :

ENNReal.ofReal r ≤ OfNat.ofNat n ↔ r ≤ OfNat.ofNat n

@[simp]

theorem ENNReal.nat_cast_lt_ofReal {n : ℕ} {r : ℝ} :

↑n < ENNReal.ofReal r ↔ ↑n < r

@[simp]

theorem ENNReal.one_lt_ofReal {r : ℝ} :

1 < ENNReal.ofReal r ↔ 1 < r

@[simp]

theorem ENNReal.ofNat_lt_ofReal {n : ℕ} [Nat.AtLeastTwo n] {r : ℝ} :

OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r

@[simp]

theorem ENNReal.ofReal_eq_nat_cast {r : ℝ} {n : ℕ} (h : n ≠ 0) :

ENNReal.ofReal r = ↑n ↔ r = ↑n

@[simp]

theorem ENNReal.ofReal_eq_one {r : ℝ} :

ENNReal.ofReal r = 1 ↔ r = 1

@[simp]

theorem ENNReal.ofReal_eq_ofNat {r : ℝ} {n : ℕ} [h : Nat.AtLeastTwo n] :

ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n

theorem ENNReal.ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :

ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

theorem ENNReal.ofReal_le_iff_le_toReal {a : ℝ} {b : ENNReal} (hb : b ≠ ⊤) :

ENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b

theorem ENNReal.ofReal_lt_iff_lt_toReal {a : ℝ} {b : ENNReal} (ha : 0 ≤ a) (hb : b ≠ ⊤) :

ENNReal.ofReal a < b ↔ a < ENNReal.toReal b

theorem ENNReal.ofReal_lt_coe_iff {a : ℝ} {b : NNReal} (ha : 0 ≤ a) :

ENNReal.ofReal a < ↑b ↔ a < ↑b

theorem ENNReal.le_ofReal_iff_toReal_le {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :

a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b

theorem ENNReal.toReal_le_of_le_ofReal {a : ENNReal} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) :

ENNReal.toReal a ≤ b

theorem ENNReal.lt_ofReal_iff_toReal_lt {a : ENNReal} {b : ℝ} (ha : a ≠ ⊤) :

a < ENNReal.ofReal b ↔ ENNReal.toReal a < b

theorem ENNReal.toReal_lt_of_lt_ofReal {a : ENNReal} {b : ℝ} (h : a < ENNReal.ofReal b) :

ENNReal.toReal a < b

theorem ENNReal.ofReal_mul {p : ℝ} {q : ℝ} (hp : 0 ≤ p) :

ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

theorem ENNReal.ofReal_mul' {p : ℝ} {q : ℝ} (hq : 0 ≤ q) :

ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

theorem ENNReal.ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :

ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

theorem ENNReal.ofReal_nsmul {x : ℝ} {n : ℕ} :

ENNReal.ofReal (n • x) = n • ENNReal.ofReal x

theorem ENNReal.ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) :

(ENNReal.ofReal x)⁻¹ = ENNReal.ofReal x⁻¹

theorem ENNReal.ofReal_div_of_pos {x : ℝ} {y : ℝ} (hy : 0 < y) :

ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

@[simp]

theorem ENNReal.toNNReal_mul {a : ENNReal} {b : ENNReal} :

ENNReal.toNNReal (a * b) = ENNReal.toNNReal a * ENNReal.toNNReal b

theorem ENNReal.toNNReal_mul_top (a : ENNReal) :

ENNReal.toNNReal (a * ⊤) = 0

theorem ENNReal.toNNReal_top_mul (a : ENNReal) :

ENNReal.toNNReal (⊤ * a) = 0

@[simp]

theorem ENNReal.smul_toNNReal (a : NNReal) (b : ENNReal) :

ENNReal.toNNReal (a • b) = a * ENNReal.toNNReal b

def ENNReal.toNNRealHom :

ENNReal →* NNReal

ENNReal.toNNReal as a MonoidHom.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ENNReal.toNNReal_pow (a : ENNReal) (n : ℕ) :

ENNReal.toNNReal (a ^ n) = ENNReal.toNNReal a ^ n

@[simp]

theorem ENNReal.toNNReal_prod {ι : Type u_3} {s : Finset ι} {f : ι → ENNReal} :

ENNReal.toNNReal (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ENNReal.toNNReal (f i)

def ENNReal.toRealHom :

ENNReal →* ℝ

ENNReal.toReal as a MonoidHom.

Equations

ENNReal.toRealHom = MonoidHom.comp (↑NNReal.toRealHom) ENNReal.toNNRealHom

Instances For

@[simp]

theorem ENNReal.toReal_mul {a : ENNReal} {b : ENNReal} :

ENNReal.toReal (a * b) = ENNReal.toReal a * ENNReal.toReal b

theorem ENNReal.toReal_nsmul (a : ENNReal) (n : ℕ) :

ENNReal.toReal (n • a) = n • ENNReal.toReal a

@[simp]

theorem ENNReal.toReal_pow (a : ENNReal) (n : ℕ) :

ENNReal.toReal (a ^ n) = ENNReal.toReal a ^ n

@[simp]

theorem ENNReal.toReal_prod {ι : Type u_3} {s : Finset ι} {f : ι → ENNReal} :

ENNReal.toReal (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ENNReal.toReal (f i)

theorem ENNReal.toReal_ofReal_mul (c : ℝ) (a : ENNReal) (h : 0 ≤ c) :

ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a

theorem ENNReal.toReal_mul_top (a : ENNReal) :

ENNReal.toReal (a * ⊤) = 0

theorem ENNReal.toReal_top_mul (a : ENNReal) :

ENNReal.toReal (⊤ * a) = 0

theorem ENNReal.toReal_eq_toReal {a : ENNReal} {b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal a = ENNReal.toReal b ↔ a = b

theorem ENNReal.toReal_smul (r : NNReal) (s : ENNReal) :

ENNReal.toReal (r • s) = r • ENNReal.toReal s

theorem ENNReal.trichotomy (p : ENNReal) :

p = 0 ∨ p = ⊤ ∨ 0 < ENNReal.toReal p

theorem ENNReal.trichotomy₂ {p : ENNReal} {q : ENNReal} (hpq : p ≤ q) :

p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ⊤ ∨ p = 0 ∧ 0 < ENNReal.toReal q ∨ p = ⊤ ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q

theorem ENNReal.dichotomy (p : ENNReal) [Fact (1 ≤ p)] :

p = ⊤ ∨ 1 ≤ ENNReal.toReal p

theorem ENNReal.toReal_pos_iff_ne_top (p : ENNReal) [Fact (1 ≤ p)] :

0 < ENNReal.toReal p ↔ p ≠ ⊤

theorem ENNReal.toNNReal_inv (a : ENNReal) :

ENNReal.toNNReal a⁻¹ = (ENNReal.toNNReal a)⁻¹

theorem ENNReal.toNNReal_div (a : ENNReal) (b : ENNReal) :

ENNReal.toNNReal (a / b) = ENNReal.toNNReal a / ENNReal.toNNReal b

theorem ENNReal.toReal_inv (a : ENNReal) :

ENNReal.toReal a⁻¹ = (ENNReal.toReal a)⁻¹

theorem ENNReal.toReal_div (a : ENNReal) (b : ENNReal) :

ENNReal.toReal (a / b) = ENNReal.toReal a / ENNReal.toReal b

theorem ENNReal.ofReal_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) :

ENNReal.ofReal (Finset.prod s fun (i : α) => f i) = Finset.prod s fun (i : α) => ENNReal.ofReal (f i)

theorem ENNReal.toNNReal_iInf {ι : Sort u_3} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)

theorem ENNReal.toNNReal_sInf (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toNNReal (sInf s) = sInf (ENNReal.toNNReal '' s)

theorem ENNReal.toNNReal_iSup {ι : Sort u_3} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toNNReal (iSup f) = ⨆ (i : ι), ENNReal.toNNReal (f i)

theorem ENNReal.toNNReal_sSup (s : Set ENNReal) (hs : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toNNReal (sSup s) = sSup (ENNReal.toNNReal '' s)

theorem ENNReal.toReal_iInf {ι : Sort u_3} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toReal (iInf f) = ⨅ (i : ι), ENNReal.toReal (f i)

theorem ENNReal.toReal_sInf (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toReal (sInf s) = sInf (ENNReal.toReal '' s)

theorem ENNReal.toReal_iSup {ι : Sort u_3} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) :

ENNReal.toReal (iSup f) = ⨆ (i : ι), ENNReal.toReal (f i)

theorem ENNReal.toReal_sSup (s : Set ENNReal) (hf : ∀ r ∈ s, r ≠ ⊤) :

ENNReal.toReal (sSup s) = sSup (ENNReal.toReal '' s)

theorem ENNReal.iInf_add {a : ENNReal} {ι : Sort u_3} {f : ι → ENNReal} :

iInf f + a = ⨅ (i : ι), f i + a

theorem ENNReal.iSup_sub {a : ENNReal} {ι : Sort u_3} {f : ι → ENNReal} :

(⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a

theorem ENNReal.sub_iInf {a : ENNReal} {ι : Sort u_3} {f : ι → ENNReal} :

a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

theorem ENNReal.sInf_add {a : ENNReal} {s : Set ENNReal} :

sInf s + a = ⨅ b ∈ s, b + a

theorem ENNReal.add_iInf {ι : Sort u_3} {f : ι → ENNReal} {a : ENNReal} :

a + iInf f = ⨅ (b : ι), a + f b

theorem ENNReal.iInf_add_iInf {ι : Sort u_3} {f : ι → ENNReal} {g : ι → ENNReal} (h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j) :

iInf f + iInf g = ⨅ (a : ι), f a + g a

theorem ENNReal.iInf_sum {α : Type u_1} {ι : Sort u_3} {f : ι → α → ENNReal} {s : Finset α} [Nonempty ι] (h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) :

(⨅ (i : ι), Finset.sum s fun (a : α) => f i a) = Finset.sum s fun (a : α) => ⨅ (i : ι), f i a

theorem ENNReal.iInf_mul_of_ne {ι : Sort u_4} {f : ι → ENNReal} {x : ENNReal} (h0 : x ≠ 0) (h : x ≠ ⊤) :

iInf f * x = ⨅ (i : ι), f i * x

If x ≠ 0 and x ≠ ∞, then right multiplication by x maps infimum to infimum. See also ENNReal.iInf_mul that assumes [Nonempty ι] but does not require x ≠ 0.

theorem ENNReal.iInf_mul {ι : Sort u_4} [Nonempty ι] {f : ι → ENNReal} {x : ENNReal} (h : x ≠ ⊤) :

iInf f * x = ⨅ (i : ι), f i * x

If x ≠ ∞, then right multiplication by x maps infimum over a nonempty type to infimum. See also ENNReal.iInf_mul_of_ne that assumes x ≠ 0 but does not require [Nonempty ι].

theorem ENNReal.mul_iInf {ι : Sort u_4} [Nonempty ι] {f : ι → ENNReal} {x : ENNReal} (h : x ≠ ⊤) :

x * iInf f = ⨅ (i : ι), x * f i

If x ≠ ∞, then left multiplication by x maps infimum over a nonempty type to infimum. See also ENNReal.mul_iInf_of_ne that assumes x ≠ 0 but does not require [Nonempty ι].

theorem ENNReal.mul_iInf_of_ne {ι : Sort u_4} {f : ι → ENNReal} {x : ENNReal} (h0 : x ≠ 0) (h : x ≠ ⊤) :

x * iInf f = ⨅ (i : ι), x * f i

If x ≠ 0 and x ≠ ∞, then left multiplication by x maps infimum to infimum. See also ENNReal.mul_iInf that assumes [Nonempty ι] but does not require x ≠ 0.

supr_mul, mul_supr and variants are in Topology.Instances.ENNReal.

@[simp]

theorem ENNReal.iSup_eq_zero {ι : Sort u_3} {f : ι → ENNReal} :

⨆ (i : ι), f i = 0 ↔ ∀ (i : ι), f i = 0

@[simp]

theorem ENNReal.iSup_zero_eq_zero {ι : Sort u_3} :

⨆ (x : ι), 0 = 0

theorem ENNReal.sup_eq_zero {a : ENNReal} {b : ENNReal} :

a ⊔ b = 0 ↔ a = 0 ∧ b = 0

theorem ENNReal.iSup_coe_nat :

⨆ (n : ℕ), ↑n = ⊤

theorem Set.OrdConnected.preimage_coe_nnreal_ennreal {u : Set ENNReal} (h : Set.OrdConnected u) :

Set.OrdConnected (ENNReal.ofNNReal ⁻¹' u)

theorem Set.OrdConnected.image_coe_nnreal_ennreal {t : Set NNReal} (h : Set.OrdConnected t) :

Set.OrdConnected (ENNReal.ofNNReal '' t)

theorem Set.OrdConnected.preimage_ennreal_ofReal {u : Set ENNReal} (h : Set.OrdConnected u) :

Set.OrdConnected (ENNReal.ofReal ⁻¹' u)

theorem Set.OrdConnected.image_ennreal_ofReal {s : Set ℝ} (h : Set.OrdConnected s) :

Set.OrdConnected (ENNReal.ofReal '' s)

def Mathlib.Meta.Positivity.evalENNRealtoReal :

Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: ENNReal.toReal.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Mathlib.Meta.Positivity.evalENNRealOfReal :

Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: ENNReal.toReal.

Equations

One or more equations did not get rendered due to their size.

Instances For

def Mathlib.Meta.Positivity.evalENNRealOfNNReal :

Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: ENNReal.ofNNReal.

Equations

One or more equations did not get rendered due to their size.

Instances For