Christian Zimmerer (Apr 26 2023 at 19:56): 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)"
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: Apr 27 2024 at 12:25 UTC