Inner product

@[simp]

theorem RCLike.wInner_one_self {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] {x✝ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → 𝕜) : ⟪f, f⟫_[𝕜] = ↑‖f‖_[2] ^ 2

theorem RCLike.dL1Norm_mul {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f g : ι → 𝕜) : ‖f * g‖_[1] = ⟪fun (i : ι) => ‖f i‖, fun (i : ι) => ‖g i‖⟫_[ℝ]

theorem RCLike.wInner_one_le_dL2Norm_mul_dL2Norm {ι : Type u_1} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f g : ι → ℝ) : ⟪f, g⟫_[ℝ] ≤ ‖f‖_[2] * ‖g‖_[2]

Cauchy-Schwarz inequality

Hölder inequality

theorem MeasureTheory.dL1Norm_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_one_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.abs_wInner_one_le_dLpNorm_mul_dLpNorm {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {p q : ENNReal} [p.HolderConjugate q] (f g : α → ℝ) : |⟪f, g⟫_[ℝ]| ≤ ‖f‖_[p] * ‖g‖_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.norm_wInner_one_le {𝕜 : Type u_2} {α : Type u_4} [Fintype α] [RCLike 𝕜] (f g : α → 𝕜) : ‖⟪f, g⟫_[𝕜]‖ ≤ ⟪fun (a : α) => ‖f a‖, fun (a : α) => ‖g a‖⟫_[ℝ]

theorem MeasureTheory.norm_wInner_one_le_dLpNorm_mul_dLpNorm {𝕜 : Type u_2} {α : 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.dLpNorm_mul_le {𝕜 : Type u_2} {α : Type u_4} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [RCLike 𝕜] {r : ENNReal} {f g : α → 𝕜} [Finite α] (p q : ENNReal) [p.HolderTriple q r] : ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q]

Hölder's inequality, binary case.

theorem MeasureTheory.dLpNorm_prod_le {𝕜 : Type u_2} {α : 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.