English
A Lebesgue Markov-type inequality for lintegral: for f,g: α→ℝ≥0∞ with hle ≤ᵐ g and hg AEMeasurable, and ε ≥ 0, the inequality ∫ f dμ + ε μ{ x | f x + ε ≤ g x } ≤ ∫ g dμ holds, with a measurability condition.
Русский
Неравенство Маркова для линеграла: для f,g с условиями а Меасуребл, и ε≥0, выполняется ∫ f + ε μ{ x | f(x)+ε ≤ g(x) } ≤ ∫ g.
LaTeX
$$$$ \int⁻ x, f x ∂μ + ε \cdot μ\{ x \mid f x + ε ≤ g x \} ≤ \int⁻ x, g x ∂μ. $$$$
Lean4
/-- A version of **Markov's inequality** for two functions. It doesn't follow from the standard
Markov's inequality because we only assume measurability of `g`, not `f`. -/
theorem lintegral_add_mul_meas_add_le_le_lintegral {f g : α → ℝ≥0∞} (hle : f ≤ᵐ[μ] g) (hg : AEMeasurable g μ)
(ε : ℝ≥0∞) : ∫⁻ a, f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ a, g a ∂μ :=
by
rcases exists_measurable_le_lintegral_eq μ f with ⟨φ, hφm, hφ_le, hφ_eq⟩
calc
∫⁻ x, f x ∂μ + ε * μ {x | f x + ε ≤ g x} = ∫⁻ x, φ x ∂μ + ε * μ {x | f x + ε ≤ g x} := by rw [hφ_eq]
_ ≤ ∫⁻ x, φ x ∂μ + ε * μ {x | φ x + ε ≤ g x} := by
gcongr
exact hφ_le _
_ = ∫⁻ x, φ x + indicator {x | φ x + ε ≤ g x} (fun _ => ε) x ∂μ :=
by
rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]
exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable
_ ≤ ∫⁻ x, g x ∂μ := lintegral_mono_ae (hle.mono fun x hx₁ => ?_)
simp only [indicator_apply]; split_ifs with hx₂
exacts [hx₂, (add_zero _).trans_le <| (hφ_le x).trans hx₁]
