Lp space

This file provides the space Lp E p μ as the subtype of elements of α →ₘ[μ] E (see MeasureTheory.AEEqFun) such that eLpNorm f p μ is finite. For 1 ≤ p, eLpNorm defines a norm and Lp is a complete metric space (the latter is proved at Mathlib.MeasureTheory.Function.LpSpace.Complete).

Main definitions

• Lp E p μ : elements of α →ₘ[μ] E such that eLpNorm f p μ is finite. Defined as an AddSubgroup of α →ₘ[μ] E.

Lipschitz functions vanishing at zero act by composition on Lp. We define this action, and prove that it is continuous. In particular,

• ContinuousLinearMap.compLp defines the action on Lp of a continuous linear map.
• Lp.posPart is the positive part of an Lp function.
• Lp.negPart is the negative part of an Lp function.

Notations

• α →₁[μ] E : the type Lp E 1 μ.
• α →₂[μ] E : the type Lp E 2 μ.

Implementation

Since Lp is defined as an AddSubgroup, dot notation does not work. Use Lp.Measurable f to say that the coercion of f to a genuine function is measurable, instead of the non-working f.Measurable.

To prove that two Lp elements are equal, it suffices to show that their coercions to functions coincide almost everywhere (this is registered as an ext rule). This can often be done using filter_upwards. For instance, a proof from first principles that f + (g + h) = (f + g) + h could read (in the Lp namespace)

example (f g h : Lp E p μ) : (f + g) + h = f + (g + h) := by
  ext1
  filter_upwards [coeFn_add (f + g) h, coeFn_add f g, coeFn_add f (g + h), coeFn_add g h]
    with _ ha1 ha2 ha3 ha4
  simp only [ha1, ha2, ha3, ha4, add_assoc]

The lemma coeFn_add states that the coercion of f + g coincides almost everywhere with the sum of the coercions of f and g. All such lemmas use coeFn in their name, to distinguish the function coercion from the coercion to almost everywhere defined functions.

Lp space

The space of equivalence classes of measurable functions for which eLpNorm f p μ < ∞.

@[simp]

theorem MeasureTheory.eLpNorm_aeeqFun {α : Type u_6} {E : Type u_7} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} (hf : AEStronglyMeasurable f μ) : eLpNorm (↑(AEEqFun.mk f hf)) p μ = eLpNorm f p μ

theorem MeasureTheory.MemLp.eLpNorm_mk_lt_top {α : Type u_6} {E : Type u_7} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} (hfp : MemLp f p μ) : eLpNorm (↑(AEEqFun.mk f ⋯)) p μ < ⊤

