English
For a nonnegative measurable f and ε > 0, ε · μ{x : ε ≤ f(x)} ≤ ∫ f dμ.
Русский
Для неотрицательной измеримой функции f и ε > 0 выполнено неравенство Маркова: ε · μ({x : ε ≤ f(x)}) ≤ ∫ f dμ.
LaTeX
$$$\\varepsilon \\cdot \\mu\\{x : \\varepsilon \\le f(x)\\} \\le \\int x\\, f(x)\\, d\\mu$$$
Lean4
/-- **Markov's inequality** also known as **Chebyshev's first inequality**. -/
theorem mul_meas_ge_le_integral_of_nonneg {f : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f) (hf_int : Integrable f μ) (ε : ℝ) :
ε * μ.real {x | ε ≤ f x} ≤ ∫ x, f x ∂μ :=
by
rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ
· simpa [measureReal_def, hμ] using integral_nonneg_of_ae hf_nonneg
· have := Fact.mk hμ
calc
ε * μ.real {x | ε ≤ f x} = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
_ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
(integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici)
_ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int
