Lp space

This file provides the space Lp E p μ as the subtype of elements of α →ₘ[μ] E (see ae_eq_fun) such that eLpNorm f p μ is finite. For 1 ≤ p, eLpNorm defines a norm and Lp is a complete metric space.

Main definitions

• Lp E p μ : elements of α →ₘ[μ] E (see ae_eq_fun) 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.

When α is a topological space equipped with a finite Borel measure, there is a bounded linear map from the normed space of bounded continuous functions (α →ᵇ E) to Lp E p μ. We construct this as BoundedContinuousFunction.toLp.

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_5} {E : Type u_6} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {f : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm (↑(MeasureTheory.AEEqFun.mk f hf)) p μ = MeasureTheory.eLpNorm f p μ

@[deprecated MeasureTheory.eLpNorm_aeeqFun]

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

Alias of MeasureTheory.eLpNorm_aeeqFun.

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

@[deprecated MeasureTheory.Memℒp.eLpNorm_mk_lt_top]

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

Alias of MeasureTheory.Memℒp.eLpNorm_mk_lt_top.

def MeasureTheory.Lp {α : Type u_6} (E : Type u_5) {m : MeasurableSpace α} [NormedAddCommGroup E] (p : ENNReal) (μ : MeasureTheory.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

Equations

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

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

Equations

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

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

make an element of Lp from a function verifying Memℒp

Equations

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

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

theorem MeasureTheory.Memℒp.coeFn_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.Memℒp f p μ) : ↑↑(MeasureTheory.Memℒp.toLp f hf) =ᵐ[μ] f

theorem MeasureTheory.Memℒp.toLp_congr {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f g : α → E} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ) (hfg : f =ᵐ[μ] g) : MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp g hg

@[simp]

theorem MeasureTheory.Memℒp.toLp_eq_toLp_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f g : α → E} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ) : MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp g hg ↔ f =ᵐ[μ] g

@[simp]

theorem MeasureTheory.Memℒp.toLp_zero {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (h : MeasureTheory.Memℒp 0 p μ) : MeasureTheory.Memℒp.toLp 0 h = 0

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

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

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

instance MeasureTheory.Lp.instCoeFun {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : CoeFun ↥(MeasureTheory.Lp E p μ) fun (x : ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f g : ↥(MeasureTheory.Lp E p μ)} (h : ↑↑f =ᵐ[μ] ↑↑g) : f = g

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

@[deprecated MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top]

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

Alias of MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top.

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

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

@[simp]

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

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

@[simp]

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

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

@[deprecated MeasureTheory.Lp.eLpNorm_lt_top]

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

Alias of MeasureTheory.Lp.eLpNorm_lt_top.

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

@[deprecated MeasureTheory.Lp.eLpNorm_ne_top]

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

Alias of MeasureTheory.Lp.eLpNorm_ne_top.

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

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

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

theorem MeasureTheory.Lp.coeFn_zero {α : Type u_1} (E : Type u_2) {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] : ↑↑0 =ᵐ[μ] 0

theorem MeasureTheory.Lp.coeFn_neg {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(-f) =ᵐ[μ] -↑↑f

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

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

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

instance MeasureTheory.Lp.instNorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : Norm ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : NNNorm ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : Dist ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] : EDist ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)) : ‖f‖ = (MeasureTheory.eLpNorm (↑↑f) p μ).toReal

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem MeasureTheory.Lp.coe_nnnorm_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.Memℒp f p μ) : ↑‖MeasureTheory.Memℒp.toLp f hf‖₊ = MeasureTheory.eLpNorm f p μ

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem MeasureTheory.Lp.norm_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : ↥(MeasureTheory.Lp E p μ)} : f = 0 ↔ ↑↑f =ᵐ[μ] 0

@[simp]

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

@[simp]

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

