Error function

Stream: Is there code for X?

[Daniel Weber]

Do we have the error function? I see in Mathlib.Analysis.SpecialFunctions.ImproperIntegrals there's

See Also: Mathlib.Analysis.SpecialFunctions.Gaussian -- integral of exp (-x ^ 2)

but I can't find Mathlib.Analysis.SpecialFunctions.Gaussian.

[llllvvuu]

That directory does exist, but it's not exactly what you want (other than maybe the integrability being useful for defining the erf): docs#integral_gaussian

[Daniel Weber]

I see. I'm interested in formalizing the theorem that the error function isn't elementary. Is there anything which might be relevant? Differential algebra, the definition of elementary functions?

[Kevin Buzzard]

I don't think we have either of them

[Daniel Weber]

Alright, so I'll do them :thumbs_up: