Documentation

LeanAPAP.Prereqs.LpNorm.Compact

Normalised Lp norms #

Lp norm #

source
noncomputable def MeasureTheory.cLpNorm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) (f : α → E) :
ℝ

The Lp norm of a function with the compact normalisation.

Equations
Instances For
    source
    def MeasureTheory.«term‖_‖ₙ_[_]» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_nonneg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} :
      0 ≤ ‖f‖ₙ_[p]
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_exponent_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) :
      ‖f‖ₙ_[0] = 0
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) :
      ‖0‖ₙ_[p] = 0
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_zero' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) :
      ‖fun (x : α) => 0‖ₙ_[p] = 0
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_of_isEmpty {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [IsEmpty α] (f : α → E) (p : ENNReal) :
      ‖f‖ₙ_[p] = 0
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_neg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (p : ENNReal) :
      ‖-f‖ₙ_[p] = ‖f‖ₙ_[p]
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_neg' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (p : ENNReal) :
      ‖fun (x : α) => -f x‖ₙ_[p] = ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_sub_comm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f g : α → E) (p : ENNReal) :
      ‖f - g‖ₙ_[p] = ‖g - f‖ₙ_[p]
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {f : α → E} (hf : StronglyMeasurable f) (p : ENNReal) :
      ‖fun (i : α) => ‖f i‖‖ₙ_[p] = ‖f‖ₙ_[p]
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_abs {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : StronglyMeasurable f) (p : ENNReal) :
      ‖|f|‖ₙ_[p] = ‖f‖ₙ_[p]
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_fun_abs {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : StronglyMeasurable f) (p : ENNReal) :
      ‖fun (i : α) => |f i|‖ₙ_[p] = ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_const_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [NormedField 𝕜] {p : ENNReal} [Module 𝕜 E] [NormSMulClass 𝕜 E] (c : 𝕜) (f : α → E) :
      ‖c • f‖ₙ_[p] = ‖c‖ * ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_nsmul {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (f : α → E) (p : ENNReal) :
      ‖n • f‖ₙ_[p] = n • ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_natCast_mul {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜) (p : ENNReal) :
      ‖↑n * f‖ₙ_[p] = ↑n * ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_fun_natCast_mul {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜) (p : ENNReal) :
      ‖fun (x : α) => ↑n * f x‖ₙ_[p] = ↑n * ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_mul_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ) (p : ENNReal) :
      ‖f * ↑n‖ₙ_[p] = ‖f‖ₙ_[p] * ↑n
      source
      theorem MeasureTheory.cLpNorm_fun_mul_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ) (p : ENNReal) :
      ‖fun (x : α) => f x * ↑n‖ₙ_[p] = ‖f‖ₙ_[p] * ↑n
      source
      theorem MeasureTheory.cLpNorm_div_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ENNReal) :
      ‖f / ↑n‖ₙ_[p] = ‖f‖ₙ_[p] / ↑n
      source
      theorem MeasureTheory.cLpNorm_fun_div_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] [CharZero 𝕜] {n : ℕ} (hn : n ≠ 0) (f : α → 𝕜) (p : ENNReal) :
      ‖fun (x : α) => f x / ↑n‖ₙ_[p] = ‖f‖ₙ_[p] / ↑n
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_conj {α : Type u_1} {R : Type u_3} [MeasurableSpace α] {p : ENNReal} [RCLike R] (f : α → R) :
      ‖(starRingEnd (α → R)) f‖ₙ_[p] = ‖f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_add_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) :
      ‖f + g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_sub_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) :
      ‖f - g‖ₙ_[p] ≤ ‖f‖ₙ_[p] + ‖g‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_sum_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [DiscreteMeasurableSpace α] [Finite α] {ι : Type u_5} {s : Finset ι} {f : ι → α → E} (hp : 1 ≤ p) :
      ‖∑ i ∈ s, f i‖ₙ_[p] ≤ ∑ i ∈ s, ‖f i‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_expect_le {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [DiscreteMeasurableSpace α] [Finite α] [Module ℚ≥0 E] [NormedSpace ℝ E] {ι : Type u_5} {s : Finset ι} {f : ι → α → E} (hp : 1 ≤ p) :
      ‖s.expect fun (i : ι) => f i‖ₙ_[p] ≤ s.expect fun (i : ι) => ‖f i‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_le_cLpNorm_add_cLpNorm_sub' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) :
      ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖f - g‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_le_cLpNorm_add_cLpNorm_sub {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) :
      ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p] + ‖g - f‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_le_add_cLpNorm_add {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) :
      ‖f‖ₙ_[p] ≤ ‖f + g‖ₙ_[p] + ‖g‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_sub_le_cLpNorm_sub_add_cLpNorm_sub {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f g h : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : 1 ≤ p) :
      ‖f - h‖ₙ_[p] ≤ ‖f - g‖ₙ_[p] + ‖g - h‖ₙ_[p]
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_const {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Finite α] [Nonempty α] {p : ENNReal} (hp : p ≠ 0) (a : E) :
      ‖fun (_i : α) => a‖ₙ_[p] = ↑‖a‖₊
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_one {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [Finite α] [NormedField 𝕜] {p : ENNReal} [Nonempty α] (hp : p ≠ 0) :
      ‖1‖ₙ_[p] = 1
      source
      theorem MeasureTheory.cLpNorm_eq_expect_norm' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [DiscreteMeasurableSpace α] [Fintype α] (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (f : α → E) :
      ‖f‖ₙ_[p] = (Finset.univ.expect fun (i : α) => ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹
      source
      theorem MeasureTheory.cLpNorm_toNNReal_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] {p : ℝ} (hp : 0 < p) (f : α → E) :
      ‖f‖ₙ_[↑p.toNNReal] = (Finset.univ.expect fun (i : α) => ‖f i‖ ^ p) ^ p⁻¹
      source
      theorem MeasureTheory.cLpNorm_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] {p : NNReal} (hp : p ≠ 0) (f : α → E) :
      ‖f‖ₙ_[↑p] = (Finset.univ.expect fun (i : α) => ‖f i‖ ^ ↑p) ^ (↑p)⁻¹
      source
      theorem MeasureTheory.cLpNorm_rpow_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] {p : NNReal} (hp : p ≠ 0) (f : α → E) :
      ‖f‖ₙ_[↑p] ^ ↑p = Finset.univ.expect fun (i : α) => ‖f i‖ ^ ↑p
      source
      theorem MeasureTheory.cLpNorm_pow_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] {p : ℕ} (hp : p ≠ 0) (f : α → E) :
      ‖f‖ₙ_[↑p] ^ p = Finset.univ.expect fun (i : α) => ‖f i‖ ^ p
      source
      theorem MeasureTheory.cL2Norm_sq_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] (f : α → E) :
      ‖f‖ₙ_[2] ^ 2 = Finset.univ.expect fun (i : α) => ‖f i‖ ^ 2
      source
      theorem MeasureTheory.cL2Norm_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] (f : α → E) :
      ‖f‖ₙ_[2] = (Finset.univ.expect fun (i : α) => ‖f i‖ ^ 2) ^ 2⁻¹
      source
      theorem MeasureTheory.cL1Norm_eq_expect_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Fintype α] (f : α → E) :
      ‖f‖ₙ_[1] = Finset.univ.expect fun (i : α) => ‖f i‖
      source
      theorem MeasureTheory.cLpNorm_exponent_top_eq_essSup {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Finite α] (f : α → E) :
      ‖f‖ₙ_[⊤] = ⨆ (i : α), ‖f i‖
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_eq_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : p ≠ 0) :
      ‖f‖ₙ_[p] = 0 ↔ f = 0
      source
      @[simp]
      theorem MeasureTheory.cLpNorm_pos {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : p ≠ 0) :
      0 < ‖f‖ₙ_[p] ↔ f ≠ 0
      source
      theorem MeasureTheory.cLpNorm_mono_right {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p q : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hpq : p ≤ q) :
      ‖f‖ₙ_[p] ≤ ‖f‖ₙ_[q]
      source
      theorem MeasureTheory.cLpNorm_mono_real {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] {g : α → ℝ} (h : ∀ (x : α), ‖f x‖ ≤ g x) :
      ‖f‖ₙ_[p] ≤ ‖g‖ₙ_[p]
      source
      theorem MeasureTheory.cLpNorm_two_mul_sum_pow {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] [Fintype α] {ι : Type u_5} {n : ℕ} (hn : n ≠ 0) (s : Finset ι) (f : ι → α → ℂ) :
      ↑‖∑ i ∈ s, f i‖ₙ_[2 * ↑n] ^ (2 * n) = ∑ x ∈ Fintype.piFinset fun (x : Fin n) => s, ∑ y ∈ Fintype.piFinset fun (x : Fin n) => s, Finset.univ.expect fun (a : α) => (∏ i : Fin n, (starRingEnd ℂ) (f (x i) a)) * ∏ i : Fin n, f (y i) a
      source
      def Mathlib.Meta.Positivity.evalCLpNorm :
      PositivityExt

      The positivity extension which identifies expressions of the form ‖f‖ₙ_[p].

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

        Hölder inequality #

        source
        theorem MeasureTheory.cLpNorm_rpow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {p q : NNReal} {f : α → ℝ} (hp : p ≠ 0) (hq : q ≠ 0) (hf : 0 ≤ f) :
        ‖f ^ ↑q‖ₙ_[↑p] = ‖f‖ₙ_[↑p * ↑q] ^ ↑q
        source
        theorem MeasureTheory.cLpNorm_pow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {p : NNReal} (hp : p ≠ 0) {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) :
        ‖f ^ q‖ₙ_[↑p] = ‖f‖ₙ_[↑p * ↑q] ^ q
        source
        theorem MeasureTheory.cL1Norm_rpow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {q : NNReal} {f : α → ℝ} (hq : q ≠ 0) (hf : 0 ≤ f) :
        ‖f ^ ↑q‖ₙ_[1] = ‖f‖ₙ_[↑q] ^ ↑q
        source
        theorem MeasureTheory.cL1Norm_pow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) :
        ‖f ^ q‖ₙ_[1] = ‖f‖ₙ_[↑q] ^ q
        source
        theorem MeasureTheory.cLpNorm_rpow' {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] [RCLike 𝕜] {p q : NNReal} (hp : p ≠ 0) (hq : q ≠ 0) (f : α → 𝕜) :
        ‖f‖ₙ_[↑p] ^ ↑q = ‖(fun (a : α) => ‖f a‖) ^ ↑q‖ₙ_[↑p / ↑q]
        source
        @[simp]
        theorem MeasureTheory.RCLike.cLpNorm_coe_comp {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [RCLike 𝕜] (p : ENNReal) (f : α → ℝ) :
        ‖RCLike.ofReal ∘ f‖ₙ_[p] = ‖f‖ₙ_[p]
        source
        @[simp]
        theorem MeasureTheory.Complex.cLpNorm_coe_comp {α : Type u_5} {mα : MeasurableSpace α} (p : ENNReal) (f : α → ℝ) :
        ‖Complex.ofReal ∘ f‖ₙ_[p] = ‖f‖ₙ_[p]

        Indicator #

        source
        theorem MeasureTheory.cLpNorm_rpow_indicate {ι : Type u_5} {R : Type u_9} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {p : NNReal} (hp : p ≠ 0) (s : Finset ι) :
        ‖𝟭 s‖ₙ_[↑p] ^ ↑p = ↑s.dens
        source
        theorem MeasureTheory.cLpNorm_indicate {ι : Type u_5} {R : Type u_9} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {p : NNReal} (hp : p ≠ 0) (s : Finset ι) :
        ‖𝟭 s‖ₙ_[↑p] = ↑s.dens ^ (↑p)⁻¹
        source
        theorem MeasureTheory.cLpNorm_pow_indicate {ι : Type u_5} {R : Type u_9} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {p : ℕ} (hp : p ≠ 0) (s : Finset ι) :
        ‖𝟭 s‖ₙ_[↑p] ^ ↑p = ↑s.dens
        source
        theorem MeasureTheory.cL2Norm_sq_indicate {ι : Type u_5} {R : Type u_9} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] (s : Finset ι) :
        ‖𝟭 s‖ₙ_[2] ^ 2 = ↑s.dens
        source
        @[simp]
        theorem MeasureTheory.cL2Norm_indicate {ι : Type u_5} {R : Type u_9} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] (s : Finset ι) :
        ‖𝟭 s‖ₙ_[2] = √↑s.dens
        source
        @[simp]
        theorem MeasureTheory.cL1Norm_indicate {ι : Type u_5} {R : Type u_9} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] (s : Finset ι) :
        ‖𝟭 s‖ₙ_[1] = ↑s.dens

        Translation #

        source
        @[simp]
        theorem MeasureTheory.cLpNorm_translate {G : Type u_6} {E : Type u_8} {mG : MeasurableSpace G} [DiscreteMeasurableSpace G] [AddCommGroup G] [Finite G] {p : ENNReal} [NormedAddCommGroup E] (a : G) (f : G → E) :
        ‖translate a f‖ₙ_[p] = ‖f‖ₙ_[p]
        source
        @[simp]
        theorem MeasureTheory.cLpNorm_conjneg {G : Type u_6} {E : Type u_8} {mG : MeasurableSpace G} [DiscreteMeasurableSpace G] [AddCommGroup G] [Finite G] {p : ENNReal} [RCLike E] (f : G → E) :
        ‖conjneg f‖ₙ_[p] = ‖f‖ₙ_[p]
        source
        theorem MeasureTheory.cLpNorm_translate_sum_sub_le {G : Type u_6} {E : Type u_8} {mG : MeasurableSpace G} [DiscreteMeasurableSpace G] [AddCommGroup G] [Finite G] {p : ENNReal} [NormedAddCommGroup E] (hp : 1 ≤ p) {ι : Type u_10} (s : Finset ι) (a : ι → G) (f : G → E) :
        ‖translate (∑ i ∈ s, a i) f - f‖ₙ_[p] ≤ ∑ i ∈ s, ‖translate (a i) f - f‖ₙ_[p]