English
If the positive part of f above a threshold R has positive measure and is integrable with a bound C, then the integral over {f > R} is strictly greater than R times its measure.
Русский
Если подмножество {x: f(x) > R} имеет положительную меру и интегрируемо с ограничением C, то интеграл больше порога R на этой мере.
LaTeX
$$$$ \\mu_\\mathbb{R}(\\{x: R < f(x)\\}) \\cdot R < \\int_{\\{x: R < f(x)\\}} f(x) \\, d\\mu(x) $$$$
Lean4
theorem setIntegral_gt_gt {R : ℝ} {f : X → ℝ} (hR : 0 ≤ R) (hfint : IntegrableOn f {x | ↑R < f x} μ)
(hμ : μ {x | ↑R < f x} ≠ 0) : μ.real {x | ↑R < f x} * R < ∫ x in {x | ↑R < f x}, f x ∂μ :=
by
have : IntegrableOn (fun _ => R) {x | ↑R < f x} μ :=
by
refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_
simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx)]
exact le_of_lt hx
rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
setIntegral_pos_iff_support_of_nonneg_ae]
· rw [← zero_lt_iff] at hμ
rwa [Set.inter_eq_self_of_subset_right]
exact fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx)
· rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]
· exact Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx
· exact nullMeasurableSet_le aemeasurable_zero (hfint.1.aemeasurable.sub aemeasurable_const)
· exact Integrable.sub hfint this
