measure_closedBall_le_integral — Mathlib

English

The real measure of a closed ball with outer radius r is positive: μ.real(closedBall(c,r)) > 0.

Русский

Положительная мера real замкнутого шара с радиусом r: μ.real(closedBall(c,r)) > 0.

LaTeX

$$$ \mu.real(\mathrm{closedBall}(c,r)) > 0 $$$

Lean4

theorem measure_closedBall_le_integral : μ.real (closedBall c f.rIn) ≤ ∫ x, f x ∂μ := by
  calc
    μ.real (closedBall c f.rIn) = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
    _ = ∫ x in closedBall c f.rIn, f x ∂μ :=
      (setIntegral_congr_fun measurableSet_closedBall (fun x hx ↦ (one_of_mem_closedBall f hx).symm))
    _ ≤ ∫ x, f x ∂μ := setIntegral_le_integral f.integrable (Eventually.of_forall (fun x ↦ f.nonneg))

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