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?

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

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

.

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

They're all pretty much equivalent.

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

You could also just use `lborel`

instead of `lebesgue`

here because it doesn't make a difference in this case.

(`lebesgue = completion lborel`

)

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: Feb 27 2024 at 08:17 UTC