integral_le_measure_closedBall — Mathlib

English

For any bump f, ∫ f ≤ μ.real(closedBall(c,rOut)).

Русский

Для функции бу́мпы выполняется интеграл ≤ μ.real(замкнутый шар(c, rOut)).

LaTeX

$$$ \int_E f(x) \, d\mu(x) \le \mu.real(\mathrm{closedBall}(c,f.rOut)) $$$

Lean4

theorem integral_le_measure_closedBall : ∫ x, f x ∂μ ≤ μ.real (closedBall c f.rOut) := by
  calc
    ∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ :=
      by
      apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
      apply f.zero_of_le_dist (le_of_lt _)
      simpa using hx
    _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ :=
      by
      apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
      simp [measure_closedBall_lt_top]
    _ = μ.real (closedBall c f.rOut) := by simp

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