@[simp]

theorem enorm_toReal_le {x : ENNReal} : ‖x.toReal‖ₑ ≤ x

@[simp]

theorem enorm_toReal {x : ENNReal} (hx : x ≠ ⊤) : ‖x.toReal‖ₑ = x

@[simp]

theorem enorm_NNReal {x : NNReal} : ‖x‖ₑ = ↑x

class ENormedAddCommSubMonoid (E : Type u_6) [TopologicalSpace E] extends ENormedAddCommMonoid E, Sub E : Type u_6

An enormed monoid is an additive monoid endowed with a continuous enorm. Note: not sure if this is the "right" class to add to Mathlib.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• add : E → E → E
• add_assoc (a b c : E) : a + b + c = a + (b + c)
• zero : E
• zero_add (a : E) : 0 + a = a
• add_zero (a : E) : a + 0 = a
• nsmul : ℕ → E → E
• nsmul_zero (x : E) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : E) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• enorm_zero : ‖0‖ₑ = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a
• enorm_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0
• sub : E → E → E
• sub_add_cancel_of_enorm_le ⦃x y : E⦄ : ‖y‖ₑ ≤ ‖x‖ₑ → x - y + y = x
• add_right_cancel_of_enorm_lt_top ⦃x : E⦄ : ‖x‖ₑ < ⊤ → ∀ {y z : E}, y + x = z + x → y = z
• esub_self (x : E) : x - x = 0

class ENormedSpace (E : Type u_6) [TopologicalSpace E] extends ENormedAddCommMonoid E, Module NNReal E : Type u_6

An enormed space is an additive monoid endowed with a continuous enorm. Note: not sure if this is the "right" class to add to Mathlib.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• add : E → E → E
• add_assoc (a b c : E) : a + b + c = a + (b + c)
• zero : E
• zero_add (a : E) : 0 + a = a
• add_zero (a : E) : a + 0 = a
• nsmul : ℕ → E → E
• nsmul_zero (x : E) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : E) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• enorm_zero : ‖0‖ₑ = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a
• enorm_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0
• smul : NNReal → E → E
• one_smul (b : E) : 1 • b = b
• mul_smul (x y : NNReal) (b : E) : (x * y) • b = x • y • b
• smul_zero (a : NNReal) : a • 0 = 0
• smul_add (a : NNReal) (x y : E) : a • (x + y) = a • x + a • y
• add_smul (r s : NNReal) (x : E) : (r + s) • x = r • x + s • x
• zero_smul (x : E) : 0 • x = 0
• enorm_smul_eq_smul (c : NNReal) (x : E) : ‖c • x‖ₑ = c • ‖x‖ₑ

instance instENormedSpaceENNReal : ENormedSpace ENNReal

Equations

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

instance instENormedSpaceNNReal : ENormedSpace NNReal

Equations

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

instance instENormedSpaceOfNormedSpaceReal {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] : ENormedSpace E

Equations

• instENormedSpaceOfNormedSpaceReal = { toENormedAddCommMonoid := NormedAddCommGroup.toENormedAddCommMonoid, toModule := NNReal.instModuleOfReal, enorm_smul_eq_smul := ⋯ }

theorem MeasureTheory.esub_zero {E : Type u_3} [TopologicalSpace E] [ENormedAddCommSubMonoid E] {x : E} : x - 0 = x

theorem MeasureTheory.enorm_smul_eq_mul {ε : Type u_6} [TopologicalSpace ε] [ENormedSpace ε] {c : NNReal} (z : ε) : ‖c • z‖ₑ = ‖c‖ₑ * ‖z‖ₑ

instance MeasureTheory.instContinuousConstSMulNNRealENNReal_carleson : ContinuousConstSMul NNReal ENNReal

theorem MeasureTheory.eLpNorm_const_nnreal_smul_le {ε : Type u_6} [TopologicalSpace ε] [ENormedSpace ε] {α : Type u_7} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {c : NNReal} {f : α → ε} : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ

theorem MeasureTheory.eLpNorm_const_smul' {ε : Type u_6} [TopologicalSpace ε] [ENormedSpace ε] {α : Type u_7} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {c : NNReal} {f : α → ε} : eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

theorem MeasureTheory.eLpNormEssSup_const_nnreal_smul_le {ε : Type u_6} [TopologicalSpace ε] [ENormedSpace ε] {α : Type u_7} {m0 : MeasurableSpace α} {μ : Measure α} {c : NNReal} {f : α → ε} : eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