theorem MeasureTheory.Lp.nnnorm_le_mul_nnnorm_of_ae_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : NNReal} {f : ↥(MeasureTheory.Lp E p μ)} {g : ↥(MeasureTheory.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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : ℝ} {f : ↥(MeasureTheory.Lp E p μ)} {g : ↥(MeasureTheory.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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : ↥(MeasureTheory.Lp E p μ)} {g : ↥(MeasureTheory.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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {c : NNReal} {f : α →ₘ[μ] E} {g : ↥(MeasureTheory.Lp F p μ)} (h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ c * ‖↑↑g x‖₊) : f ∈ MeasureTheory.Lp E p μ

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

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

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

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

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

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

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

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

Equations

• MeasureTheory.Lp.instNormedAddCommGroup = NormedAddCommGroup.mk ⋯

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

def MeasureTheory.Lp.LpSubmodule {α : Type u_1} (E : Type u_2) {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] (𝕜 : Type u_5) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 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} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : (MeasureTheory.Lp.LpSubmodule E p μ 𝕜).toAddSubgroup = MeasureTheory.Lp E p μ

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

Equations

• MeasureTheory.Lp.instModule = Module.mk ⋯ ⋯

theorem MeasureTheory.Lp.coeFn_smul {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (c : 𝕜) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑(c • f) =ᵐ[μ] c • ↑↑f

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

instance MeasureTheory.Lp.instSMulCommClass {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} {𝕜' : Type u_6} [NormedRing 𝕜] [NormedRing 𝕜'] [Module 𝕜 E] [Module 𝕜' E] [BoundedSMul 𝕜 E] [BoundedSMul 𝕜' E] [SMulCommClass 𝕜 𝕜' E] : SMulCommClass 𝕜 𝕜' ↥(MeasureTheory.Lp E p μ)

instance MeasureTheory.Lp.instIsScalarTower {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} {𝕜' : Type u_6} [NormedRing 𝕜] [NormedRing 𝕜'] [Module 𝕜 E] [Module 𝕜' E] [BoundedSMul 𝕜 E] [BoundedSMul 𝕜' E] [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower 𝕜 𝕜' ↥(MeasureTheory.Lp E p μ)

instance MeasureTheory.Lp.instBoundedSMul {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] [Fact (1 ≤ p)] : BoundedSMul 𝕜 ↥(MeasureTheory.Lp E p μ)

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

Equations

• MeasureTheory.Lp.instNormedSpace = NormedSpace.mk ⋯

theorem MeasureTheory.Memℒp.toLp_const_smul {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] {f : α → E} (c : 𝕜) (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp.toLp (c • f) ⋯ = c • MeasureTheory.Memℒp.toLp f hf

Indicator of a set as an element of Lᵖ

For a set s with (hs : MeasurableSet s) and (hμs : μ s < ∞), we build indicatorConstLp p hs hμs c, the element of Lp corresponding to s.indicator (fun _ => c).

theorem MeasureTheory.eLpNormEssSup_indicator_le {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (f : α → G) : MeasureTheory.eLpNormEssSup (s.indicator f) μ ≤ MeasureTheory.eLpNormEssSup f μ

@[deprecated MeasureTheory.eLpNormEssSup_indicator_le]

theorem MeasureTheory.snormEssSup_indicator_le {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (f : α → G) : MeasureTheory.eLpNormEssSup (s.indicator f) μ ≤ MeasureTheory.eLpNormEssSup f μ

Alias of MeasureTheory.eLpNormEssSup_indicator_le.

theorem MeasureTheory.eLpNormEssSup_indicator_const_le {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) : MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ ≤ ↑‖c‖₊

@[deprecated MeasureTheory.eLpNormEssSup_indicator_const_le]

theorem MeasureTheory.snormEssSup_indicator_const_le {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) : MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ ≤ ↑‖c‖₊

Alias of MeasureTheory.eLpNormEssSup_indicator_const_le.

theorem MeasureTheory.eLpNormEssSup_indicator_const_eq {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) (hμs : μ s ≠ 0) : MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ = ↑‖c‖₊

@[deprecated MeasureTheory.eLpNormEssSup_indicator_const_eq]

theorem MeasureTheory.snormEssSup_indicator_const_eq {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] (s : Set α) (c : G) (hμs : μ s ≠ 0) : MeasureTheory.eLpNormEssSup (s.indicator fun (x : α) => c) μ = ↑‖c‖₊

Alias of MeasureTheory.eLpNormEssSup_indicator_const_eq.

theorem MeasureTheory.eLpNorm_indicator_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (f : α → E) : MeasureTheory.eLpNorm (s.indicator f) p μ ≤ MeasureTheory.eLpNorm f p μ

@[deprecated MeasureTheory.eLpNorm_indicator_le]

theorem MeasureTheory.snorm_indicator_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (f : α → E) : MeasureTheory.eLpNorm (s.indicator f) p μ ≤ MeasureTheory.eLpNorm f p μ

Alias of MeasureTheory.eLpNorm_indicator_le.

theorem MeasureTheory.eLpNorm_indicator_const₀ {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} {c : G} (hs : MeasureTheory.NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)

@[deprecated MeasureTheory.eLpNorm_indicator_const₀]

theorem MeasureTheory.snorm_indicator_const₀ {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} {c : G} (hs : MeasureTheory.NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)

Alias of MeasureTheory.eLpNorm_indicator_const₀.

theorem MeasureTheory.eLpNorm_indicator_const {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} {c : G} (hs : MeasurableSet s) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)

@[deprecated MeasureTheory.eLpNorm_indicator_const]

theorem MeasureTheory.snorm_indicator_const {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} {c : G} (hs : MeasurableSet s) (hp : p ≠ 0) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)

Alias of MeasureTheory.eLpNorm_indicator_const.

theorem MeasureTheory.eLpNorm_indicator_const' {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} {c : G} (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)

@[deprecated MeasureTheory.eLpNorm_indicator_const']

theorem MeasureTheory.snorm_indicator_const' {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} {c : G} (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)

Alias of MeasureTheory.eLpNorm_indicator_const'.

theorem MeasureTheory.eLpNorm_indicator_const_le {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} (c : G) (p : ENNReal) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)

@[deprecated MeasureTheory.eLpNorm_indicator_const_le]

theorem MeasureTheory.snorm_indicator_const_le {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {s : Set α} (c : G) (p : ENNReal) : MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)

Alias of MeasureTheory.eLpNorm_indicator_const_le.

theorem MeasureTheory.Memℒp.indicator {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {s : Set α} (hs : MeasurableSet s) (hf : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (s.indicator f) p μ

theorem MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {s : Set α} {f : α → F} (hs : MeasurableSet s) : MeasureTheory.eLpNormEssSup (s.indicator f) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s)

@[deprecated MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict]

theorem MeasureTheory.snormEssSup_indicator_eq_snormEssSup_restrict {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {s : Set α} {f : α → F} (hs : MeasurableSet s) : MeasureTheory.eLpNormEssSup (s.indicator f) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s)

Alias of MeasureTheory.eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict.

theorem MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {s : Set α} {f : α → F} (hs : MeasurableSet s) : MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)

@[deprecated MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict]

theorem MeasureTheory.snorm_indicator_eq_snorm_restrict {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {s : Set α} {f : α → F} (hs : MeasurableSet s) : MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)

Alias of MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict.

theorem MeasureTheory.memℒp_indicator_iff_restrict {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.Memℒp (s.indicator f) p μ ↔ MeasureTheory.Memℒp f p (μ.restrict s)

theorem MeasureTheory.Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p q : ENNReal} {f : α → E} (hfq : MeasureTheory.Memℒp f q μ) {s : Set α} (hf : ∀ x ∉ s, f x = 0) (hs : μ s ≠ ⊤) (hpq : p ≤ q) : MeasureTheory.Memℒp f p μ

If a function is supported on a finite-measure set and belongs to ℒ^p, then it belongs to ℒ^q for any q ≤ p.

theorem MeasureTheory.memℒp_indicator_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ⊤) : MeasureTheory.Memℒp (s.indicator fun (x : α) => c) p μ

theorem MeasureTheory.exists_eLpNorm_indicator_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hp : p ≠ ⊤) (c : E) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (η : NNReal), 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ε

The ℒ^p norm of the indicator of a set is uniformly small if the set itself has small measure, for any p < ∞. Given here as an existential ∀ ε > 0, ∃ η > 0, ... to avoid later management of ℝ≥0∞-arithmetic.

@[deprecated MeasureTheory.exists_eLpNorm_indicator_le]

theorem MeasureTheory.exists_snorm_indicator_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hp : p ≠ ⊤) (c : E) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (η : NNReal), 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → MeasureTheory.eLpNorm (s.indicator fun (x : α) => c) p μ ≤ ε

Alias of MeasureTheory.exists_eLpNorm_indicator_le.

---

The ℒ^p norm of the indicator of a set is uniformly small if the set itself has small measure, for any p < ∞. Given here as an existential ∀ ε > 0, ∃ η > 0, ... to avoid later management of ℝ≥0∞-arithmetic.

theorem MeasureTheory.Memℒp.piecewise {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {g : α → E} (hs : MeasurableSet s) (hf : MeasureTheory.Memℒp f p (μ.restrict s)) (hg : MeasureTheory.Memℒp g p (μ.restrict sᶜ)) : MeasureTheory.Memℒp (s.piecewise f g) p μ

theorem HasCompactSupport.memℒp_of_bound {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_5} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E} (hf : HasCompactSupport f) (h2f : MeasureTheory.AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) : MeasureTheory.Memℒp f p μ

A bounded measurable function with compact support is in L^p.

theorem Continuous.memℒp_of_hasCompactSupport {E : Type u_2} {p : ENNReal} [NormedAddCommGroup E] {X : Type u_5} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X] {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) : MeasureTheory.Memℒp f p μ

A continuous function with compact support is in L^p.

def MeasureTheory.indicatorConstLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} (p : ENNReal) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E) : ↥(MeasureTheory.Lp E p μ)

Indicator of a set as an element of Lp.

Equations

• MeasureTheory.indicatorConstLp p hs hμs c = MeasureTheory.Memℒp.toLp (s.indicator fun (x : α) => c) ⋯

theorem MeasureTheory.indicatorConstLp_add {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c c' : E} : MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p hs hμs c' = MeasureTheory.indicatorConstLp p hs hμs (c + c')

A version of Set.indicator_add for MeasureTheory.indicatorConstLp.

theorem MeasureTheory.indicatorConstLp_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c c' : E} : MeasureTheory.indicatorConstLp p hs hμs c - MeasureTheory.indicatorConstLp p hs hμs c' = MeasureTheory.indicatorConstLp p hs hμs (c - c')

A version of Set.indicator_sub for MeasureTheory.indicatorConstLp.

theorem MeasureTheory.indicatorConstLp_coeFn {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) =ᵐ[μ] s.indicator fun (x : α) => c

theorem MeasureTheory.indicatorConstLp_coeFn_mem {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = c

theorem MeasureTheory.indicatorConstLp_coeFn_nmem {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = 0

theorem MeasureTheory.norm_indicatorConstLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : ‖MeasureTheory.indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

theorem MeasureTheory.norm_indicatorConstLp_top {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} (hμs_ne_zero : μ s ≠ 0) : ‖MeasureTheory.indicatorConstLp ⊤ hs hμs c‖ = ‖c‖

theorem MeasureTheory.norm_indicatorConstLp' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} (hp_pos : p ≠ 0) (hμs_pos : μ s ≠ 0) : ‖MeasureTheory.indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

theorem MeasureTheory.norm_indicatorConstLp_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ‖MeasureTheory.indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

theorem MeasureTheory.nnnorm_indicatorConstLp_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ‖MeasureTheory.indicatorConstLp p hs hμs c‖₊ ≤ ‖c‖₊ * (μ s).toNNReal ^ (1 / p.toReal)

theorem MeasureTheory.ennnorm_indicatorConstLp_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} : ↑‖MeasureTheory.indicatorConstLp p hs hμs c‖₊ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)

theorem MeasureTheory.edist_indicatorConstLp_eq_nnnorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ⊤} : edist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) = ↑‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖₊

theorem MeasureTheory.dist_indicatorConstLp_eq_norm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ⊤} : dist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) = ‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖

