Zulip Chat Archive

Stream: Is there code for X?

Topic: integral of piecewise constant function


Kevin Buzzard (Nov 26 2020 at 19:07):

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][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 (Nov 26 2020 at 19:13):

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

Kevin Buzzard (Nov 26 2020 at 22:35):

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

Kevin Buzzard (Nov 26 2020 at 22:35):

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

Bryan Gin-ge Chen (Nov 26 2020 at 22:39):

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

Jason KY. (Nov 26 2020 at 22:56):

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 (Nov 26 2020 at 22:58):

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 (Nov 27 2020 at 02:16):

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 (Nov 27 2020 at 08:08):

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

Jacques Carette (Nov 30 2020 at 16:20):

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.


Last updated: Dec 20 2023 at 11:08 UTC