Zulip Chat Archive

Stream: Is there code for X?

Topic: integral of piecewise constant function

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 26 2020 at 19:13):

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

view this post on Zulip Kevin Buzzard (Nov 26 2020 at 22:35):

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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 26 2020 at 22:39):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 16 2021 at 05:21 UTC