theorem MeasureTheory.tendsto_indicatorConstLp_set {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} [hp₁ : Fact (1 ≤ p)] {β : Type u_5} {l : Filter β} {t : β → Set α} {ht : ∀ (b : β), MeasurableSet (t b)} {hμt : ∀ (b : β), μ (t b) ≠ ⊤} (hp : p ≠ ⊤) (h : Filter.Tendsto (fun (b : β) => μ (symmDiff (t b) s)) l (nhds 0)) : Filter.Tendsto (fun (b : β) => MeasureTheory.indicatorConstLp p ⋯ ⋯ c) l (nhds (MeasureTheory.indicatorConstLp p hs hμs c))

A family of indicatorConstLp functions tends to an indicatorConstLp, if the underlying sets tend to the set in the sense of the measure of the symmetric difference.

theorem MeasureTheory.continuous_indicatorConstLp_set {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {c : E} [Fact (1 ≤ p)] {X : Type u_5} [TopologicalSpace X] {s : X → Set α} {hs : ∀ (x : X), MeasurableSet (s x)} {hμs : ∀ (x : X), μ (s x) ≠ ⊤} (hp : p ≠ ⊤) (h : ∀ (x : X), Filter.Tendsto (fun (y : X) => μ (symmDiff (s y) (s x))) (nhds x) (nhds 0)) : Continuous fun (x : X) => MeasureTheory.indicatorConstLp p ⋯ ⋯ c

A family of indicatorConstLp functions is continuous in the parameter, if μ (s y ∆ s x) tends to zero as y tends to x for all x.

@[simp]

theorem MeasureTheory.indicatorConstLp_empty {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {c : E} : MeasureTheory.indicatorConstLp p ⋯ ⋯ c = 0

theorem MeasureTheory.indicatorConstLp_inj {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (hsμ : μ s ≠ ⊤) (ht : MeasurableSet t) (htμ : μ t ≠ ⊤) {c : E} (hc : c ≠ 0) : MeasureTheory.indicatorConstLp p hs hsμ c = MeasureTheory.indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t

theorem MeasureTheory.memℒp_add_of_disjoint {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f g : α → E} (h : Disjoint (Function.support f) (Function.support g)) (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g) : MeasureTheory.Memℒp (f + g) p μ ↔ MeasureTheory.Memℒp f p μ ∧ MeasureTheory.Memℒp g p μ

theorem MeasureTheory.indicatorConstLp_disjoint_union {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤) (hst : Disjoint s t) (c : E) : MeasureTheory.indicatorConstLp p ⋯ ⋯ c = MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p ht hμt c

The indicator of a disjoint union of two sets is the sum of the indicators of the sets.

def MeasureTheory.Lp.const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] : E →+ ↥(MeasureTheory.Lp E p μ)

Constant function as an element of MeasureTheory.Lp for a finite measure.

Equations

• MeasureTheory.Lp.const p μ = { toFun := fun (c : E) => ⟨MeasureTheory.AEEqFun.const α c, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem MeasureTheory.Lp.coeFn_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) : ↑↑((MeasureTheory.Lp.const p μ) c) =ᵐ[μ] Function.const α c

@[simp]

theorem MeasureTheory.Lp.const_val {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) : ↑((MeasureTheory.Lp.const p μ) c) = MeasureTheory.AEEqFun.const α c

@[simp]

theorem MeasureTheory.Memℒp.toLp_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) : MeasureTheory.Memℒp.toLp (fun (x : α) => c) ⋯ = (MeasureTheory.Lp.const p μ) c

@[simp]

theorem MeasureTheory.indicatorConstLp_univ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) : MeasureTheory.indicatorConstLp p ⋯ ⋯ c = (MeasureTheory.Lp.const p μ) c

