Commit 2026-03-02 21:29 630ea421

feat: weaken assumptions for integration by parts (#35870)

• Previously you had to prove that both functions are differentiable everywhere. Now you only have to show that each function is differentiable on the topological support of the other function.
• This is useful when one of the functions has compact support / a test function. Then the conditions on the other function can be weakened.
• This is used for Sobolev spaces.
• Most hypotheses to IBP are straightforwardly weakened, by adding an additional assumption.
• A few hypotheses are reformulated from Differentiable ℝ f to ∀ x ∈ tsupport g, DifferentiableAt ℝ f x.
• Also add some straightforward lemmas about the interaction of (t)support and deriv. These are immediate analogues of lemmas for fderiv.