Theorems · Theorem · measure theory

MeasureTheory.pow_mul_meas_ge_le_eLpNorm

∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} (μ : MeasureTheory.Measure α),
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → ε'},
        MeasureTheory.AEStronglyMeasurable f μ →
          ∀ (ε : ENNReal), (ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm