@[simp]

theorem enorm_toReal_le {x : ENNReal} : ‖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) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : E) : (n + 1) • x = 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

instance instENormSMulClassENNReal_carleson : ENormSMulClass ENNReal ENNReal

instance instContinuousConstSMulNNRealENNReal_carleson : ContinuousConstSMul NNReal ENNReal

@[instance_reducible]

instance instContinuousENormNNReal_carleson : ContinuousENorm NNReal

Equations

• instContinuousENormNNReal_carleson = { toENorm := NNNorm.toENorm, continuous_enorm := instContinuousENormNNReal_carleson._proof_1 }

@[instance_reducible]

instance instENormedAddCommMonoidNNReal_carleson : ENormedAddCommMonoid NNReal

Equations

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

instance instENormSMulClassNNRealENNReal_carleson : ENormSMulClass NNReal ENNReal

instance instENormSMulClassNNReal_carleson {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] : ENormSMulClass NNReal E

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

theorem ENNReal.toNNReal_smul {α : Type u_6} {c : ENNReal} (hc : c ≠ ⊤) {f : α → ENNReal} : c.toNNReal • f = c • f

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

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

theorem MeasureTheory.eLpNorm_top_smul {α : Type u_8} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ENNReal} (hf : AEStronglyMeasurable f μ) : eLpNorm (⊤ • f) p μ = ⊤ * eLpNorm f p μ

theorem MeasureTheory.eLpNorm_const_smul'' {α : Type u_8} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {c : ENNReal} (hc : c ≠ ⊤) {f : α → ENNReal} : eLpNorm (c • f) p μ = c * eLpNorm f p μ

theorem MeasureTheory.eLpNorm_const_smul''' {α : Type u_8} {m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {c : ENNReal} {f : α → ENNReal} (hf : AEStronglyMeasurable f μ) : eLpNorm (c • f) p μ = c * eLpNorm f p μ

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