Lp norms

theorem MeasureTheory.cLpNorm_pow_eq_card_inv_mul_dLpNorm_pow {ι : Type u_1} {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [Fintype ι] {n : ℕ} (hn₀ : n ≠ 0) (f : ι → ℂ) : ‖f‖ₙ_[↑n] ^ n = (↑(Fintype.card ι))⁻¹ * ‖f‖_[↑n] ^ n

Indicator

theorem MeasureTheory.dLpNorm_rpow_indicator_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {p : NNReal} (hp : p ≠ 0) (s : Finset ι) : ‖(↑s).indicator fun (x : ι) => 1‖_[↑p] ^ ↑p = ↑s.card

theorem MeasureTheory.dLpNorm_indicator_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {p : NNReal} (hp : p ≠ 0) (s : Finset ι) : ‖(↑s).indicator fun (x : ι) => 1‖_[↑p] = ↑s.card ^ (↑p)⁻¹

theorem MeasureTheory.dLpNorm_pow_indicator_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {p : ℕ} (hp : p ≠ 0) (s : Finset ι) : ‖(↑s).indicator fun (x : ι) => 1‖_[↑p] ^ ↑p = ↑s.card

theorem MeasureTheory.dL2Norm_sq_indicator_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] (s : Finset ι) : ‖(↑s).indicator fun (x : ι) => 1‖_[2] ^ 2 = ↑s.card

@[simp]

theorem MeasureTheory.dL2Norm_indicator_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] (s : Finset ι) : ‖(↑s).indicator fun (x : ι) => 1‖_[2] = √↑s.card

@[simp]

theorem MeasureTheory.dL1Norm_indicator_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] (s : Finset ι) : ‖(↑s).indicator fun (x : ι) => 1‖_[1] = ↑s.card

theorem MeasureTheory.dLpNorm_mu {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {s : Finset ι} {p : NNReal} (hp : 1 ≤ p) (hs : s.Nonempty) : ‖mu s‖_[↑p] = ↑s.card ^ ((↑p)⁻¹ - 1)

theorem MeasureTheory.dLpNorm_mu_le {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {s : Finset ι} {p : NNReal} (hp : 1 ≤ p) : ‖mu s‖_[↑p] ≤ ↑s.card ^ (↑p⁻¹ - 1)

@[simp]

theorem MeasureTheory.dL1Norm_mu {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {s : Finset ι} (hs : s.Nonempty) : ‖mu s‖_[1] = 1

theorem MeasureTheory.dL1Norm_mu_le_one {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {s : Finset ι} : ‖mu s‖_[1] ≤ 1

@[simp]

theorem MeasureTheory.dL2Norm_mu {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] {s : Finset ι} (hs : s.Nonempty) : ‖mu s‖_[2] = ↑s.card ^ (-2⁻¹)

Translation

@[simp]

theorem MeasureTheory.dLpNorm_translate {G : Type u_2} {E : Type u_4} {mG : MeasurableSpace G} [DiscreteMeasurableSpace G] [AddCommGroup G] [Finite G] {p : ENNReal} [NormedAddCommGroup E] (a : G) (f : G → E) : ‖translate a f‖_[p] = ‖f‖_[p]

@[simp]

theorem MeasureTheory.dLpNorm_conjneg {G : Type u_2} {E : Type u_4} {mG : MeasurableSpace G} [DiscreteMeasurableSpace G] [AddCommGroup G] [Finite G] {p : ENNReal} [RCLike E] (f : G → E) : ‖conjneg f‖_[p] = ‖f‖_[p]

theorem MeasureTheory.dLpNorm_translate_sum_sub_le {G : Type u_2} {E : Type u_4} {mG : MeasurableSpace G} [DiscreteMeasurableSpace G] [AddCommGroup G] [Finite G] {p : ENNReal} [NormedAddCommGroup E] (hp : 1 ≤ p) {ι : Type u_6} (s : Finset ι) (a : ι → G) (f : G → E) : ‖translate (∑ i ∈ s, a i) f - f‖_[p] ≤ ∑ i ∈ s, ‖translate (a i) f - f‖_[p]