Talk:Reversal of Limits of Definite Integral

From ProofWiki
Jump to navigation Jump to search

Re circular

Think it's worse - this theorem isn't even compatible with our definition of definite integral since we would speak about subdivisions of $\closedint b a$, which is empty if $b > a$. I think the common convention is that this is a definition for $\ds \int_b^a$. We would have to either make this a definition or adopt a non-standard definition of the Riemann integral that allows for swapped endpoints like this. Caliburn (talk) 18:11, 7 August 2020 (UTC)

Yeah well in one of the proofs round here the conditions have been changed from $a < b$ to $a \le b$ so if we have free rein to just change the parameters of the theorems we're proving, we can have absolutely no claims to rigour whatsoever. I wonder whether we were being too ambitious when we started this shitty website. --prime mover (talk) 21:05, 7 August 2020 (UTC)
IMO I don't think there's a problem in making theorems more general as long as only trivial alterations to any existing proofs are required. (eg. considering an extra case or making some inequalities non-strict) I don't think this diminishes rigour at all. If this can't be done the generalised statement probably warrants its own page. If we refactor this into a definition, all we need to do is prove a minor extension of FTC that for continuous $f$ we have $\ds \int_b^a \map f x \rd x = \map F a - \map F b$, which is basically immediate. The "main use" of this theorem is cleaning up after a substitution and assuming that we quote this modified FTC on that page we'll be fine on that front. (it already virtually "assumes" this modified FTC) So crisis averted once that's done. Well the project is ambitious but could be supported with an active enough userbase which we unfortunately don't have at the moment. I feel you're too pessimistic about these things, we can't expect the site to be perfect in every area. Caliburn (talk) 22:06, 7 August 2020 (UTC)