setLIntegral_le_meas — Mathlib

English

For s,t measurable and f constrained by 1 on s versus t, the set L-integral over s is bounded by μ t.

Русский

Для измеримых s,t и ограничений f на s по 1 ≤ f ≤ 1 на t интеграл по s ограничен μ t.

LaTeX

$$$$ \int⁻ a in s, f a ∂μ ≤ μ t, \text{ under suitable conditions}. $$$$

Lean4

theorem setLIntegral_le_meas {s t : Set α} (hs : MeasurableSet s) {f : α → ℝ≥0∞} (hf : ∀ a ∈ s, a ∈ t → f a ≤ 1)
    (hf' : ∀ a ∈ s, a ∉ t → f a = 0) : ∫⁻ a in s, f a ∂μ ≤ μ t :=
  by
  rw [← lintegral_indicator hs]
  refine lintegral_le_meas (fun a ↦ ?_) (by simp_all)
  by_cases has : a ∈ s <;> [by_cases hat : a ∈ t; skip] <;> simp [*]

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