integral_eq_integral_meas_le — Mathlib

English

The standard Cavalieri-type formula: ∫ f dμ = ∫_{0}^{∞} μ{a: f(a) ≥ t} dt, for nonnegative measurable f.

Русский

Стандартная формула Cavalieri: ∫ f dμ = ∫_{0}^{∞} μ{a: f(a) ≥ t} dt, для неотрицательной измеримой f.

LaTeX

$$$$ \\int f \\, d\\mu = \\int_{0}^{\\infty} \\mu\\{a : f(a) \\ge t\\} \\, dt. $$$$

Lean4

theorem integral_eq_integral_meas_le (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
    ∫ ω, f ω ∂μ = ∫ t in Set.Ioi 0, μ.real {a : α | t ≤ f a} :=
  by
  rw [Integrable.integral_eq_integral_meas_lt f_intble f_nn]
  apply integral_congr_ae
  filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht
  exact congrArg ENNReal.toReal ht.symm

Похожие утверждения