Stream: Beginner Questions

Topic: Integration


view this post on Zulip Christian Zimmerer (Apr 26 2023 at 19:56):

I'm trying to prove that the integral of a constant function (λx. c) over {a..<b} is equal to (b-a)*c. Now I'm trying to use HOL-Analysis.Interval_Integral and have defined the lemma. How would I go about proving this?

view this post on Zulip Yosuke Ito (Apr 29 2023 at 02:52):

Not sure, but maybe the lemmas 'integral_completion' and 'interval_integral_const' can solve this.

view this post on Zulip Manuel Eberl (May 04 2023 at 11:57):

Christian Zimmerer said:

I'm trying to prove that the integral of a constant function (λx. c) over {a..<b} is equal to (b-a)*c. Now I'm trying to use HOL-Analysis.Interval_Integral and have defined the lemma. How would I go about proving this?

Well that is definitely not true. That's the integral over c from -∞ to .

view this post on Zulip Manuel Eberl (May 04 2023 at 11:59):

If you want to use the Lebesgue integral you can one of the following:

term "set_lebesgue_integral lebesgue {a..<b} (λ_. c) = T"
term "lebesgue_integral lebesgue (λx. c * indicator {a..<b} x) = T"
term "interval_lebesgue_integral lebesgue (ereal a) (ereal b) (λ_. c :: real)"

view this post on Zulip Manuel Eberl (May 04 2023 at 11:59):

They're all pretty much equivalent.

view this post on Zulip Manuel Eberl (May 04 2023 at 12:00):

(and there's some nice notation defined as well, but you'll see that yourself when you type them in)

view this post on Zulip Manuel Eberl (May 04 2023 at 12:00):

You could also just use lborel instead of lebesgue here because it doesn't make a difference in this case.

view this post on Zulip Manuel Eberl (May 04 2023 at 12:00):

(lebesgue = completion lborel)

view this post on Zulip Manuel Eberl (May 04 2023 at 12:02):

You can also use the Henstock–Kurzweil integral though:

term "((λx. c) has_integral (c * (a - b))) {a..<b}"
term "integral {a..<b} (λx. c) = c * (a - b)"

It is convertible to the Lebesgue integral.


Last updated: Jun 20 2024 at 08:21 UTC