Integration with filters

Emanuele Bottazzi and Monroe Eskew

The paper concerns measures over [0,∞].

In Lean this interval is known as the type ENNReal, the extended nonnegative reals. The number ∞ is represented as ⊤.

Here we explore the arithmetic of this type.

theorem iReal : (-1) ^ (1 / 2) = 0