## Stream: Beginner Questions

### Topic: Integration

#### 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?

#### Yosuke Ito (Apr 29 2023 at 02:52):

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

#### 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 `∞`.

#### 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)"
``````

#### Manuel Eberl (May 04 2023 at 11:59):

They're all pretty much equivalent.

#### 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)

#### 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.

#### Manuel Eberl (May 04 2023 at 12:00):

(`lebesgue = completion lborel`)

#### 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: Sep 11 2024 at 16:22 UTC