Lp norms

Indicator

theorem MeasureTheory.dLpNorm_rpow_indicate {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {p : NNReal} (hp : p ≠ 0) (s : Finset ι) : ‖𝟭 s‖_[↑p] ^ ↑p = ↑s.card

theorem MeasureTheory.dLpNorm_indicate {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {p : NNReal} (hp : p ≠ 0) (s : Finset ι) : ‖𝟭 s‖_[↑p] = ↑s.card ^ (↑p)⁻¹

theorem MeasureTheory.dLpNorm_pow_indicate {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {p : ℕ} (hp : p ≠ 0) (s : Finset ι) : ‖𝟭 s‖_[↑p] ^ ↑p = ↑s.card

theorem MeasureTheory.dL2Norm_sq_indicate {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] (s : Finset ι) : ‖𝟭 s‖_[2] ^ 2 = ↑s.card

@[simp]

theorem MeasureTheory.dL2Norm_indicate {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] (s : Finset ι) : ‖𝟭 s‖_[2] = √↑s.card

@[simp]

theorem MeasureTheory.dL1Norm_indicate {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] (s : Finset ι) : ‖𝟭 s‖_[1] = ↑s.card

theorem MeasureTheory.dLpNorm_mu {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {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] [DecidableEq ι] {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] [DecidableEq ι] {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] [DecidableEq ι] {s : Finset ι} : ‖mu s‖_[1] ≤ 1

@[simp]

theorem MeasureTheory.dL2Norm_mu {ι : Type u_1} {R : Type u_5} [Finite ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] [RCLike R] [DecidableEq ι] {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]