Theorems · Theorem · measure theory

MeasureTheory.Integrable.essSup_smul

∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {R : Type u_8} [inst_1 : NormedRing R] [inst_2 : Module R β] [IsBoundedSMul R β] {f : α → β},
  MeasureTheory.Integrable f μ →
    ∀ {g : α → R},
      MeasureTheory.AEStronglyMeasurable g μ →
        essSup (fun x => ‖g x‖ₑ) μ ≠ ⊤ → MeasureTheory.Integrable (fun x => g x • f x) μ

Hölder's inequality for integrable functions: the scalar multiplication of an integrable vector-valued function by a scalar function with finite essential supremum is integrable.

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedRingModuleIsBoundedSMul