Inner product

@[simp]

theorem RCLike.wInner_cWeight_self {ι : Type u_1} {𝕜 : Type u_3} [Fintype ι] [RCLike 𝕜] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → 𝕜) : ⟪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] = ⟪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 : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2]

Cauchy-Schwarz inequality

Hölder inequality

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_of_nonneg {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {f g : α → ℝ} (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖ₙ_[1] = ⟪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] : ⟪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] : |⟪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 : α → 𝕜) : ↑‖⟪f, g⟫ₙ_[𝕜]‖₊ ≤ ⟪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] : ↑‖⟪f, g⟫ₙ_[𝕜]‖₊ ≤ ‖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.