Documentation

APAP.Prereqs.LpNorm.Weighted

Lp norms #

Weighted Lp norm #

source
noncomputable def wLpNorm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) (w : α → NNReal) (f : α → E) :
ℝ

The weighted Lp norm of a function.

Equations
Instances For
    source
    def «term‖_‖_[_,_]» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem wLpNorm_nonneg {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {w : α → NNReal} {f : α → E} :
      0 ≤ ‖f‖_[p, w]
      source
      @[simp]
      theorem wLpNorm_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} (w : α → NNReal) :
      ‖0‖_[p, w] = 0
      source
      @[simp]
      theorem wLpNorm_neg {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} (w : α → NNReal) (f : α → E) :
      ‖-f‖_[p, w] = ‖f‖_[p, w]
      source
      theorem wLpNorm_sub_comm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} (w : α → NNReal) (f g : α → E) :
      ‖f - g‖_[p, w] = ‖g - f‖_[p, w]
      source
      @[simp]
      theorem wLpNorm_one_eq_dLpNorm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) (f : α → E) :
      ‖f‖_[p, 1] = ‖f‖_[p]
      source
      @[simp]
      theorem wLpNorm_fun_one_eq_dLpNorm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal) (f : α → E) :
      ‖f‖_[p, fun (x : α) => 1] = ‖f‖_[p]
      source
      @[simp]
      theorem wLpNorm_exponent_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] (w : α → NNReal) (f : α → E) :
      ‖f‖_[0, w] = 0
      source
      @[simp]
      theorem wLpNorm_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {f : α → E} (w : α → NNReal) (hf : MeasureTheory.StronglyMeasurable f) :
      ‖fun (i : α) => ‖f i‖‖_[p, w] = ‖f‖_[p, w]
      source
      theorem wLpNorm_smul {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedField 𝕜] [NormedSpace 𝕜 E] (c : 𝕜) (f : α → E) (p : ENNReal) (w : α → NNReal) :
      ‖c • f‖_[p, w] = ↑‖c‖₊ * ‖f‖_[p, w]
      source
      theorem wLpNorm_nsmul {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) (f : α → E) (p : ENNReal) (w : α → NNReal) :
      ‖n • f‖_[p, w] = n • ‖f‖_[p, w]
      source
      @[simp]
      theorem wLpNorm_conj {α : Type u_1} [MeasurableSpace α] {p : ENNReal} {w : α → NNReal} {K : Type u_4} [RCLike K] (f : α → K) :
      ‖(starRingEnd (α → K)) f‖_[p, w] = ‖f‖_[p, w]
      source
      @[simp]
      theorem wLpNorm_const_right {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] (hp : p ≠ ⊤) (w : NNReal) (f : α → E) :
      ‖f‖_[p, Function.const α w] = ↑w ^ p.toReal⁻¹ * ‖f‖_[p]
      source
      @[simp]
      theorem wLpNorm_smul_right {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {w : α → NNReal} [Finite α] (hp : p ≠ ⊤) (c : NNReal) (f : α → E) :
      ‖f‖_[p, c • w] = ↑c ^ p.toReal⁻¹ * ‖f‖_[p, w]
      source
      theorem wLpNorm_eq_sum_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] [Fintype α] [DiscreteMeasurableSpace α] (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (w : α → NNReal) (f : α → E) :
      ‖f‖_[p, w] = (∑ i : α, w i • ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹
      source
      theorem wLpNorm_toNNReal_eq_sum_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [Finite α] [Fintype α] [DiscreteMeasurableSpace α] {p : ℝ} (hp : 0 < p) (w : α → NNReal) (f : α → E) :
      ‖f‖_[↑p.toNNReal, w] = (∑ i : α, w i • ‖f i‖ ^ p) ^ p⁻¹
      source
      theorem wLpNorm_rpow_eq_sum_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [Finite α] [Fintype α] [DiscreteMeasurableSpace α] {p : NNReal} (hp : p ≠ 0) (w : α → NNReal) (f : α → E) :
      ‖f‖_[↑p, w] ^ ↑p = ∑ i : α, w i • ‖f i‖ ^ ↑p
      source
      theorem wLpNorm_pow_eq_sum_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [Finite α] [Fintype α] [DiscreteMeasurableSpace α] {p : ℕ} (hp : p ≠ 0) (w : α → NNReal) (f : α → E) :
      ‖f‖_[↑p, w] ^ p = ∑ i : α, w i • ‖f i‖ ^ p
      source
      theorem wL1Norm_eq_sum_norm {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [Finite α] [Fintype α] [DiscreteMeasurableSpace α] (w : α → NNReal) (f : α → E) :
      ‖f‖_[1, w] = ∑ i : α, w i • ‖f i‖
      source
      theorem wLpNorm_mono_right {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p q : ENNReal} {w : α → NNReal} [Finite α] [Fintype α] [DiscreteMeasurableSpace α] (hw : ∑ i : α, ↑(w i) = 1) (hpq : p ≤ q) (f : α → E) :
      ‖f‖_[p, w] ≤ ‖f‖_[q, w]

      Monotonicity of weighted L^p norms in the exponent, for probability weights.

      source
      theorem wLpNorm_add_le {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] [DiscreteMeasurableSpace α] (hp : 1 ≤ p) (w : α → NNReal) (f g : α → E) :
      ‖f + g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w]
      source
      theorem wLpNorm_sub_le {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] [DiscreteMeasurableSpace α] (hp : 1 ≤ p) (w : α → NNReal) (f g : α → E) :
      ‖f - g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w]
      source
      theorem wLpNorm_le_wLpNorm_add_wLpNorm_sub' {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] [DiscreteMeasurableSpace α] (hp : 1 ≤ p) (w : α → NNReal) (f g : α → E) :
      ‖f‖_[p, w] ≤ ‖g‖_[p, w] + ‖f - g‖_[p, w]
      source
      theorem wLpNorm_le_wLpNorm_add_wLpNorm_sub {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] [DiscreteMeasurableSpace α] (hp : 1 ≤ p) (w : α → NNReal) (f g : α → E) :
      ‖f‖_[p, w] ≤ ‖g‖_[p, w] + ‖g - f‖_[p, w]
      source
      theorem wLpNorm_le_add_wLpNorm_add {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} [Finite α] [DiscreteMeasurableSpace α] (hp : 1 ≤ p) (w : α → NNReal) (f g : α → E) :
      ‖f‖_[p, w] ≤ ‖f + g‖_[p, w] + ‖g‖_[p, w]
      source
      theorem wLpNorm_sub_le_wLpNorm_sub_add_wLpNorm_sub {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {w : α → NNReal} {h : α → E} [Finite α] [DiscreteMeasurableSpace α] (hp : 1 ≤ p) (f g : α → E) :
      ‖f - h‖_[p, w] ≤ ‖f - g‖_[p, w] + ‖g - h‖_[p, w]
      source
      @[simp]
      theorem wLpNorm_one {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] {p : ENNReal} [Fintype α] (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (w : α → NNReal) :
      ‖1‖_[p, w] = ↑(∑ i : α, w i) ^ p.toReal⁻¹
      source
      theorem wLpNorm_mono {α : Type u_1} [MeasurableSpace α] [DiscreteMeasurableSpace α] {p : ENNReal} {w : α → NNReal} {f g : α → ℝ} [Finite α] (hf : 0 ≤ f) (hfg : f ≤ g) :
      ‖f‖_[p, w] ≤ ‖g‖_[p, w]
      source
      @[simp]
      theorem wLpNorm_translate {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [Finite α] [DiscreteMeasurableSpace α] {p : NNReal} {w : α → NNReal} [AddCommGroup α] [NormedAddCommGroup E] (a : α) (f : α → E) :
      ‖translate a f‖_[↑p, translate a w] = ‖f‖_[↑p, w]
      source
      def Mathlib.Meta.Positivity.evalWLpNorm :
      PositivityExt

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

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