theorem MeasureTheory.Lp.norm_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) [NeZero μ] (hp_zero : p ≠ 0) : ‖(MeasureTheory.Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

theorem MeasureTheory.Lp.norm_const' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤) : ‖(MeasureTheory.Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

theorem MeasureTheory.Lp.norm_const_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (c : E) : ‖(MeasureTheory.Lp.const p μ) c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

def MeasureTheory.Lp.constₗ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] : E →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ)

MeasureTheory.Lp.const as a LinearMap.

Equations

• MeasureTheory.Lp.constₗ p μ 𝕜 = { toFun := ⇑(MeasureTheory.Lp.const p μ), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MeasureTheory.Lp.constₗ_apply {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (a : E) : (MeasureTheory.Lp.constₗ p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a

def MeasureTheory.Lp.constL {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] : E →L[𝕜] ↥(MeasureTheory.Lp E p μ)

Equations

• MeasureTheory.Lp.constL p μ 𝕜 = (MeasureTheory.Lp.constₗ p μ 𝕜).mkContinuous ((μ Set.univ).toReal ^ (1 / p.toReal)) ⋯

@[simp]

theorem MeasureTheory.Lp.constL_apply {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] (a : E) : (MeasureTheory.Lp.constL p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a

theorem MeasureTheory.Lp.norm_constL_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Fact (1 ≤ p)] : ‖MeasureTheory.Lp.constL p μ 𝕜‖ ≤ (μ Set.univ).toReal ^ (1 / p.toReal)

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

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

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

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

Composition with a measure preserving function

def MeasureTheory.Lp.compMeasurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} (f : α → β) (hf : MeasureTheory.MeasurePreserving f μ μb) : ↥(MeasureTheory.Lp E p μb) →+ ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β} (g : ↥(MeasureTheory.Lp E p μb)) (hf : MeasureTheory.MeasurePreserving f μ μb) : ↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) = (↑g).compMeasurePreserving f hf

