integral_coe_le_of_lintegral_coe_le

English

If ∫⁻ f ≤ b for f: α → ℝ≥0 with Integrable, then ∫ f ≤ b (with b interpreted as a real bound).

Русский

Если ∫⁻ f ≤ b для f: α → ℝ≥0 с интегрируемостью, то ∫ f ≤ b (граница в действительных числах).

LaTeX

$$$\\\\int a \\, (f(a) \\,: \\, ℝ) \\, d\\\\mu \\\\le b \\\\Leftarrow \\\\int⁻ a \\, f(a) \\, d\\\\mu \\\\le b$$$

Lean4

theorem integral_coe_le_of_lintegral_coe_le {f : α → ℝ≥0} {b : ℝ≥0} (h : ∫⁻ a, f a ∂μ ≤ b) : ∫ a, (f a : ℝ) ∂μ ≤ b :=
  by
  by_cases hf : Integrable (fun a => (f a : ℝ)) μ
  · exact (lintegral_coe_le_coe_iff_integral_le hf).1 h
  · rw [integral_undef hf]; exact b.2

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