Documentation

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

ℒp space #

This file describes properties of almost everywhere strongly measurable functions with finite p-seminorm, denoted by snorm f p μ and defined for p:ℝ≥0∞ as 0 if p=0, (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and essSup ‖f‖ μ for p=∞.

The Prop-valued Memℒp f p μ states that a function f : α → E has finite p-seminorm and is almost everywhere strongly measurable.

Main definitions #

ℒp seminorm #

We define the ℒp seminorm, denoted by snorm f p μ. For real p, it is given by an integral formula (for which we use the notation snorm' f p μ), and for p = ∞ it is the essential supremum (for which we use the notation snormEssSup f μ).

We also define a predicate Memℒp f p μ, requesting that a function is almost everywhere measurable and has finite snorm f p μ.

This paragraph is devoted to the basic properties of these definitions. It is constructed as follows: for a given property, we prove it for snorm' and snormEssSup when it makes sense, deduce it for snorm, and translate it in terms of Memℒp.

def MeasureTheory.snorm' {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] :
{x : MeasurableSpace α} → (αF)MeasureTheory.Measure αENNReal

(∫ ‖f a‖^q ∂μ) ^ (1/q), which is a seminorm on the space of measurable functions for which this quantity is finite

Equations
Instances For
    def MeasureTheory.snormEssSup {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] :
    {x : MeasurableSpace α} → (αF)MeasureTheory.Measure αENNReal

    seminorm for ℒ∞, equal to the essential supremum of ‖f‖.

    Equations
    Instances For
      def MeasureTheory.snorm {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] :
      {x : MeasurableSpace α} → (αF)ENNRealMeasureTheory.Measure αENNReal

      ℒp seminorm, equal to 0 for p=0, to (∫ ‖f a‖^p ∂μ) ^ (1/p) for 0 < p < ∞ and to essSup ‖f‖ μ for p = ∞.

      Equations
      Instances For
        theorem MeasureTheory.snorm_eq_snorm' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp_ne_zero : p 0) (hp_ne_top : p ) {f : αF} :
        theorem MeasureTheory.snorm_eq_lintegral_rpow_nnnorm {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp_ne_zero : p 0) (hp_ne_top : p ) {f : αF} :
        MeasureTheory.snorm f p μ = (∫⁻ (x : α), f x‖₊ ^ p.toRealμ) ^ (1 / p.toReal)
        theorem MeasureTheory.snorm_one_eq_lintegral_nnnorm {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
        MeasureTheory.snorm f 1 μ = ∫⁻ (x : α), f x‖₊μ
        def MeasureTheory.Memℒp {E : Type u_2} [NormedAddCommGroup E] {α : Type u_5} :
        {x : MeasurableSpace α} → (αE)ENNRealautoParam (MeasureTheory.Measure α) _auto✝Prop

        The property that f:α→E is ae strongly measurable and (∫ ‖f a‖^p ∂μ)^(1/p) is finite if p < ∞, or essSup f < ∞ if p = ∞.

        Equations
        Instances For
          theorem MeasureTheory.lintegral_rpow_nnnorm_eq_rpow_snorm' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} (hq0_lt : 0 < q) :
          ∫⁻ (a : α), f a‖₊ ^ qμ = MeasureTheory.snorm' f q μ ^ q
          theorem MeasureTheory.Memℒp.snorm_lt_top {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (hfp : MeasureTheory.Memℒp f p μ) :
          theorem MeasureTheory.Memℒp.snorm_ne_top {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (hfp : MeasureTheory.Memℒp f p μ) :
          theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} (hq0_lt : 0 < q) (hfq : MeasureTheory.snorm' f q μ < ) :
          ∫⁻ (a : α), f a‖₊ ^ qμ <
          theorem MeasureTheory.lintegral_rpow_nnnorm_lt_top_of_snorm_lt_top {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} (hp_ne_zero : p 0) (hp_ne_top : p ) (hfp : MeasureTheory.snorm f p μ < ) :
          ∫⁻ (a : α), f a‖₊ ^ p.toRealμ <
          theorem MeasureTheory.snorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} (hp_ne_zero : p 0) (hp_ne_top : p ) :
          MeasureTheory.snorm f p μ < ∫⁻ (a : α), f a‖₊ ^ p.toRealμ <
          @[simp]
          theorem MeasureTheory.snorm'_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          @[simp]
          theorem MeasureTheory.snorm_exponent_zero {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          @[simp]
          theorem MeasureTheory.snorm'_zero {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp0_lt : 0 < q) :
          @[simp]
          theorem MeasureTheory.snorm'_zero' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hq0_ne : q 0) (hμ : μ 0) :
          @[simp]
          theorem MeasureTheory.snorm_zero {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] :
          @[simp]
          theorem MeasureTheory.snorm_zero' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] :
          MeasureTheory.snorm (fun (x : α) => 0) p μ = 0
          theorem MeasureTheory.zero_mem_ℒp' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] :
          MeasureTheory.Memℒp (fun (x : α) => 0) p μ
          theorem MeasureTheory.snorm'_measure_zero_of_pos {α : Type u_1} {F : Type u_3} {q : } [NormedAddCommGroup F] [MeasurableSpace α] {f : αF} (hq_pos : 0 < q) :
          theorem MeasureTheory.snorm'_measure_zero_of_neg {α : Type u_1} {F : Type u_3} {q : } [NormedAddCommGroup F] [MeasurableSpace α] {f : αF} (hq_neg : q < 0) :
          @[simp]
          @[simp]
          theorem MeasureTheory.snorm_measure_zero {α : Type u_1} {F : Type u_3} {p : ENNReal} [NormedAddCommGroup F] [MeasurableSpace α] {f : αF} :
          @[simp]
          theorem MeasureTheory.snorm'_neg {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          @[simp]
          theorem MeasureTheory.snorm_neg {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          theorem MeasureTheory.Memℒp.neg {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (hf : MeasureTheory.Memℒp f p μ) :
          theorem MeasureTheory.memℒp_neg_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} :
          theorem MeasureTheory.snorm'_const {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (hq_pos : 0 < q) :
          MeasureTheory.snorm' (fun (x : α) => c) q μ = c‖₊ * μ Set.univ ^ (1 / q)
          theorem MeasureTheory.snorm'_const' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [MeasureTheory.IsFiniteMeasure μ] (c : F) (hc_ne_zero : c 0) (hq_ne_zero : q 0) :
          MeasureTheory.snorm' (fun (x : α) => c) q μ = c‖₊ * μ Set.univ ^ (1 / q)
          theorem MeasureTheory.snormEssSup_const {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (hμ : μ 0) :
          MeasureTheory.snormEssSup (fun (x : α) => c) μ = c‖₊
          theorem MeasureTheory.snorm'_const_of_isProbabilityMeasure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (hq_pos : 0 < q) [MeasureTheory.IsProbabilityMeasure μ] :
          MeasureTheory.snorm' (fun (x : α) => c) q μ = c‖₊
          theorem MeasureTheory.snorm_const {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (h0 : p 0) (hμ : μ 0) :
          MeasureTheory.snorm (fun (x : α) => c) p μ = c‖₊ * μ Set.univ ^ (1 / p.toReal)
          theorem MeasureTheory.snorm_const' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (c : F) (h0 : p 0) (h_top : p ) :
          MeasureTheory.snorm (fun (x : α) => c) p μ = c‖₊ * μ Set.univ ^ (1 / p.toReal)
          theorem MeasureTheory.snorm_const_lt_top_iff {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ENNReal} {c : F} (hp_ne_zero : p 0) (hp_ne_top : p ) :
          MeasureTheory.snorm (fun (x : α) => c) p μ < c = 0 μ Set.univ <
          theorem MeasureTheory.memℒp_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (c : E) [MeasureTheory.IsFiniteMeasure μ] :
          MeasureTheory.Memℒp (fun (x : α) => c) p μ
          theorem MeasureTheory.memℒp_top_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (c : E) :
          MeasureTheory.Memℒp (fun (x : α) => c) μ
          theorem MeasureTheory.memℒp_const_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {p : ENNReal} {c : E} (hp_ne_zero : p 0) (hp_ne_top : p ) :
          MeasureTheory.Memℒp (fun (x : α) => c) p μ c = 0 μ Set.univ <
          theorem MeasureTheory.snorm'_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (hq : 0 q) (h : ∀ᵐ (x : α) ∂μ, f x‖₊ g x‖₊) :
          theorem MeasureTheory.snorm'_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (hq : 0 q) (h : ∀ᵐ (x : α) ∂μ, f x g x) :
          theorem MeasureTheory.snorm'_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : αF} (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ = g x‖₊) :
          theorem MeasureTheory.snorm'_congr_norm_ae {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : αF} (hfg : ∀ᵐ (x : α) ∂μ, f x = g x) :
          theorem MeasureTheory.snorm'_congr_ae {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : αF} (hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g) :
          theorem MeasureTheory.snormEssSup_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : αF} (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ g x‖₊) :
          theorem MeasureTheory.snorm_mono_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ g x‖₊) :
          theorem MeasureTheory.snorm_mono_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
          theorem MeasureTheory.snorm_mono_ae_real {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : α} (h : ∀ᵐ (x : α) ∂μ, f x g x) :
          theorem MeasureTheory.snorm_mono_nnnorm {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (h : ∀ (x : α), f x‖₊ g x‖₊) :
          theorem MeasureTheory.snorm_mono {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (h : ∀ (x : α), f x g x) :
          theorem MeasureTheory.snorm_mono_real {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : α} (h : ∀ (x : α), f x g x) :
          theorem MeasureTheory.snormEssSup_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, f x‖₊ C) :
          theorem MeasureTheory.snormEssSup_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
          theorem MeasureTheory.snormEssSup_lt_top_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, f x‖₊ C) :
          theorem MeasureTheory.snormEssSup_lt_top_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
          theorem MeasureTheory.snorm_le_of_ae_nnnorm_bound {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {C : NNReal} (hfC : ∀ᵐ (x : α) ∂μ, f x‖₊ C) :
          MeasureTheory.snorm f p μ C μ Set.univ ^ p.toReal⁻¹
          theorem MeasureTheory.snorm_le_of_ae_bound {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {C : } (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
          MeasureTheory.snorm f p μ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C
          theorem MeasureTheory.snorm_congr_nnnorm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ = g x‖₊) :
          theorem MeasureTheory.snorm_congr_norm_ae {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} (hfg : ∀ᵐ (x : α) ∂μ, f x = g x) :
          @[simp]
          theorem MeasureTheory.snorm'_norm {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          MeasureTheory.snorm' (fun (a : α) => f a) q μ = MeasureTheory.snorm' f q μ
          @[simp]
          theorem MeasureTheory.snorm_norm {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : αF) :
          MeasureTheory.snorm (fun (x : α) => f x) p μ = MeasureTheory.snorm f p μ
          theorem MeasureTheory.snorm'_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : αF) (p : ) (q : ) (hq_pos : 0 < q) :
          MeasureTheory.snorm' (fun (x : α) => f x ^ q) p μ = MeasureTheory.snorm' f (p * q) μ ^ q
          theorem MeasureTheory.snorm_norm_rpow {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : αF) (hq_pos : 0 < q) :
          MeasureTheory.snorm (fun (x : α) => f x ^ q) p μ = MeasureTheory.snorm f (p * ENNReal.ofReal q) μ ^ q
          theorem MeasureTheory.snorm_congr_ae {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} {g : αF} (hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g) :
          theorem MeasureTheory.memℒp_congr_ae {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} {g : αE} (hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g) :
          theorem MeasureTheory.Memℒp.ae_eq {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} {g : αE} (hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g) (hf_Lp : MeasureTheory.Memℒp f p μ) :
          theorem MeasureTheory.Memℒp.of_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 : αF} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :
          theorem MeasureTheory.Memℒp.mono {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x g x) :

          Alias of MeasureTheory.Memℒp.of_le.

          theorem MeasureTheory.Memℒp.mono' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} {g : α} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h : ∀ᵐ (a : α) ∂μ, f a g a) :
          theorem MeasureTheory.Memℒp.congr_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
          theorem MeasureTheory.memℒp_congr_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, f a = g a) :
          theorem MeasureTheory.memℒp_top_of_bound {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
          theorem MeasureTheory.Memℒp.of_bound {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) (C : ) (hfC : ∀ᵐ (x : α) ∂μ, f x C) :
          theorem MeasureTheory.snorm'_mono_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : αF) (hμν : ν μ) (hq : 0 q) :
          theorem MeasureTheory.snorm_mono_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : αF) (hμν : ν μ) :
          theorem MeasureTheory.Memℒp.mono_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (hμν : ν μ) (hf : MeasureTheory.Memℒp f p μ) :
          theorem MeasureTheory.snorm'_smul_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : } (hp : 0 p) {f : αF} (c : ENNReal) :
          MeasureTheory.snorm' f p (c μ) = c ^ (1 / p) * MeasureTheory.snorm' f p μ
          theorem MeasureTheory.snorm_smul_measure_of_ne_zero {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ENNReal} {f : αF} {c : ENNReal} (hc : c 0) :
          MeasureTheory.snorm f p (c μ) = c ^ (1 / p).toReal MeasureTheory.snorm f p μ
          theorem MeasureTheory.snorm_smul_measure_of_ne_top {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {p : ENNReal} (hp_ne_top : p ) {f : αF} (c : ENNReal) :
          MeasureTheory.snorm f p (c μ) = c ^ (1 / p).toReal MeasureTheory.snorm f p μ
          theorem MeasureTheory.snorm_one_smul_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} (c : ENNReal) :
          theorem MeasureTheory.Memℒp.of_measure_le_smul {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {μ' : MeasureTheory.Measure α} (c : ENNReal) (hc : c ) (hμ'_le : μ' c μ) {f : αE} (hf : MeasureTheory.Memℒp f p μ) :
          theorem MeasureTheory.Memℒp.smul_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} {c : ENNReal} (hf : MeasureTheory.Memℒp f p μ) (hc : c ) :
          theorem MeasureTheory.Memℒp.left_of_add_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (h : MeasureTheory.Memℒp f p (μ + ν)) :
          theorem MeasureTheory.Memℒp.norm {α : 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 (fun (x : α) => f x) p μ
          theorem MeasureTheory.memℒp_norm_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
          MeasureTheory.Memℒp (fun (x : α) => f x) p μ MeasureTheory.Memℒp f p μ
          theorem MeasureTheory.snorm'_eq_zero_of_ae_zero {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} (hq0_lt : 0 < q) (hf_zero : f =ᶠ[MeasureTheory.Measure.ae μ] 0) :
          theorem MeasureTheory.snorm'_eq_zero_of_ae_zero' {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hq0_ne : q 0) (hμ : μ 0) {f : αF} (hf_zero : f =ᶠ[MeasureTheory.Measure.ae μ] 0) :
          theorem MeasureTheory.snorm'_eq_zero_iff {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hq0_lt : 0 < q) {f : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
          theorem MeasureTheory.coe_nnnorm_ae_le_snormEssSup {α : Type u_1} {F : Type u_3} [NormedAddCommGroup F] :
          ∀ {x : MeasurableSpace α} (f : αF) (μ : MeasureTheory.Measure α), ∀ᵐ (x_1 : α) ∂μ, f x_1‖₊ MeasureTheory.snormEssSup f μ
          theorem MeasureTheory.ae_le_snormEssSup {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          ∀ᵐ (y : α) ∂μ, f y‖₊ MeasureTheory.snormEssSup f μ
          theorem MeasureTheory.meas_snormEssSup_lt {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {f : αF} :
          μ {y : α | MeasureTheory.snormEssSup f μ < f y‖₊} = 0
          theorem MeasureTheory.snorm_map_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : αβ} {g : βE} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) :
          theorem MeasureTheory.Memℒp.comp_of_map {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : αβ} {g : βE} (hg : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) :
          theorem MeasureTheory.snorm_comp_measurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : αβ} {g : βE} {ν : MeasureTheory.Measure β} (hg : MeasureTheory.AEStronglyMeasurable g ν) (hf : MeasureTheory.MeasurePreserving f μ ν) :
          theorem MeasureTheory.Memℒp.comp_measurePreserving {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {β : Type u_5} {mβ : MeasurableSpace β} {f : αβ} {g : βE} {ν : MeasureTheory.Measure β} (hg : MeasureTheory.Memℒp g p ν) (hf : MeasureTheory.MeasurePreserving f μ ν) :
          theorem MeasurableEmbedding.snorm_map_measure {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_5} {mβ : MeasurableSpace β} {f : αβ} {g : βF} (hf : MeasurableEmbedding f) :
          theorem MeasurableEmbedding.memℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_5} {mβ : MeasurableSpace β} {f : αβ} {g : βF} (hf : MeasurableEmbedding f) :
          theorem MeasurableEquiv.memℒp_map_measure_iff {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {β : Type u_5} {mβ : MeasurableSpace β} (f : α ≃ᵐ β) {g : βF} :
          theorem MeasureTheory.snorm'_le_nnreal_smul_snorm'_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) {p : } (hp : 0 < p) :
          theorem MeasureTheory.snormEssSup_le_nnreal_smul_snormEssSup_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) :
          theorem MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} {c : NNReal} (h : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) (p : ENNReal) :
          theorem MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (hc : c < 0) (p : ENNReal) :

          When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an snorm of 0.

          theorem MeasureTheory.snorm_le_mul_snorm_of_ae_le_mul {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedAddCommGroup G] {f : αF} {g : αG} {c : } (h : ∀ᵐ (x : α) ∂μ, f x c * g x) (p : ENNReal) :
          theorem MeasureTheory.Memℒp.of_nnnorm_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {c : NNReal} (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x‖₊ c * g x‖₊) :
          theorem MeasureTheory.Memℒp.of_le_mul {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : αE} {g : αF} {c : } (hg : MeasureTheory.Memℒp g p μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfg : ∀ᵐ (x : α) ∂μ, f x c * g x) :

          Bounded actions by normed rings #

          In this section we show inequalities on the norm.

          theorem MeasureTheory.snorm'_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : αF) (hq_pos : 0 < q) :
          theorem MeasureTheory.snormEssSup_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : αF) :
          theorem MeasureTheory.snorm_const_smul_le {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : αF) :
          theorem MeasureTheory.Memℒp.const_smul {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {𝕜 : Type u_5} [NormedRing 𝕜] [MulActionWithZero 𝕜 E] [BoundedSMul 𝕜 E] {f : αE} (hf : MeasureTheory.Memℒp f p μ) (c : 𝕜) :
          theorem MeasureTheory.Memℒp.const_mul {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {R : Type u_6} [NormedRing R] {f : αR} (hf : MeasureTheory.Memℒp f p μ) (c : R) :
          MeasureTheory.Memℒp (fun (x : α) => c * f x) p μ

          Bounded actions by normed division rings #

          The inequalities in the previous section are now tight.

          theorem MeasureTheory.snorm'_const_smul {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] {f : αF} (c : 𝕜) (hq_pos : 0 < q) :
          theorem MeasureTheory.snormEssSup_const_smul {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : αF) :
          theorem MeasureTheory.snorm_const_smul {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] {𝕜 : Type u_5} [NormedDivisionRing 𝕜] [Module 𝕜 F] [BoundedSMul 𝕜 F] (c : 𝕜) (f : αF) :
          theorem MeasureTheory.snorm_indicator_ge_of_bdd_below {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (hp : p 0) (hp' : p ) {f : αF} (C : NNReal) {s : Set α} (hs : MeasurableSet s) (hf : ∀ᵐ (x : α) ∂μ, x sC Set.indicator s f x‖₊) :
          C μ s ^ (1 / p.toReal) MeasureTheory.snorm (Set.indicator s f) p μ
          theorem MeasureTheory.Memℒp.re {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α𝕜} (hf : MeasureTheory.Memℒp f p μ) :
          MeasureTheory.Memℒp (fun (x : α) => RCLike.re (f x)) p μ
          theorem MeasureTheory.Memℒp.im {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α𝕜} (hf : MeasureTheory.Memℒp f p μ) :
          MeasureTheory.Memℒp (fun (x : α) => RCLike.im (f x)) p μ
          theorem MeasureTheory.ae_bdd_liminf_atTop_rpow_of_snorm_bdd {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} {f : αE} (hfmeas : ∀ (n : ), Measurable (f n)) (hbdd : ∀ (n : ), MeasureTheory.snorm (f n) p μ R) :
          ∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ) => f n x‖₊ ^ p.toReal) Filter.atTop <
          theorem MeasureTheory.ae_bdd_liminf_atTop_of_snorm_bdd {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} (hp : p 0) {f : αE} (hfmeas : ∀ (n : ), Measurable (f n)) (hbdd : ∀ (n : ), MeasureTheory.snorm (f n) p μ R) :
          ∀ᵐ (x : α) ∂μ, Filter.liminf (fun (n : ) => f n x‖₊) Filter.atTop <

          A continuous function with compact support belongs to L^∞.