@[deprecated MeasureTheory.MemLp.eLpNorm_mk_lt_top (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.eLpNorm_mk_lt_top {α : Type u_6} {E : Type u_7} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} (hfp : MemLp f p μ) : eLpNorm (↑(AEEqFun.mk f ⋯)) p μ < ⊤

Alias of MeasureTheory.MemLp.eLpNorm_mk_lt_top.

def MeasureTheory.Lp {α : Type u_7} (E : Type u_6) {m : MeasurableSpace α} [NormedAddCommGroup E] (p : ENNReal) (μ : Measure α := by volume_tac) : AddSubgroup (α →ₘ[μ] E)

Lp space

Equations

• MeasureTheory.Lp E p μ = { carrier := {f : α →ₘ[μ] E | MeasureTheory.eLpNorm (↑f) p μ < ⊤}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def MeasureTheory.«term_→₁[_]_» : Lean.TrailingParserDescr

α →₁[μ] E is the type of L¹ or integrable functions from α to E.

Equations

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

def MeasureTheory.«term_→₂[_]_» : Lean.TrailingParserDescr

α →₂[μ] E is the type of L² or square-integrable functions from α to E.

Equations

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

def MeasureTheory.MemLp.toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : α → E) (h_mem_ℒp : MemLp f p μ) : ↥(Lp E p μ)

make an element of Lp from a function verifying MemLp

Equations

• MeasureTheory.MemLp.toLp f h_mem_ℒp = ⟨MeasureTheory.AEEqFun.mk f ⋯, ⋯⟩

theorem MeasureTheory.MemLp.toLp_val {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (h : MemLp f p μ) : ↑(toLp f h) = AEEqFun.mk f ⋯

theorem MeasureTheory.MemLp.coeFn_toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) : ↑↑(toLp f hf) =ᶠ[ae μ] f

theorem MeasureTheory.MemLp.toLp_congr {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) (hfg : f =ᶠ[ae μ] g) : toLp f hf = toLp g hg

@[simp]

theorem MeasureTheory.MemLp.toLp_eq_toLp_iff {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : toLp f hf = toLp g hg ↔ f =ᶠ[ae μ] g

@[simp]

theorem MeasureTheory.MemLp.toLp_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (h : MemLp 0 p μ) : toLp 0 h = 0

theorem MeasureTheory.MemLp.toLp_add {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : toLp (f + g) ⋯ = toLp f hf + toLp g hg

theorem MeasureTheory.MemLp.toLp_neg {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) : toLp (-f) ⋯ = -toLp f hf

theorem MeasureTheory.MemLp.toLp_sub {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : toLp (f - g) ⋯ = toLp f hf - toLp g hg

instance MeasureTheory.Lp.instCoeFun {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : CoeFun ↥(Lp E p μ) fun (x : ↥(Lp E p μ)) => α → E

Equations

• MeasureTheory.Lp.instCoeFun = { coe := fun (f : ↥(MeasureTheory.Lp E p μ)) => ↑↑f }

theorem MeasureTheory.Lp.ext {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : ↥(Lp E p μ)} (h : ↑↑f =ᶠ[ae μ] ↑↑g) : f = g

theorem MeasureTheory.Lp.ext_iff {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f g : ↥(Lp E p μ)} : f = g ↔ ↑↑f =ᶠ[ae μ] ↑↑g

theorem MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ eLpNorm (↑f) p μ < ⊤

theorem MeasureTheory.Lp.mem_Lp_iff_memLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ MemLp (↑f) p μ

@[deprecated MeasureTheory.Lp.mem_Lp_iff_memLp (since := "2025-02-21")]

theorem MeasureTheory.Lp.mem_Lp_iff_memℒp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α →ₘ[μ] E} : f ∈ Lp E p μ ↔ MemLp (↑f) p μ

Alias of MeasureTheory.Lp.mem_Lp_iff_memLp.

theorem MeasureTheory.Lp.antitone {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [IsFiniteMeasure μ] {p q : ENNReal} (hpq : p ≤ q) : Lp E q μ ≤ Lp E p μ

@[simp]

theorem MeasureTheory.Lp.coeFn_mk {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α →ₘ[μ] E} (hf : eLpNorm (↑f) p μ < ⊤) : ↑↑⟨f, hf⟩ = ↑f

theorem MeasureTheory.Lp.coe_mk {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α →ₘ[μ] E} (hf : eLpNorm (↑f) p μ < ⊤) : ↑⟨f, hf⟩ = f

@[simp]

theorem MeasureTheory.Lp.toLp_coeFn {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hf : MemLp (↑↑f) p μ) : MemLp.toLp (↑↑f) hf = f

theorem MeasureTheory.Lp.eLpNorm_lt_top {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : eLpNorm (↑↑f) p μ < ⊤

theorem MeasureTheory.Lp.eLpNorm_ne_top {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : eLpNorm (↑↑f) p μ ≠ ⊤

theorem MeasureTheory.Lp.stronglyMeasurable {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : StronglyMeasurable ↑↑f

theorem MeasureTheory.Lp.aestronglyMeasurable {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : AEStronglyMeasurable (↑↑f) μ

theorem MeasureTheory.Lp.memLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : MemLp (↑↑f) p μ

@[deprecated MeasureTheory.Lp.memLp (since := "2025-02-21")]

theorem MeasureTheory.Lp.memℒp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : MemLp (↑↑f) p μ

Alias of MeasureTheory.Lp.memLp.

theorem MeasureTheory.Lp.coeFn_zero {α : Type u_1} (E : Type u_4) {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] : ↑↑0 =ᶠ[ae μ] 0

theorem MeasureTheory.Lp.coeFn_neg {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ↑↑(-f) =ᶠ[ae μ] -↑↑f

theorem MeasureTheory.Lp.coeFn_add {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : ↑↑(f + g) =ᶠ[ae μ] ↑↑f + ↑↑g

theorem MeasureTheory.Lp.coeFn_sub {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : ↑↑(f - g) =ᶠ[ae μ] ↑↑f - ↑↑g

theorem MeasureTheory.Lp.const_mem_Lp {E : Type u_4} {p : ENNReal} [NormedAddCommGroup E] (α : Type u_6) {x✝ : MeasurableSpace α} (μ : Measure α) (c : E) [IsFiniteMeasure μ] : AEEqFun.const α c ∈ Lp E p μ

instance MeasureTheory.Lp.instNorm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : Norm ↥(Lp E p μ)

Equations

• MeasureTheory.Lp.instNorm = { norm := fun (f : ↥(MeasureTheory.Lp E p μ)) => (MeasureTheory.eLpNorm (↑↑f) p μ).toReal }

instance MeasureTheory.Lp.instNNNorm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : NNNorm ↥(Lp E p μ)

Equations

• MeasureTheory.Lp.instNNNorm = { nnnorm := fun (f : ↥(MeasureTheory.Lp E p μ)) => ⟨‖f‖, ⋯⟩ }

instance MeasureTheory.Lp.instDist {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : Dist ↥(Lp E p μ)

Equations

• MeasureTheory.Lp.instDist = { dist := fun (f g : ↥(MeasureTheory.Lp E p μ)) => ‖f - g‖ }

instance MeasureTheory.Lp.instEDist {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : EDist ↥(Lp E p μ)

Equations

• MeasureTheory.Lp.instEDist = { edist := fun (f g : ↥(MeasureTheory.Lp E p μ)) => MeasureTheory.eLpNorm (↑↑f - ↑↑g) p μ }

theorem MeasureTheory.Lp.norm_def {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ‖f‖ = (eLpNorm (↑↑f) p μ).toReal

theorem MeasureTheory.Lp.nnnorm_def {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ‖f‖₊ = (eLpNorm (↑↑f) p μ).toNNReal

@[simp]

theorem MeasureTheory.Lp.coe_nnnorm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ↑‖f‖₊ = ‖f‖

@[simp]

theorem MeasureTheory.Lp.enorm_def {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ‖f‖ₑ = eLpNorm (↑↑f) p μ

@[deprecated MeasureTheory.Lp.enorm_def (since := "2025-01-20")]

theorem MeasureTheory.Lp.nnnorm_coe_ennreal {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ‖f‖ₑ = eLpNorm (↑↑f) p μ

Alias of MeasureTheory.Lp.enorm_def.

@[simp]

theorem MeasureTheory.Lp.norm_toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : α → E) (hf : MemLp f p μ) : ‖MemLp.toLp f hf‖ = (eLpNorm f p μ).toReal

@[simp]

theorem MeasureTheory.Lp.nnnorm_toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : α → E) (hf : MemLp f p μ) : ‖MemLp.toLp f hf‖₊ = (eLpNorm f p μ).toNNReal

theorem MeasureTheory.Lp.enorm_toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) : ‖MemLp.toLp f hf‖ₑ = eLpNorm f p μ

@[deprecated MeasureTheory.Lp.enorm_toLp (since := "2025-01-20")]

theorem MeasureTheory.Lp.coe_nnnorm_toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) : ‖MemLp.toLp f hf‖ₑ = eLpNorm f p μ

Alias of MeasureTheory.Lp.enorm_toLp.

theorem MeasureTheory.Lp.dist_def {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : dist f g = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

theorem MeasureTheory.Lp.edist_def {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : edist f g = eLpNorm (↑↑f - ↑↑g) p μ

theorem MeasureTheory.Lp.edist_dist {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : edist f g = ENNReal.ofReal (dist f g)

theorem MeasureTheory.Lp.dist_edist {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : dist f g = (edist f g).toReal

theorem MeasureTheory.Lp.dist_eq_norm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : ↥(Lp E p μ)) : dist f g = ‖f - g‖

@[simp]

theorem MeasureTheory.Lp.edist_toLp_toLp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f g : α → E) (hf : MemLp f p μ) (hg : MemLp g p μ) : edist (MemLp.toLp f hf) (MemLp.toLp g hg) = eLpNorm (f - g) p μ

@[simp]

theorem MeasureTheory.Lp.edist_toLp_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : α → E) (hf : MemLp f p μ) : edist (MemLp.toLp f hf) 0 = eLpNorm f p μ

@[simp]

theorem MeasureTheory.Lp.nnnorm_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : ‖0‖₊ = 0

@[simp]

theorem MeasureTheory.Lp.norm_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] : ‖0‖ = 0

@[simp]

theorem MeasureTheory.Lp.norm_measure_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} [NormedAddCommGroup E] (f : ↥(Lp E p 0)) : ‖f‖ = 0

@[simp]

theorem MeasureTheory.Lp.norm_exponent_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E 0 μ)) : ‖f‖ = 0

theorem MeasureTheory.Lp.nnnorm_eq_zero_iff {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : ↥(Lp E p μ)} (hp : 0 < p) : ‖f‖₊ = 0 ↔ f = 0

theorem MeasureTheory.Lp.norm_eq_zero_iff {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : ↥(Lp E p μ)} (hp : 0 < p) : ‖f‖ = 0 ↔ f = 0

theorem MeasureTheory.Lp.eq_zero_iff_ae_eq_zero {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : ↥(Lp E p μ)} : f = 0 ↔ ↑↑f =ᶠ[ae μ] 0

@[simp]

theorem MeasureTheory.Lp.nnnorm_neg {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ‖-f‖₊ = ‖f‖₊

@[simp]

theorem MeasureTheory.Lp.norm_neg {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) : ‖-f‖ = ‖f‖

theorem MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : NNReal} {f : ↥(Lp E p μ)} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊) : ‖f‖₊ ≤ c * ‖g‖₊

theorem MeasureTheory.Lp.norm_le_mul_norm_of_ae_le_mul {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : ℝ} {f : ↥(Lp E p μ)} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖) : ‖f‖ ≤ c * ‖g‖

theorem MeasureTheory.Lp.norm_le_norm_of_ae_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : ↥(Lp E p μ)} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖) : ‖f‖ ≤ ‖g‖

theorem MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le_mul {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : NNReal} {f : α →ₘ[μ] E} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ c * ‖↑↑g x‖₊) : f ∈ Lp E p μ

theorem MeasureTheory.Lp.mem_Lp_of_ae_le_mul {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : ℝ} {f : α →ₘ[μ] E} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ c * ‖↑↑g x‖) : f ∈ Lp E p μ

theorem MeasureTheory.Lp.mem_Lp_of_nnnorm_ae_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α →ₘ[μ] E} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ ‖↑↑g x‖₊) : f ∈ Lp E p μ

theorem MeasureTheory.Lp.mem_Lp_of_ae_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α →ₘ[μ] E} {g : ↥(Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ ‖↑↑g x‖) : f ∈ Lp E p μ

theorem MeasureTheory.Lp.mem_Lp_of_ae_nnnorm_bound {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [IsFiniteMeasure μ] {f : α →ₘ[μ] E} (C : NNReal) (hfC : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ C) : f ∈ Lp E p μ

theorem MeasureTheory.Lp.mem_Lp_of_ae_bound {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [IsFiniteMeasure μ] {f : α →ₘ[μ] E} (C : ℝ) (hfC : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ C) : f ∈ Lp E p μ

theorem MeasureTheory.Lp.nnnorm_le_of_ae_bound {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [IsFiniteMeasure μ] {f : ↥(Lp E p μ)} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C) : ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

theorem MeasureTheory.Lp.norm_le_of_ae_bound {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [IsFiniteMeasure μ] {f : ↥(Lp E p μ)} {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C) : ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * C

instance MeasureTheory.Lp.instNormedAddCommGroup {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [hp : Fact (1 ≤ p)] : NormedAddCommGroup ↥(Lp E p μ)

Equations

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

theorem MeasureTheory.Lp.const_smul_mem_Lp {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) (f : ↥(Lp E p μ)) : c • ↑f ∈ Lp E p μ

def MeasureTheory.Lp.LpSubmodule {α : Type u_1} (𝕜 : Type u_2) (E : Type u_4) {m : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : Submodule 𝕜 (α →ₘ[μ] E)

The 𝕜-submodule of elements of α →ₘ[μ] E whose Lp norm is finite. This is Lp E p μ, with extra structure.

Equations

• MeasureTheory.Lp.LpSubmodule 𝕜 E p μ = { toAddSubmonoid := (MeasureTheory.Lp E p μ).toAddSubmonoid, smul_mem' := ⋯ }

theorem MeasureTheory.Lp.coe_LpSubmodule {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : (LpSubmodule 𝕜 E p μ).toAddSubgroup = Lp E p μ

instance MeasureTheory.Lp.instModule {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : Module 𝕜 ↥(Lp E p μ)

Equations

• MeasureTheory.Lp.instModule = (MeasureTheory.Lp.LpSubmodule 𝕜 E p μ).module

theorem MeasureTheory.Lp.coeFn_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (c : 𝕜) (f : ↥(Lp E p μ)) : ↑↑(c • f) =ᶠ[ae μ] c • ↑↑f

instance MeasureTheory.Lp.instIsCentralScalar {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Module 𝕜ᵐᵒᵖ E] [IsBoundedSMul 𝕜ᵐᵒᵖ E] [IsCentralScalar 𝕜 E] : IsCentralScalar 𝕜 ↥(Lp E p μ)

instance MeasureTheory.Lp.instSMulCommClass {α : Type u_1} {𝕜 : Type u_2} {𝕜' : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [NormedRing 𝕜'] [Module 𝕜 E] [Module 𝕜' E] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜' E] [SMulCommClass 𝕜 𝕜' E] : SMulCommClass 𝕜 𝕜' ↥(Lp E p μ)

instance MeasureTheory.Lp.instIsScalarTower {α : Type u_1} {𝕜 : Type u_2} {𝕜' : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [NormedRing 𝕜'] [Module 𝕜 E] [Module 𝕜' E] [IsBoundedSMul 𝕜 E] [IsBoundedSMul 𝕜' E] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower 𝕜 𝕜' ↥(Lp E p μ)

instance MeasureTheory.Lp.instIsBoundedSMul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 ↥(Lp E p μ)

instance MeasureTheory.Lp.instNormedSpace {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {𝕜 : Type u_6} [NormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] : NormedSpace 𝕜 ↥(Lp E p μ)

Equations

• MeasureTheory.Lp.instNormedSpace = { toModule := MeasureTheory.Lp.instModule, norm_smul_le := ⋯ }

theorem MeasureTheory.MemLp.toLp_const_smul {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {𝕜 : Type u_6} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {f : α → E} (c : 𝕜) (hf : MemLp f p μ) : toLp (c • f) ⋯ = c • toLp f hf

theorem MeasureTheory.MemLp.norm_rpow_div {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) (q : ENNReal) : MemLp (fun (x : α) => ‖f x‖ ^ q.toReal) (p / q) μ

@[deprecated MeasureTheory.MemLp.norm_rpow_div (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.norm_rpow_div {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) (q : ENNReal) : MemLp (fun (x : α) => ‖f x‖ ^ q.toReal) (p / q) μ

Alias of MeasureTheory.MemLp.norm_rpow_div.

theorem MeasureTheory.memLp_norm_rpow_iff {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {q : ENNReal} {f : α → E} (hf : AEStronglyMeasurable f μ) (q_zero : q ≠ 0) (q_top : q ≠ ⊤) : MemLp (fun (x : α) => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

@[deprecated MeasureTheory.memLp_norm_rpow_iff (since := "2025-02-21")]

theorem MeasureTheory.memℒp_norm_rpow_iff {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {q : ENNReal} {f : α → E} (hf : AEStronglyMeasurable f μ) (q_zero : q ≠ 0) (q_top : q ≠ ⊤) : MemLp (fun (x : α) => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Alias of MeasureTheory.memLp_norm_rpow_iff.

theorem MeasureTheory.MemLp.norm_rpow {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MemLp (fun (x : α) => ‖f x‖ ^ p.toReal) 1 μ

@[deprecated MeasureTheory.MemLp.norm_rpow (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.norm_rpow {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : MemLp (fun (x : α) => ‖f x‖ ^ p.toReal) 1 μ

Alias of MeasureTheory.MemLp.norm_rpow.

theorem MeasureTheory.AEEqFun.compMeasurePreserving_mem_Lp {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} {g : β →ₘ[μb] E} (hg : g ∈ Lp E p μb) {f : α → β} (hf : MeasurePreserving f μ μb) : g.compMeasurePreserving f hf ∈ Lp E p μ

Composition with a measure preserving function

def MeasureTheory.Lp.compMeasurePreserving {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} (f : α → β) (hf : MeasurePreserving f μ μb) : ↥(Lp E p μb) →+ ↥(Lp E p μ)

Composition of an L^p function with a measure preserving function is an L^p function.

Equations

• MeasureTheory.Lp.compMeasurePreserving f hf = { toFun := fun (g : ↥(MeasureTheory.Lp E p μb)) => ⟨(↑g).compMeasurePreserving f hf, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.Lp.compMeasurePreserving_val {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} {f : α → β} (g : ↥(Lp E p μb)) (hf : MeasurePreserving f μ μb) : ↑((compMeasurePreserving f hf) g) = (↑g).compMeasurePreserving f hf

theorem MeasureTheory.Lp.coeFn_compMeasurePreserving {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} {f : α → β} (g : ↥(Lp E p μb)) (hf : MeasurePreserving f μ μb) : ↑↑((compMeasurePreserving f hf) g) =ᶠ[ae μ] ↑↑g ∘ f

@[simp]

theorem MeasureTheory.Lp.norm_compMeasurePreserving {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} {f : α → β} (g : ↥(Lp E p μb)) (hf : MeasurePreserving f μ μb) : ‖(compMeasurePreserving f hf) g‖ = ‖g‖

theorem MeasureTheory.Lp.isometry_compMeasurePreserving {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} {f : α → β} [Fact (1 ≤ p)] (hf : MeasurePreserving f μ μb) : Isometry ⇑(compMeasurePreserving f hf)

theorem MeasureTheory.Lp.toLp_compMeasurePreserving {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} {f : α → β} {g : β → E} (hg : MemLp g p μb) (hf : MeasurePreserving f μ μb) : (compMeasurePreserving f hf) (MemLp.toLp g hg) = MemLp.toLp (g ∘ f) ⋯

def MeasureTheory.Lp.compMeasurePreservingₗ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} (𝕜 : Type u_7) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : α → β) (hf : MeasurePreserving f μ μb) : ↥(Lp E p μb) →ₗ[𝕜] ↥(Lp E p μ)

MeasureTheory.Lp.compMeasurePreserving as a linear map.

Equations

• MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf = { toFun := (↑(MeasureTheory.Lp.compMeasurePreserving f hf)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MeasureTheory.Lp.compMeasurePreservingₗ_apply {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} (𝕜 : Type u_7) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : α → β) (hf : MeasurePreserving f μ μb) (a✝ : ↥(Lp E p μb)) : (compMeasurePreservingₗ 𝕜 f hf) a✝ = (↑(compMeasurePreserving f hf)).toFun a✝

def MeasureTheory.Lp.compMeasurePreservingₗᵢ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} (𝕜 : Type u_7) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (1 ≤ p)] (f : α → β) (hf : MeasurePreserving f μ μb) : ↥(Lp E p μb) →ₗᵢ[𝕜] ↥(Lp E p μ)

MeasureTheory.Lp.compMeasurePreserving as a linear isometry.

Equations

• MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 f hf = { toLinearMap := MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf, norm_map' := ⋯ }

@[simp]

theorem MeasureTheory.Lp.compMeasurePreservingₗᵢ_apply_coe {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {β : Type u_6} [MeasurableSpace β] {μb : Measure β} (𝕜 : Type u_7) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Fact (1 ≤ p)] (f : α → β) (hf : MeasurePreserving f μ μb) (a✝ : ↥(Lp E p μb)) : ↑((compMeasurePreservingₗᵢ 𝕜 f hf) a✝) = (↑a✝).compMeasurePreserving f hf

Composition on L^p

We show that Lipschitz functions vanishing at zero act by composition on L^p, and specialize this to the composition with continuous linear maps, and to the definition of the positive part of an L^p function.

theorem LipschitzWith.comp_memLp {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K : NNReal} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g) (g0 : g 0 = 0) (hL : MeasureTheory.MemLp f p μ) : MeasureTheory.MemLp (g ∘ f) p μ

@[deprecated LipschitzWith.comp_memLp (since := "2025-02-21")]

theorem LipschitzWith.comp_memℒp {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K : NNReal} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g) (g0 : g 0 = 0) (hL : MeasureTheory.MemLp f p μ) : MeasureTheory.MemLp (g ∘ f) p μ

Alias of LipschitzWith.comp_memLp.

theorem MeasureTheory.MemLp.of_comp_antilipschitzWith {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K' : NNReal} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hL : MemLp (g ∘ f) p μ) (hg : UniformContinuous g) (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) : MemLp f p μ

@[deprecated MeasureTheory.MemLp.of_comp_antilipschitzWith (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.of_comp_antilipschitzWith {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K' : NNReal} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hL : MemLp (g ∘ f) p μ) (hg : UniformContinuous g) (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) : MemLp f p μ

Alias of MeasureTheory.MemLp.of_comp_antilipschitzWith.

theorem LipschitzWith.memLp_comp_iff_of_antilipschitz {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K K' : NNReal} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g) (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) : MeasureTheory.MemLp (g ∘ f) p μ ↔ MeasureTheory.MemLp f p μ

@[deprecated LipschitzWith.memLp_comp_iff_of_antilipschitz (since := "2025-02-21")]

theorem LipschitzWith.memℒp_comp_iff_of_antilipschitz {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K K' : NNReal} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g) (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) : MeasureTheory.MemLp (g ∘ f) p μ ↔ MeasureTheory.MemLp f p μ

Alias of LipschitzWith.memLp_comp_iff_of_antilipschitz.

def LipschitzWith.compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : ↥(MeasureTheory.Lp E p μ)) : ↥(MeasureTheory.Lp F p μ)

When g is a Lipschitz function sending 0 to 0 and f is in Lp, then g ∘ f is well defined as an element of Lp.

Equations

• hg.compLp g0 f = ⟨MeasureTheory.AEEqFun.comp g ⋯ ↑f, ⋯⟩

theorem LipschitzWith.coeFn_compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(hg.compLp g0 f) =ᵐ[μ] g ∘ ↑↑f

@[simp]

theorem LipschitzWith.compLp_zero {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g) (g0 : g 0 = 0) : hg.compLp g0 0 = 0

theorem LipschitzWith.norm_compLp_sub_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g) (g0 : g 0 = 0) (f f' : ↥(MeasureTheory.Lp E p μ)) : ‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ ↑c * ‖f - f'‖

theorem LipschitzWith.norm_compLp_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : ↥(MeasureTheory.Lp E p μ)) : ‖hg.compLp g0 f‖ ≤ ↑c * ‖f‖

theorem LipschitzWith.lipschitzWith_compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} [Fact (1 ≤ p)] (hg : LipschitzWith c g) (g0 : g 0 = 0) : LipschitzWith c (hg.compLp g0)

theorem LipschitzWith.continuous_compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {g : E → F} {c : NNReal} [Fact (1 ≤ p)] (hg : LipschitzWith c g) (g0 : g 0 = 0) : Continuous (hg.compLp g0)

def ContinuousLinearMap.compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : ↥(MeasureTheory.Lp F p μ)

Composing f : Lp with L : E →L[𝕜] F.

Equations

• L.compLp f = ⋯.compLp ⋯ f

theorem ContinuousLinearMap.coeFn_compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : ∀ᵐ (a : α) ∂μ, ↑↑(L.compLp f) a = L (↑↑f a)

theorem ContinuousLinearMap.coeFn_compLp' {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(L.compLp f) =ᵐ[μ] fun (a : α) => L (↑↑f a)

theorem ContinuousLinearMap.comp_memLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : MeasureTheory.MemLp (⇑L ∘ ↑↑f) p μ

@[deprecated ContinuousLinearMap.comp_memLp (since := "2025-02-21")]

theorem ContinuousLinearMap.comp_memℒp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : MeasureTheory.MemLp (⇑L ∘ ↑↑f) p μ

Alias of ContinuousLinearMap.comp_memLp.

theorem ContinuousLinearMap.comp_memLp' {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) {f : α → E} (hf : MeasureTheory.MemLp f p μ) : MeasureTheory.MemLp (⇑L ∘ f) p μ

@[deprecated ContinuousLinearMap.comp_memLp' (since := "2025-02-21")]

theorem ContinuousLinearMap.comp_memℒp' {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) {f : α → E} (hf : MeasureTheory.MemLp f p μ) : MeasureTheory.MemLp (⇑L ∘ f) p μ

Alias of ContinuousLinearMap.comp_memLp'.

theorem MeasureTheory.MemLp.ofReal {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {K : Type u_7} [RCLike K] {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun (x : α) => ↑(f x)) p μ

@[deprecated MeasureTheory.MemLp.ofReal (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.ofReal {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {K : Type u_7} [RCLike K] {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun (x : α) => ↑(f x)) p μ

Alias of MeasureTheory.MemLp.ofReal.

theorem MeasureTheory.memLp_re_im_iff {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {K : Type u_7} [RCLike K] {f : α → K} : MemLp (fun (x : α) => RCLike.re (f x)) p μ ∧ MemLp (fun (x : α) => RCLike.im (f x)) p μ ↔ MemLp f p μ

@[deprecated MeasureTheory.memLp_re_im_iff (since := "2025-02-21")]

theorem MeasureTheory.memℒp_re_im_iff {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {K : Type u_7} [RCLike K] {f : α → K} : MemLp (fun (x : α) => RCLike.re (f x)) p μ ∧ MemLp (fun (x : α) => RCLike.im (f x)) p μ ↔ MemLp f p μ

Alias of MeasureTheory.memLp_re_im_iff.

theorem ContinuousLinearMap.add_compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L L' : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : (L + L').compLp f = L.compLp f + L'.compLp f

theorem ContinuousLinearMap.smul_compLp {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {𝕜' : Type u_7} [NormedRing 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : (c • L).compLp f = c • L.compLp f

theorem ContinuousLinearMap.norm_compLp_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : ‖L.compLp f‖ ≤ ‖L‖ * ‖f‖

def ContinuousLinearMap.compLpₗ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) : ↥(MeasureTheory.Lp E p μ) →ₗ[𝕜] ↥(MeasureTheory.Lp F p μ)

Composing f : Lp E p μ with L : E →L[𝕜] F, seen as a 𝕜-linear map on Lp E p μ.

Equations

• ContinuousLinearMap.compLpₗ p μ L = { toFun := fun (f : ↥(MeasureTheory.Lp E p μ)) => L.compLp f, map_add' := ⋯, map_smul' := ⋯ }

def ContinuousLinearMap.compLpL {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [Fact (1 ≤ p)] (L : E →L[𝕜] F) : ↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp F p μ)

Composing f : Lp E p μ with L : E →L[𝕜] F, seen as a continuous 𝕜-linear map on Lp E p μ. See also the similar

• LinearMap.compLeft for functions,
• ContinuousLinearMap.compLeftContinuous for continuous functions,
• ContinuousLinearMap.compLeftContinuousBounded for bounded continuous functions,
• ContinuousLinearMap.compLeftContinuousCompact for continuous functions on compact spaces.

Equations

• ContinuousLinearMap.compLpL p μ L = (ContinuousLinearMap.compLpₗ p μ L).mkContinuous ‖L‖ ⋯

theorem ContinuousLinearMap.coeFn_compLpL {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [Fact (1 ≤ p)] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑((compLpL p μ L) f) =ᵐ[μ] fun (a : α) => L (↑↑f a)

theorem ContinuousLinearMap.add_compLpL {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [Fact (1 ≤ p)] (L L' : E →L[𝕜] F) : compLpL p μ (L + L') = compLpL p μ L + compLpL p μ L'

theorem ContinuousLinearMap.smul_compLpL {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [Fact (1 ≤ p)] {𝕜' : Type u_7} [NormedRing 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) : compLpL p μ (c • L) = c • compLpL p μ L

theorem ContinuousLinearMap.norm_compLpL_le {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_6} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [Fact (1 ≤ p)] (L : E →L[𝕜] F) : ‖compLpL p μ L‖ ≤ ‖L‖

theorem MeasureTheory.Lp.lipschitzWith_pos_part : LipschitzWith 1 fun (x : ℝ) => x ⊔ 0

theorem MeasureTheory.MemLp.pos_part {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun (x : α) => f x ⊔ 0) p μ

@[deprecated MeasureTheory.MemLp.pos_part (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.pos_part {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun (x : α) => f x ⊔ 0) p μ

Alias of MeasureTheory.MemLp.pos_part.

theorem MeasureTheory.MemLp.neg_part {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun (x : α) => -f x ⊔ 0) p μ

@[deprecated MeasureTheory.MemLp.neg_part (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.neg_part {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun (x : α) => -f x ⊔ 0) p μ

Alias of MeasureTheory.MemLp.neg_part.

def MeasureTheory.Lp.posPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} (f : ↥(Lp ℝ p μ)) : ↥(Lp ℝ p μ)

Positive part of a function in L^p.

Equations

• MeasureTheory.Lp.posPart f = MeasureTheory.Lp.lipschitzWith_pos_part.compLp MeasureTheory.Lp.posPart._proof_45 f

def MeasureTheory.Lp.negPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} (f : ↥(Lp ℝ p μ)) : ↥(Lp ℝ p μ)

Negative part of a function in L^p.

Equations

• MeasureTheory.Lp.negPart f = MeasureTheory.Lp.posPart (-f)

theorem MeasureTheory.Lp.coe_posPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} (f : ↥(Lp ℝ p μ)) : ↑(posPart f) = (↑f).posPart

theorem MeasureTheory.Lp.coeFn_posPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} (f : ↥(Lp ℝ p μ)) : ↑↑(posPart f) =ᶠ[ae μ] fun (a : α) => ↑↑f a ⊔ 0

theorem MeasureTheory.Lp.coeFn_negPart_eq_max {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} (f : ↥(Lp ℝ p μ)) : ∀ᵐ (a : α) ∂μ, ↑↑(negPart f) a = -↑↑f a ⊔ 0

theorem MeasureTheory.Lp.coeFn_negPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} (f : ↥(Lp ℝ p μ)) : ∀ᵐ (a : α) ∂μ, ↑↑(negPart f) a = -(↑↑f a ⊓ 0)

theorem MeasureTheory.Lp.continuous_posPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] : Continuous fun (f : ↥(Lp ℝ p μ)) => posPart f

theorem MeasureTheory.Lp.continuous_negPart {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [Fact (1 ≤ p)] : Continuous fun (f : ↥(Lp ℝ p μ)) => negPart f

theorem MeasureTheory.Lp.pow_mul_meas_ge_le_enorm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (ε : ENNReal) : (ε * μ {x : α | ε ≤ ‖↑↑f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ ENNReal.ofReal ‖f‖

A version of Markov's inequality with elements of Lp.

theorem MeasureTheory.Lp.mul_meas_ge_le_pow_enorm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (ε : ENNReal) : ε * μ {x : α | ε ≤ ‖↑↑f x‖ₑ ^ p.toReal} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal

A version of Markov's inequality with elements of Lp.

theorem MeasureTheory.Lp.mul_meas_ge_le_pow_enorm' {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (ε : ENNReal) : ε ^ p.toReal * μ {x : α | ε ≤ ↑‖↑↑f x‖₊} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal

A version of Markov's inequality with elements of Lp.

theorem MeasureTheory.Lp.meas_ge_le_mul_pow_enorm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ↑‖↑↑f x‖₊} ≤ ε⁻¹ ^ p.toReal * ENNReal.ofReal ‖f‖ ^ p.toReal

A version of Markov's inequality with elements of Lp.

@[deprecated MeasureTheory.Lp.pow_mul_meas_ge_le_enorm (since := "2025-01-20")]

theorem MeasureTheory.Lp.pow_mul_meas_ge_le_norm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (ε : ENNReal) : (ε * μ {x : α | ε ≤ ‖↑↑f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ ENNReal.ofReal ‖f‖

Alias of MeasureTheory.Lp.pow_mul_meas_ge_le_enorm.

---

A version of Markov's inequality with elements of Lp.

@[deprecated MeasureTheory.Lp.mul_meas_ge_le_pow_enorm (since := "2025-01-20")]

theorem MeasureTheory.Lp.mul_meas_ge_le_pow_norm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (ε : ENNReal) : ε * μ {x : α | ε ≤ ‖↑↑f x‖ₑ ^ p.toReal} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal

Alias of MeasureTheory.Lp.mul_meas_ge_le_pow_enorm.

---

A version of Markov's inequality with elements of Lp.

@[deprecated MeasureTheory.Lp.mul_meas_ge_le_pow_enorm' (since := "2025-01-20")]

theorem MeasureTheory.Lp.mul_meas_ge_le_pow_norm' {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) (ε : ENNReal) : ε ^ p.toReal * μ {x : α | ε ≤ ↑‖↑↑f x‖₊} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal

Alias of MeasureTheory.Lp.mul_meas_ge_le_pow_enorm'.

---

A version of Markov's inequality with elements of Lp.

@[deprecated MeasureTheory.Lp.meas_ge_le_mul_pow_enorm (since := "2025-01-20")]

theorem MeasureTheory.Lp.meas_ge_le_mul_pow_norm {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] (f : ↥(Lp E p μ)) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : μ {x : α | ε ≤ ↑‖↑↑f x‖₊} ≤ ε⁻¹ ^ p.toReal * ENNReal.ofReal ‖f‖ ^ p.toReal

Alias of MeasureTheory.Lp.meas_ge_le_mul_pow_enorm.

---

A version of Markov's inequality with elements of Lp.