Inner product

@[simp]

theorem RCLike.wInner_cWeight_self {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → 𝕜) : wInner cWeight f f = ↑‖f‖ₙ_[2] ^ 2

theorem RCLike.cL1Norm_mul {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f g : ι → 𝕜) : ‖f * g‖ₙ_[1] = wInner cWeight (fun (i : ι) => ‖f i‖) fun (i : ι) => ‖g i‖

theorem RCLike.wInner_cWeight_le_cL2Norm_mul_cL2Norm {ι : Type u_1} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f g : ι → ℝ) : wInner cWeight f g ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2]

Cauchy-Schwarz inequality

Hölder inequality

theorem MeasureTheory.cL1Norm_mul_of_nonneg {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {f g : α → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖ₙ_[1] = RCLike.wInner RCLike.cWeight f g

theorem MeasureTheory.wInner_cWeight_le_cLpNorm_mul_cLpNorm {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {f g : α → ℝ} (p q : ENNReal) [p.HolderConjugate q] : RCLike.wInner RCLike.cWeight f g ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.abs_wInner_cWeight_le_dLpNorm_mul_dLpNorm {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {f g : α → ℝ} (p q : ENNReal) [p.HolderConjugate q] : |RCLike.wInner RCLike.cWeight f g| ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.norm_wInner_cWeight_le {𝕜 : Type u_3} {α : Type u_4} [Fintype α] [RCLike 𝕜] (f g : α → 𝕜) : ↑‖RCLike.wInner RCLike.cWeight f g‖₊ ≤ RCLike.wInner RCLike.cWeight (fun (a : α) => ‖f a‖) fun (a : α) => ‖g a‖

theorem MeasureTheory.norm_wInner_cWeight_le_dLpNorm_mul_dLpNorm {𝕜 : Type u_3} {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike 𝕜] {f g : α → 𝕜} (p q : ENNReal) [p.HolderConjugate q] : ↑‖RCLike.wInner RCLike.cWeight f g‖₊ ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.cLpNorm_mul_le {𝕜 : Type u_3} {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [RCLike 𝕜] {r : ENNReal} {f g : α → 𝕜} [Finite α] (p q : ENNReal) (hr₀ : r ≠ 0) [hpqr : p.HolderTriple q r] : ‖f * g‖ₙ_[r] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.cL1Norm_mul_le {𝕜 : Type u_3} {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [RCLike 𝕜] {f g : α → 𝕜} [Finite α] (p q : ENNReal) [hpq : p.HolderConjugate q] : ‖f * g‖ₙ_[1] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.cLpNorm_prod_le {𝕜 : Type u_3} {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [RCLike 𝕜] [Finite α] {ι : Type u_5} {s : Finset ι} (hs : s.Nonempty) {p : ι → NNReal} (hp : ∀ (i : ι), p i ≠ 0) (q : NNReal) (hpq : ∑ i ∈ s, (↑(p i))⁻¹ = (↑q)⁻¹) (f : ι → α → 𝕜) : ‖∏ i ∈ s, f i‖ₙ_[↑q] ≤ ∏ i ∈ s, ‖f i‖ₙ_[↑(p i)]

Hölder's inequality, finitary case.