Unpacking the definition Lebesgue integral

Stream: new members

[Peter Hansen]

In Mathlib the Lebesgue integral is defined as

irreducible_def lintegral {_ : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) : ℝ≥0∞ :=
  ⨆ (g : α →ₛ ℝ≥0∞) (_ : ⇑g ≤ f), g.lintegral μ

I’m familiar with the mathematical definition and I can see the resemblance. But I would like to really understand why the Lean definition is correct.

By clicking on the supremum symbol, I get the following explanation

-- `⨆ i, f i` : `iSup f`, the supremum of the range of `f`;

where

def iSup [SupSet α] {ι} (s : ι → α) : α :=
  sSup (range s)

and further

notation3 "⨆ "(...)", "r:60:(scoped f => iSup f) => r

I having trouble understanding how to interpret the notation declaration. It looks like iSup takes a function as a single argument, so how does the indexing i come into the picture? And what is f and iin the Lean definition of the integral? I'm sorry if I sound incoherent, but I find it so confusing that I don't know where to start.

[Sebastien Gouezel]

The notation means: take the supremum over all simple functions g which are bounded above by f of the integral of g (where the integral of a simple function is in fact just a sum). There is a subtelty, though, that there is a double supremum. It unfolds to:

⨆ (g : α →ₛ ℝ≥0∞), (⨆ (H : ⇑g ≤ f), g.lintegral μ)

Let's first have a look at the second term ⨆ (H : ⇑g ≤ f), g.lintegral μ. If g is bounded by f, it is a supremum over a single index (the proposition that g is bounded by f) of the quantity g.lintegral μ, so it will just reduce to g.lintegral μ. On the other hand, if g is not bounded by f, it is a supremum over the empty set, i.e., 0 (and will therefore not play any role in the overall supremum).

Now, the outermost supremum is indeed also of the form ⨆ i, F i, where the indexing space is the space of all simple functions (that's why we use the letter g instead of i, as it is more evocative), and the function F maps g to ⨆ (H : ⇑g ≤ f), g.lintegral μ, i.e., 0 if g is not bounded by f and the integral of g otherwise.

[Peter Hansen]

Thank you for taking your time to give such a thorough answer. I think I get it now :) I had to reread a couple of times to really appreciate it. From the idea of the nested supremum, I made by own (very ugly) definition of the integral as follows:

def lintegral {_ : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) : ℝ≥0∞ :=
  ⨆ (g : α →ₛ ℝ≥0∞) (_ : ⇑g ≤ f), g.lintegral μ

def mylintegral {_ : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) : ℝ≥0∞ :=
  iSup (fun (g : α →ₛ ℝ≥0∞) => iSup (fun (_ : ⇑g ≤ f) => SimpleFunc.lintegral g μ))

example {_ : MeasurableSpace α} (μ : Measure α) (f : α → ℝ≥0∞) :
  mylintegral μ f = lintegral μ f := by rfl

It at least helped myself better understand what we were indexing over. I guess part of what confused me is the use g.lintegral notation, that combines the function and index intro one.