Inner product

@[simp]

theorem RCLike.wInner_one_self {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] {x✝ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → 𝕜) : wInner 1 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] = wInner 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 : ι → ℝ) : wInner 1 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] = RCLike.wInner 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] : RCLike.wInner 1 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 : α → ℝ) : |RCLike.wInner 1 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 : α → 𝕜) : ↑‖RCLike.wInner 1 f g‖₊ ≤ RCLike.wInner 1 (fun (a : α) => ‖f a‖) fun (a : α) => ‖g a‖

theorem MeasureTheory.nnnorm_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] : ↑‖RCLike.wInner 1 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) (hr₀ : r ≠ 0) [hpqr : p.HolderTriple q r] : ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q]

Hölder's inequality, binary case.

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