theorem MeasureTheory.Lp.coeFn_compMeasurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β} (g : ↥(MeasureTheory.Lp E p μb)) (hf : MeasureTheory.MeasurePreserving f μ μb) : ↑↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) =ᵐ[μ] ↑↑g ∘ f

@[simp]

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

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

theorem MeasureTheory.Lp.toLp_compMeasurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β} {g : β → E} (hg : MeasureTheory.Memℒp g p μb) (hf : MeasureTheory.MeasurePreserving f μ μb) : (MeasureTheory.Lp.compMeasurePreserving f hf) (MeasureTheory.Memℒp.toLp g hg) = MeasureTheory.Memℒp.toLp (g ∘ f) ⋯

theorem MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} {f : α → β} {s : Set β} (hs : MeasurableSet s) (hμs : μb s ≠ ⊤) (c : E) (hf : MeasureTheory.MeasurePreserving f μ μb) : (MeasureTheory.Lp.compMeasurePreserving f hf) (MeasureTheory.indicatorConstLp p hs hμs c) = MeasureTheory.indicatorConstLp p ⋯ ⋯ c

def MeasureTheory.Lp.compMeasurePreservingₗ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} (𝕜 : Type u_6) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : α → β) (hf : MeasureTheory.MeasurePreserving f μ μb) : ↥(MeasureTheory.Lp E p μb) →ₗ[𝕜] ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} (𝕜 : Type u_6) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : α → β) (hf : MeasureTheory.MeasurePreserving f μ μb) (a✝ : ↥(MeasureTheory.Lp E p μb)) : (MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf) a✝ = (↑(MeasureTheory.Lp.compMeasurePreserving f hf)).toFun a✝

