Documentation

APAP.Prereqs.LpNorm.Discrete.Defs

Lp norms #

source
noncomputable def MeasureTheory.dLpNorm {α : 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.dLpNorm_nonneg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} :
      0 ≤ ‖f‖_[p]
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_exponent_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) :
      ‖f‖_[0] = 0
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) :
      ‖0‖_[p] = 0
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_zero' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) :
      ‖fun (x : α) => 0‖_[p] = 0
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_of_isEmpty {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [IsEmpty α] (f : α → E) (p : ENNReal) :
      ‖f‖_[p] = 0
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_neg {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (p : ENNReal) :
      ‖-f‖_[p] = ‖f‖_[p]
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_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.dLpNorm_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.dLpNorm_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.dLpNorm_abs {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : StronglyMeasurable f) (p : ENNReal) :
      ‖|f|‖_[p] = ‖f‖_[p]
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_fun_abs {α : Type u_1} [MeasurableSpace α] {f : α → ℝ} (hf : StronglyMeasurable f) (p : ENNReal) :
      ‖fun (i : α) => |f i|‖_[p] = ‖f‖_[p]
      source
      theorem MeasureTheory.dLpNorm_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.dLpNorm_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.dLpNorm_natCast_mul {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜) (p : ENNReal) :
      ‖↑n * f‖_[p] = ↑n * ‖f‖_[p]
      source
      theorem MeasureTheory.dLpNorm_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.dLpNorm_mul_natCast {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [NormedField 𝕜] [NormedSpace ℝ 𝕜] (f : α → 𝕜) (n : ℕ) (p : ENNReal) :
      ‖f * ↑n‖_[p] = ‖f‖_[p] * ↑n
      source
      theorem MeasureTheory.dLpNorm_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.dLpNorm_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.dLpNorm_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
      theorem MeasureTheory.dLpNorm_nnqsmul {α : Type u_1} [MeasurableSpace α] {p : ENNReal} (q : ℚ≥0) (f : α → ℂ) :
      ‖q • f‖_[p] = ↑q * ‖f‖_[p]
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_conj {α : Type u_1} {R : Type u_3} [MeasurableSpace α] {p : ENNReal} [RCLike R] (f : α → R) :
      ‖(starRingEnd (α → R)) f‖_[p] = ‖f‖_[p]
      source
      theorem MeasureTheory.dLpNorm_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.dLpNorm_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.dLpNorm_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.dLpNorm_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.dLpNorm_le_dLpNorm_add_dLpNorm_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.dLpNorm_le_dLpNorm_add_dLpNorm_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.dLpNorm_le_add_dLpNorm_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.dLpNorm_sub_le_dLpNorm_sub_add_dLpNorm_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.dLpNorm_const {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [Nonempty α] {p : ENNReal} (hp : p ≠ 0) (a : E) :
      ‖fun (_i : α) => a‖_[p] = ↑‖a‖₊ * ↑(Fintype.card α) ^ p.toReal⁻¹
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_const' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (a : E) :
      ‖fun (_i : α) => a‖_[p] = ↑‖a‖₊ * ↑(Fintype.card α) ^ p.toReal⁻¹
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_one {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [Fintype α] [NormedField 𝕜] {p : ENNReal} [Nonempty α] (hp : p ≠ 0) :
      ‖1‖_[p] = ↑(Fintype.card α) ^ p.toReal⁻¹
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_one' {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [Fintype α] [NormedField 𝕜] {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) :
      ‖1‖_[p] = ↑(Fintype.card α) ^ p.toReal⁻¹
      source
      theorem MeasureTheory.dLpNorm_eq_sum_norm' {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Fintype α] [DiscreteMeasurableSpace α] (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (f : α → E) :
      ‖f‖_[p] = (∑ i : α, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹
      source
      theorem MeasureTheory.dLpNorm_toNNReal_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : ℝ} (hp : 0 < p) (f : α → E) :
      ‖f‖_[↑p.toNNReal] = (∑ i : α, ‖f i‖ ^ p) ^ p⁻¹
      source
      theorem MeasureTheory.dLpNorm_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : NNReal} (hp : p ≠ 0) (f : α → E) :
      ‖f‖_[↑p] = (∑ i : α, ‖f i‖ ^ ↑p) ^ (↑p)⁻¹
      source
      theorem MeasureTheory.dLpNorm_rpow_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : NNReal} (hp : p ≠ 0) (f : α → E) :
      ‖f‖_[↑p] ^ ↑p = ∑ i : α, ‖f i‖ ^ ↑p
      source
      theorem MeasureTheory.dLpNorm_pow_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] {p : ℕ} (hp : p ≠ 0) (f : α → E) :
      ‖f‖_[↑p] ^ p = ∑ i : α, ‖f i‖ ^ p
      source
      theorem MeasureTheory.dL2Norm_sq_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] (f : α → E) :
      ‖f‖_[2] ^ 2 = ∑ i : α, ‖f i‖ ^ 2
      source
      theorem MeasureTheory.dL2Norm_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] (f : α → E) :
      ‖f‖_[2] = (∑ i : α, ‖f i‖ ^ 2) ^ 2⁻¹
      source
      theorem MeasureTheory.dL1Norm_eq_sum_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [Fintype α] [DiscreteMeasurableSpace α] (f : α → E) :
      ‖f‖_[1] = ∑ i : α, ‖f i‖
      source
      theorem MeasureTheory.dLinftyNorm_eq_iSup_norm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] [DiscreteMeasurableSpace α] [Finite α] (f : α → E) :
      ‖f‖_[⊤] = ⨆ (i : α), ‖f i‖
      source
      theorem MeasureTheory.norm_le_dLinftyNorm {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {f : α → E} [DiscreteMeasurableSpace α] [Finite α] {i : α} :
      ‖f i‖ ≤ ‖f‖_[⊤]
      source
      @[simp]
      theorem MeasureTheory.dLpNorm_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.dLpNorm_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.dLpNorm_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.dLpNorm_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, ∑ a : α, (∏ i : Fin n, (starRingEnd ℂ) (f (x i) a)) * ∏ i : Fin n, f (y i) a
      source
      theorem Mathlib.Meta.Positivity.dLpNorm_pos_of_ne_zero {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} [DiscreteMeasurableSpace α] [Finite α] (hp : p ≠ 0) :
      f ≠ 0 → 0 < ‖f‖_[p]

      Alias of the reverse direction of MeasureTheory.dLpNorm_pos.

      source
      def Mathlib.Meta.Positivity.evalDLpNorm :
      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.dLpNorm_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.dLpNorm_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.dL1Norm_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.dL1Norm_pow {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] {q : ℕ} (hq : q ≠ 0) (f : α → ℂ) :
        ‖f ^ q‖_[1] = ‖f‖_[↑q] ^ q
        source
        theorem MeasureTheory.dLpNorm_eq_dL1Norm_rpow {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] [RCLike 𝕜] {p : NNReal} (hp : p ≠ 0) (f : α → 𝕜) :
        ‖f‖_[↑p] = ‖fun (a : α) => ‖f a‖ ^ ↑p‖_[1] ^ (↑p)⁻¹
        source
        theorem MeasureTheory.dLpNorm_rpow' {𝕜 : Type u_2} {α : Type u_5} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Finite α] [RCLike 𝕜] {q : NNReal} {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (hq : q ≠ 0) (f : α → 𝕜) :
        ‖f‖_[p] ^ ↑q = ‖(fun (a : α) => ‖f a‖) ^ ↑q‖_[p / ↑q]
        source
        @[simp]
        theorem MeasureTheory.RCLike.dLpNorm_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.dLpNorm_coe_comp {α : Type u_5} {mα : MeasurableSpace α} (p : ENNReal) (f : α → ℝ) :
        ‖Complex.ofReal ∘ f‖_[p] = ‖f‖_[p]