Where to put some integration lemmas

Stream: general

[David Loeffler]

I have some lemmas about integration by substitution over infinite intervals: things like making the change u = x^2 in an integral over x in Ioi 0. I'd like to make a PR to add this to the library, but I'm not sure what file this stuff should go in -- can I ask for some suggestions?

(The motivation here is evaluating the Gamma function at 1/2, reducing it to the computation of the Gaussian integral exp(-x^2) that @Sebastien Gouezel has added.)

[Scott Morrison]

Could you post the list of imports you need?

[Riccardo Brasca]

We have the folowing python script (I think by @Eric Wieser )

import networkx as nx
import requests
import io
import operator
from functools import reduce

with requests.get("https://leanprover-community.github.io/mathlib_docs/import.gexf") as r:
    g = nx.read_gexf(io.StringIO(r.text))

# where you need the lemma, and which files it needs
needed_in = ('mathlib:algebra.gcd_monoid.basic',)
needs = ('mathlib:algebra.gcd_monoid.basic', 'mathlib:ring_theory.coprime.basic')

ok = (reduce(operator.and_, [nx.ancestors(g, n) for n in needs]) &
      reduce(operator.and_, [nx.descendants(g, n) for n in needed_in]))
print(ok)

to find where to place lemmas (of course it doesn't know anything about the mathematics, it just looks at the imports).

[David Loeffler]

Hi guys, sorry I missed your reply until now (I should probably set up notifications in zulip or something). I guess I was more asking "where is the morally / aesthetically right place to put X", rather than "where can I get away with putting X without creating circular imports". I ended up putting the lemmas in two batches, first #17540 (now merged) and second #17542 (awaiting review).

[rtertr (Sonia)]

Hi @David Loeffler , can I ask where these lemma exists? Are they available in the mathlib library?
Kind regards, Sonia

[David Loeffler]

If you look at the PR's on github (linked in my last message) you can see where the lemmas ended up. The one about substituting $u = x^p$ integrals over $(0, \infty)$ is now measure_theory.integral_comp_rpow_Ioi.