integral of piecewise constant function

Stream: Is there code for X?

[Kevin Buzzard]

At Xena. We just tried to do this:

import tactic
import measure_theory.interval_integral

open set

noncomputable def f (x : ℝ) := if x ≤ 1/37 then 37 else 0

noncomputable def a : ℝ := ∫ x in 0..1, f x

example : a = 1 := sorry

but failed miserably. I don't know how to steer integrals at all. We managed to split the integral up into two pieces but then we had to prove that the pieces were interval_integrable; we constructed a measure on the reals which was supported on $[0,1/37]$ but then couldn't integrate f because it wasn't constant on the entire reals. It is equal to a constant function modulo a set of measure zero but to prove this we then had to prove was measurable. Maybe we could persevere but I thought it was easier to just ask.

[Mario Carneiro]

It's a simple function, so you could use the simple function integral

[Kevin Buzzard]

So 150 lines later we have computed the lintegral of a related ennreal-valued function :-/

[Kevin Buzzard]

This is harder than it looks, even when you look at it a bit and note that it's hard

[Bryan Gin-ge Chen]

Are we missing API? Or automation? (a measurable tactic?)

[Jason KY.]

I think one problem was we used pnat in the definition which was not easy to work with (kept needing to coerce to ennreal and back)

[Kevin Buzzard]

I don't know the API (nobody did, we were all looking at it for the first time, Shing and Bhavik and Jason were involved). Switching from reals to ennreals (note there's no coercion in either direction) was a bit of a shock. We were trying to do something more general involving pnats which didn't help. I still don't know how to compute the integral because I don't know how to relate it to the lintegral of the ennreal-valued function. Yury has done a ton of stuff but I don't really know how to steer it. I explained the trouble I had when trying to compute it directly, but perhaps Yury or someone else who knows this part of the library might be able to sail through it.

[Yury G. Kudryashov]

I'll try to add missing lemmas in a few days. I have a few deadlines on Nov. 30 and Dec. 1, so please ping me on Dec. 2.

[Kevin Buzzard]

This is not high priority! As usual in Xena it came from trying to do random undergraduate maths in Lean.

[Jacques Carette]

Good representations of piecewise functions are very tricky. I've written a couple of papers about that, and I was only scratching the surface. The problems only arise when you start to worry about efficiency, undefinedness or decidability - if you ignore them, then it's not that big a deal.