Theorems · Theorem · functional analysis

MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm

∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.Measure α} {f : α → E} {g : α → F}
  {p q r : ENNReal},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (b : E → F → G) (c : NNReal),
        (∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) →
          ∀ [hpqr : p.HolderTriple q r],
            MeasureTheory.eLpNorm (fun x => b (f x) (g x)) r μ ≤
              ↑c * MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g q μ

Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation fun x => b (f x) (g x).

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Cited by

4 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupENNReal.HolderTriple