Michael Soegtrop (Oct 21 2022 at 12:39): Michael Soegtrop (Oct 21 2022 at 12:39):I want to integrate a rather intricate piecewise mostly linear and in a few places rational function on [-1,1]^4 - given as a recursive gallina function which always terminates in a few steps and in total there are about 30 pieces. As far as I understand the measure theory in mathcomp-analysis is R^1. Is this correct?
If so I wonder if you have suggestions what else I could try. Coquelicot has parametric integrals, but I don't see how this gets me beyond R^2.
Zachary Stone (Oct 21 2022 at 14:49):I did not write the measure stuff, so someone should correct me if I'm wrong. But the measure theory should be quite generic (with regard to the domains of integrals). Integrating from R^4 -> \bar R (the extended reals) should be supported. If all goes well, the measure of R^4 will be (canonically) inferred thanks to HB.instance Definition prod_salgebra_mixin := ... in measure.v. And you can compute the integral one dimension at a time thanks to the Fubini machinery. I'd be quite curious to see how far you can get with the integral machinery here.
Michael Soegtrop (Oct 21 2022 at 15:08):@Zachary Stone : thanks - looking at it again with your pointers will hopefully lift the fog.
Michael Soegtrop (Oct 21 2022 at 15:26):Btw.: Looking if R^n measure theory is supported I stopped here (https://github.com/math-comp/analysis/blob/master/theories/lebesgue_measure.v). The definition of the Lebesgue measure seems from the documentation header to be clearly R^1 and my conclusion was that then R^n integration is not supported.
It might make sense to leave a pointer to the R^n measure theory in this file, because IMHO it is a natural point to look at and it is not uncommon to define Lebesgue measure on R^n right away. But I guess doing this in a text book and in Coq is a different thing and might follow different paths ...
Michael Soegtrop (Oct 21 2022 at 17:11):One question: should I define a function which is 0 outside of [-1,1]^4 and integrate it over R^n, or should I define a measure on [-1,1]^4? I can't figure out how to do the latter (easily), but it seems to me to be the more reasonable approach.
Michael Soegtrop (Oct 21 2022 at 17:22):On point I didn't mention: the "domain pieces" of my function are in general not axis aligned plyhedra. I am unsure if I should try to define corresponding sets and measures on them or to work with integrals of functions times a cutting plane functions, which is 1 on one side and 0 on the other side of an arbitrary plane.
Zachary Stone (Oct 22 2022 at 15:02):Subspaces are weird in MCA sometimes. You can scroll up to see much discussion on the matter. TLDR, I'd try to define things from R^4 -> R first. There are a bunch of theorems that'll help you to ignore the values outside [1,-1]^4
Regarding the misaligned axis, that shouldn't prevent you from _stating_ the integral. As far as computing it goes... I honestly have no idea what you'll encounter.
Last updated: Apr 18 2024 at 07:02 UTC