Lp norms

Weighted Lp norm

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

• ‖f‖_[p, w] = MeasureTheory.lpNorm f p (MeasureTheory.Measure.sum fun (i : α) => w i • MeasureTheory.Measure.dirac i)

def «term‖_‖_[_,_]» : Lean.ParserDescr

Equations

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

@[simp]

theorem wLpNorm_nonneg {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {w : α → NNReal} {f : α → E} : 0 ≤ ‖f‖_[p, w]

@[simp]

theorem wLpNorm_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} (w : α → NNReal) : ‖0‖_[p, w] = 0

@[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]

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]

@[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]

@[simp]

theorem wLpNorm_exponent_zero {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] (w : α → NNReal) (f : α → E) : ‖f‖_[0, w] = 0

@[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]

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]

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]

@[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]

@[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]

@[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]

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⁻¹

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⁻¹

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

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

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‖

theorem wLpNorm_mono_right {α : Type u_1} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p q : ENNReal} [Finite α] [DiscreteMeasurableSpace α] (hpq : p ≤ q) (w : α → NNReal) (f : α → E) : ‖f‖_[p, w] ≤ ‖f‖_[q, w]

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]

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]

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]

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]

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]

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]

@[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⁻¹

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]

@[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]

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.