def MeasureTheory.Lp.compMeasurePreservingₗᵢ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} (𝕜 : Type u_6) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] [Fact (1 ≤ p)] (f : α → β) (hf : MeasureTheory.MeasurePreserving f μ μb) : ↥(MeasureTheory.Lp E p μb) →ₗᵢ[𝕜] ↥(MeasureTheory.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_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} [MeasurableSpace β] {μb : MeasureTheory.Measure β} (𝕜 : Type u_6) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E] [Fact (1 ≤ p)] (f : α → β) (hf : MeasureTheory.MeasurePreserving f μ μb) (a✝ : ↥(MeasureTheory.Lp E p μb)) : ↑((MeasureTheory.Lp.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_memℒp {p : ENNReal} {α : Type u_5} {E : Type u_6} {F : Type u_7} {K : NNReal} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g) (g0 : g 0 = 0) (hL : MeasureTheory.Memℒp f p μ) : MeasureTheory.Memℒp (g ∘ f) p μ

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

theorem LipschitzWith.memℒp_comp_iff_of_antilipschitz {p : ENNReal} {α : Type u_5} {E : Type u_6} {F : Type u_7} {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.Memℒp (g ∘ f) p μ ↔ MeasureTheory.Memℒp f p μ

def LipschitzWith.compLp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : 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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_memℒp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : MeasureTheory.Memℒp (⇑L ∘ ↑↑f) p μ

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

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

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

theorem ContinuousLinearMap.add_compLp {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {𝕜' : Type u_6} [NormedRing 𝕜'] [Module 𝕜' F] [BoundedSMul 𝕜' 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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_2} {F : Type u_3} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_2} {F : Type u_3} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [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_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [Fact (1 ≤ p)] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)) : ↑↑((ContinuousLinearMap.compLpL p μ L) f) =ᵐ[μ] fun (a : α) => L (↑↑f a)

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

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

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

theorem MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {s : Set α} [NormedSpace ℝ F] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : F) : MeasureTheory.indicatorConstLp 2 hs hμs x = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (MeasureTheory.indicatorConstLp 2 hs hμs 1)

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

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

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

def MeasureTheory.Lp.posPart {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)) : ↥(MeasureTheory.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_2 f

def MeasureTheory.Lp.negPart {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)) : ↥(MeasureTheory.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} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)) : ↑(MeasureTheory.Lp.posPart f) = (↑f).posPart

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

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

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

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

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

L^p is a complete space

We show that L^p is a complete space for 1 ≤ p.

theorem MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {ι : Type u_5} [Nonempty ι] [LinearOrder ι] {f : ι → α → G} {p : ℝ} (hp_nonneg : 0 ≤ p) {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun (m : ι) => ↑‖f m a‖₊ ^ p) Filter.atTop ∂μ) ^ (1 / p)

@[deprecated MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf]

theorem MeasureTheory.Lp.snorm'_lim_eq_lintegral_liminf {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {ι : Type u_5} [Nonempty ι] [LinearOrder ι] {f : ι → α → G} {p : ℝ} (hp_nonneg : 0 ≤ p) {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun (m : ι) => ↑‖f m a‖₊ ^ p) Filter.atTop ∂μ) ^ (1 / p)

Alias of MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf.

theorem MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {f : ℕ → α → E} {p : ℝ} (hp_pos : 0 < p) (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm' f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => MeasureTheory.eLpNorm' (f n) p μ) Filter.atTop

@[deprecated MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm']

theorem MeasureTheory.Lp.snorm'_lim_le_liminf_snorm' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {f : ℕ → α → E} {p : ℝ} (hp_pos : 0 < p) (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm' f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => MeasureTheory.eLpNorm' (f n) p μ) Filter.atTop

Alias of MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm'.

theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {ι : Type u_5} [Nonempty ι] [LinearOrder ι] {f : ι → α → G} {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim ⊤ μ = essSup (fun (x : α) => Filter.liminf (fun (m : ι) => ↑‖f m x‖₊) Filter.atTop) μ

@[deprecated MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf]

theorem MeasureTheory.Lp.snorm_exponent_top_lim_eq_essSup_liminf {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup G] {ι : Type u_5} [Nonempty ι] [LinearOrder ι] {f : ι → α → G} {f_lim : α → G} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim ⊤ μ = essSup (fun (x : α) => Filter.liminf (fun (m : ι) => ↑‖f m x‖₊) Filter.atTop) μ

Alias of MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf.

theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {ι : Type u_5} [Nonempty ι] [Countable ι] [LinearOrder ι] {f : ι → α → F} {f_lim : α → F} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim ⊤ μ ≤ Filter.liminf (fun (n : ι) => MeasureTheory.eLpNorm (f n) ⊤ μ) Filter.atTop

@[deprecated MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top]

theorem MeasureTheory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {ι : Type u_5} [Nonempty ι] [Countable ι] [LinearOrder ι] {f : ι → α → F} {f_lim : α → F} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim ⊤ μ ≤ Filter.liminf (fun (n : ι) => MeasureTheory.eLpNorm (f n) ⊤ μ) Filter.atTop

Alias of MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top.

theorem MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (f_lim : α → E) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop

@[deprecated MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm]

theorem MeasureTheory.Lp.snorm_lim_le_liminf_snorm {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (f_lim : α → E) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop

Alias of MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm.

Lp is complete iff Cauchy sequences of ℒp have limits in ℒp

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_5} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → ↥(MeasureTheory.Lp E p μ)) (f_lim : ↥(MeasureTheory.Lp E p μ)) : Filter.Tendsto f fi (nhds f_lim) ↔ Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (nhds 0)

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_5} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → ↥(MeasureTheory.Lp E p μ)) (f_lim : α → E) (f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ) : Filter.Tendsto f fi (nhds (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (↑↑(f n) - f_lim) p μ) fi (nhds 0)

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_ℒp'' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_5} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → α → E) (f_ℒp : ∀ (n : ι), MeasureTheory.Memℒp (f n) p μ) (f_lim : α → E) (f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ) : Filter.Tendsto (fun (n : ι) => MeasureTheory.Memℒp.toLp (f n) ⋯) fi (nhds (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - f_lim) p μ) fi (nhds 0)

