theorem ENNReal.ofReal_norm {E : Type u_3} [SeminormedAddGroup E] (x : E) : ENNReal.ofReal ‖x‖ = ‖x‖ₑ

@[simp]

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

@[simp]

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

class ContinuousENorm (E : Type u_7) extends ENorm E, TopologicalSpace E : Type u_7

A type E equipped with a continuous map ‖·‖ₑ : E → ℝ≥0∞. Note: do we want to unbundle this (at least separate out TopologicalSpace E?) Note: not sure if this is the "right" class to add to Mathlib.

• enorm : E → ENNReal
• IsOpen : Set E → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set E) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set E)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• continuous_enorm : Continuous enorm

class ENormedAddMonoid (E : Type u_7) extends ContinuousENorm E, AddMonoid E : Type u_7

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
• IsOpen : Set E → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set E) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set E)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• 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_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

class ENormedAddCommMonoid (E : Type u_7) extends ENormedAddMonoid E, AddCommMonoid E : Type u_7

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
• IsOpen : Set E → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set E) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set E)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• 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_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a

class ENormedAddCommSubMonoid (E : Type u_7) extends ENormedAddCommMonoid E, Sub E : Type u_7

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
• IsOpen : Set E → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set E) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set E)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• 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_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a
• 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_7) extends ENormedAddCommMonoid E, Module NNReal E : Type u_7

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
• IsOpen : Set E → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set E) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set E)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• 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_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a
• 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 (c : NNReal) (x : E) : ‖c • x‖ₑ = c • ‖x‖ₑ

@[simp]

theorem enorm_zero {ε : Type u_7} [ENormedAddMonoid ε] : ‖0‖ₑ = 0

instance instENormedSpaceENNReal : ENormedSpace ENNReal

Equations

• instENormedSpaceENNReal = ENormedSpace.mk instENormedSpaceENNReal.proof_4

instance instContinuousENormOfSeminormedAddGroup {E : Type u_3} [SeminormedAddGroup E] : ContinuousENorm E

Equations

• instContinuousENormOfSeminormedAddGroup = ContinuousENorm.mk ⋯

instance instENormedAddMonoidOfNormedAddGroup {E : Type u_3} [NormedAddGroup E] : ENormedAddMonoid E

Equations

• instENormedAddMonoidOfNormedAddGroup = ENormedAddMonoid.mk ⋯ ⋯

@[simp]

theorem enorm_neg {E : Type u_3} [NormedAddGroup E] (x : E) : ‖-x‖ₑ = ‖x‖ₑ

instance instENormedAddCommMonoidOfNormedAddCommGroup {E : Type u_3} [NormedAddCommGroup E] : ENormedAddCommMonoid E

Equations

• instENormedAddCommMonoidOfNormedAddCommGroup = ENormedAddCommMonoid.mk ⋯

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

Equations

• instENormedSpaceOfNormedSpaceReal = ENormedSpace.mk ⋯

theorem MeasureTheory.Continuous.enorm {E : Type u_8} [ContinuousENorm E] {X : Type u_9} [TopologicalSpace X] {f : X → E} (hf : Continuous f) : Continuous fun (x : X) => ‖f x‖ₑ

theorem MeasureTheory.measurable_enorm {E : Type u_8} [ContinuousENorm E] [MeasurableSpace E] [OpensMeasurableSpace E] : Measurable fun (a : E) => ‖a‖ₑ

theorem MeasureTheory.AEMeasurable.enorm {α : Type u_7} {E : Type u_8} {m : MeasurableSpace α} [ContinuousENorm E] {μ : Measure α} [MeasurableSpace E] [OpensMeasurableSpace E] {f : α → E} (hf : AEMeasurable f μ) : AEMeasurable (fun (a : α) => ‖f a‖ₑ) μ

theorem MeasureTheory.AEStronglyMeasurable.enorm {α : Type u_7} {E : Type u_8} {m : MeasurableSpace α} [ContinuousENorm E] {μ : Measure α} {f : α → E} (hf : AEStronglyMeasurable f μ) : AEMeasurable (fun (a : α) => ‖f a‖ₑ) μ

theorem MeasureTheory.StronglyMeasurable.enorm {α : Type u_7} {E : Type u_8} {m : MeasurableSpace α} [ContinuousENorm E] {f : α → E} (hf : StronglyMeasurable f) : StronglyMeasurable fun (a : α) => ‖f a‖ₑ

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