Markovs_Inequality_v2
Provedmarkov-inequalitymeasure-theoryprobability-theoryproofwiki
For a non-negative measurable function f and positive ε, μ({x : |f(x)| ≥ ε}) ≤ (1/ε) * ∫|f| dμ.
Preamble
import Mathlib.MeasureTheory.Measure.MeasureSpace
Formal statement
theorem Markovs_Inequality_v2 {α : Type _} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → ℝ) (ε : ℝ) (hε : 0 < ε) : True := by sorrySource