theorem MeasureTheory.Lp.tendsto_Lp_of_tendsto_ℒp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_5} {fi : Filter ι} [Fact (1 ≤ p)] {f : ι → ↥(MeasureTheory.Lp E p μ)} (f_lim : α → E) (f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ) (h_tendsto : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (↑↑(f n) - f_lim) p μ) fi (nhds 0)) : Filter.Tendsto f fi (nhds (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp))

theorem MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_ℒp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {ι : Type u_5} [Nonempty ι] [SemilatticeSup ι] [hp : Fact (1 ≤ p)] (f : ι → ↥(MeasureTheory.Lp E p μ)) : CauchySeq f ↔ Filter.Tendsto (fun (n : ι × ι) => MeasureTheory.eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) Filter.atTop (nhds 0)

theorem MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [hp : Fact (1 ≤ p)] (H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) → ∀ (B : ℕ → ENNReal), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N) → ∃ (f_lim : α → E), MeasureTheory.Memℒp f_lim p μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)) : CompleteSpace ↥(MeasureTheory.Lp E p μ)

Prove that controlled Cauchy sequences of ℒp have limits in ℒp

@[deprecated _private.Mathlib.MeasureTheory.Function.LpSpace.0.MeasureTheory.Lp.eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm']

theorem MeasureTheory.Lp.snorm'_sum_norm_sub_le_tsum_of_cauchy_snorm' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) {p : ℝ} (hp1 : 1 ≤ p) {B : ℕ → ENNReal} (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm' (f n - f m) p μ < B N) (n : ℕ) : MeasureTheory.eLpNorm' (fun (x : α) => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i

Alias of _private.Mathlib.MeasureTheory.Function.LpSpace.0.MeasureTheory.Lp.eLpNorm'_sum_norm_sub_le_tsum_of_cauchy_eLpNorm'.

theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} {p : ℝ} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hp1 : 1 ≤ p) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm' (f n - f m) p μ < B N) : ∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)

@[deprecated MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm']

theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} {p : ℝ} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hp1 : 1 ≤ p) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm' (f n - f m) p μ < B N) : ∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)

Alias of MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm'.

theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hp : 1 ≤ p) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N) : ∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)

@[deprecated MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm]

theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_snorm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hp : 1 ≤ p) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N) : ∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)

Alias of MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm.

theorem MeasureTheory.Lp.cauchy_tendsto_of_tendsto {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (f_lim : α → E) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)

theorem MeasureTheory.Lp.memℒp_of_cauchy_tendsto {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) (f_lim : α → E) (h_lim_meas : MeasureTheory.AEStronglyMeasurable f_lim μ) (h_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)) : MeasureTheory.Memℒp f_lim p μ

theorem MeasureTheory.Lp.cauchy_complete_ℒp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N) : ∃ (f_lim : α → E), MeasureTheory.Memℒp f_lim p μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)

Lp is complete for 1 ≤ p

instance MeasureTheory.Lp.instCompleteSpace {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] [hp : Fact (1 ≤ p)] : CompleteSpace ↥(MeasureTheory.Lp E p μ)

Continuous functions in Lp

def MeasureTheory.Lp.boundedContinuousFunction {α : Type u_1} (E : Type u_2) {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] : AddSubgroup ↥(MeasureTheory.Lp E p μ)

An additive subgroup of Lp E p μ, consisting of the equivalence classes which contain a bounded continuous representative.

Equations

• MeasureTheory.Lp.boundedContinuousFunction E p μ = ((ContinuousMap.toAEEqFunAddHom μ).comp (BoundedContinuousFunction.toContinuousMapAddHom α E)).range.addSubgroupOf (MeasureTheory.Lp E p μ)

theorem MeasureTheory.Lp.mem_boundedContinuousFunction_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] {f : ↥(MeasureTheory.Lp E p μ)} : f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔ ∃ (f₀ : BoundedContinuousFunction α E), ContinuousMap.toAEEqFun μ f₀.toContinuousMap = ↑f

By definition, the elements of Lp.boundedContinuousFunction E p μ are the elements of Lp E p μ which contain a bounded continuous representative.

theorem BoundedContinuousFunction.mem_Lp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction α E) : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ MeasureTheory.Lp E p μ

A bounded continuous function on a finite-measure space is in Lp.

theorem BoundedContinuousFunction.Lp_nnnorm_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction α E) : ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊

