MeasureTheory.MeasureSpace.Lebesgue

このファイルでは下ルベーグ積分の定義を行います.

コード元 MeasureTheory.MeasurableSpace.Lebesgue

/-- The **lower Lebesgue integral** of a function `f` with respect to a measure `μ`. -/
irreducible_def lintegral {_ : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) : ℝ≥0∞ :=
  ⨆ (g : α →ₛ ℝ≥0∞) (_ : ⇑g ≤ f), g.lintegral μ

g ≤ fを満たす単関数gの中で積分が最大となるものをlintegralで定義します.

@[inherit_doc MeasureTheory.lintegral]
notation3 "∫⁻ "(...)", "r:60:(scoped f => f)" ∂"μ:70 => lintegral μ r

@[inherit_doc MeasureTheory.lintegral]
notation3 "∫⁻ "(...)", "r:60:(scoped f => lintegral volume f) => r

lintegralは上記のように積分の記法でも書けます.