MeasureTheory.mul_meas_ge_le_pow_snorm'

theorem MeasureTheory.mul_meas_ge_le_pow_snorm' : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] {p : ENNReal} (μ : MeasureTheory.Measure α) {f : α → E}, p ≠ 0 → p ≠ ⊤ → MeasureTheory.AEStronglyMeasurable f μ → ∀ (ε : ENNReal), ε ^ p.toReal * ↑↑μ {x | ε ≤ ↑‖f x‖₊} ≤ MeasureTheory.snorm f p μ ^ p.toReal

This theorem is a version of the Chebyshev-Markov inequality using Lp-norms. It states that for a measure space `α` and a normed additive commutative group `E`, given a measure `μ` on `α` and a function `f` from `α` to `E`, if `f` is almost everywhere strongly measurable with respect to `μ` and `p` is a non-zero extended nonnegative real number different from `∞`, then for any extended nonnegative real number `ε`, the product of `ε` raised to the power of `p` and the measure of the set of `α` where `ε` is less than or equal to the nonnegative real part of the norm of `f(x)` is less than or equal to the `ℒp` seminorm of `f` with respect to measure `μ` raised to the power `p`.

More concisely: For a measure space `α`, a normed additive commutative group `E`, a measure `μ`, a strongly measurable function `f: α → E`, and a non-zero extended real number `p`, if the `ℒp` seminorm of `f` with respect to `μ` is finite, then for any extended nonnegative real number `ε`, the measure of the set where the nonnegative real part of the norm of `f(x)` is less than `ε` is less than or equal to `(ε^-p) * (∫ |f(x)|^p dμ)`.