The Lp-norm of a bounded continuous function is at most a constant (depending on the measure of the whole space) times its sup-norm.

theorem BoundedContinuousFunction.Lp_norm_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction α E) : ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * ‖f‖

The Lp-norm of a bounded continuous function is at most a constant (depending on the measure of the whole space) times its sup-norm.

def BoundedContinuousFunction.toLpHom {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] [Fact (1 ≤ p)] : NormedAddGroupHom (BoundedContinuousFunction α E) ↥(MeasureTheory.Lp E p μ)

The normed group homomorphism of considering a bounded continuous function on a finite-measure space as an element of Lp.

Equations

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

theorem BoundedContinuousFunction.range_toLpHom {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] [Fact (1 ≤ p)] : (BoundedContinuousFunction.toLpHom p μ).range = MeasureTheory.Lp.boundedContinuousFunction E p μ

def BoundedContinuousFunction.toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] : BoundedContinuousFunction α E →L[𝕜] ↥(MeasureTheory.Lp E p μ)

The bounded linear map of considering a bounded continuous function on a finite-measure space as an element of Lp.

Equations

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

theorem BoundedContinuousFunction.coeFn_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : BoundedContinuousFunction α E) : ↑↑((BoundedContinuousFunction.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f

theorem BoundedContinuousFunction.range_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] : (LinearMap.range (BoundedContinuousFunction.toLp p μ 𝕜)).toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ

theorem BoundedContinuousFunction.toLp_norm_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : ‖BoundedContinuousFunction.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹

theorem BoundedContinuousFunction.toLp_inj {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] {f g : BoundedContinuousFunction α E} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] : (BoundedContinuousFunction.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) g ↔ f = g

theorem BoundedContinuousFunction.toLp_injective {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] : Function.Injective ⇑(BoundedContinuousFunction.toLp p μ 𝕜)

def ContinuousMap.toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_5) [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] : C(α, E) →L[𝕜] ↥(MeasureTheory.Lp E p μ)

The bounded linear map of considering a continuous function on a compact finite-measure space α as an element of Lp. By definition, the norm on C(α, E) is the sup-norm, transferred from the space α →ᵇ E of bounded continuous functions, so this construction is just a matter of transferring the structure from BoundedContinuousFunction.toLp along the isometry.

Equations

• ContinuousMap.toLp p μ 𝕜 = (BoundedContinuousFunction.toLp p μ 𝕜).comp (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearIsometry.toContinuousLinearMap

theorem ContinuousMap.range_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] : (LinearMap.range (ContinuousMap.toLp p μ 𝕜)).toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ

theorem ContinuousMap.coeFn_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) : ↑↑((ContinuousMap.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f

theorem ContinuousMap.toLp_def {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) : (ContinuousMap.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) ((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f)

@[simp]

theorem ContinuousMap.toLp_comp_toContinuousMap {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : BoundedContinuousFunction α E) : (ContinuousMap.toLp p μ 𝕜) f.toContinuousMap = (BoundedContinuousFunction.toLp p μ 𝕜) f

@[simp]

theorem ContinuousMap.coe_toLp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NormedField 𝕜] [NormedSpace 𝕜 E] (f : C(α, E)) : ↑((ContinuousMap.toLp p μ 𝕜) f) = ContinuousMap.toAEEqFun μ f

theorem ContinuousMap.toLp_injective {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] : Function.Injective ⇑(ContinuousMap.toLp p μ 𝕜)

theorem ContinuousMap.toLp_inj {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] {f g : C(α, E)} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] : (ContinuousMap.toLp p μ 𝕜) f = (ContinuousMap.toLp p μ 𝕜) g ↔ f = g

theorem ContinuousMap.hasSum_of_hasSum_Lp {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] {β : Type u_6} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] {g : β → C(α, E)} {f : C(α, E)} (hg : Summable g) (hg2 : HasSum (⇑(ContinuousMap.toLp p μ 𝕜) ∘ g) ((ContinuousMap.toLp p μ 𝕜) f)) : HasSum g f

If a sum of continuous functions g n is convergent, and the same sum converges in Lᵖ to h, then in fact g n converges uniformly to h.

theorem ContinuousMap.toLp_norm_eq_toLp_norm_coe {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : ‖ContinuousMap.toLp p μ 𝕜‖ = ‖BoundedContinuousFunction.toLp p μ 𝕜‖

theorem ContinuousMap.toLp_norm_le {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [TopologicalSpace α] [BorelSpace α] [SecondCountableTopologyEither α E] [CompactSpace α] [MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_5} [Fact (1 ≤ p)] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : ‖ContinuousMap.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹

Bound for the operator norm of ContinuousMap.toLp.

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

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

theorem MeasureTheory.Lp.mul_meas_ge_le_pow_norm' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (f : ↥(MeasureTheory.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_norm {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (f : ↥(MeasureTheory.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