Bochners Theorem U(1)

Stream: mathlib4

[Zachary Mullaghy]

Hi everyone -

I have recently finished putting together a build for bochners theorem, fejer riesz, and a riesz representation theorem for U(1). I come from a bit of an unusual background in medical physics but im applying to math phds right now. I am planning to use this build in my own work and considering ive leveraged mathlib so heavily for my own work I thought it would be useful to ask if this work is desirable for the community..

Full disclosure, unfortunately as of now I work alone - i have a small company im starting but that being said I use ai heavily. I have checked these statements consistently but I dont want to pretend anything. It is what it is and im just thankful for a community. The github repo CI passes fully without sorry, admit, or axiom.

Please find the repo here: https://github.com/RoyGBivens137/Reusable

i am happy to improve it as necessary.

Best,
Zach

[Kevin Buzzard]

These proofs look very long and unidiomatic. Did you use AI to generate them?

[Jireh Loreaux]

Kevin, yes, he disclosed this
Zachary Mullaghy said:

but that being said I use ai heavily

[Zachary Mullaghy]

The theory behind it is something I developed analytically from work in GL matrix based refinement. I used AI to help me write the proofs yes.

[Kevin Buzzard]

Sorry, I had misparsed the original message as meaning "I use AI in my day job".

[Zachary Mullaghy]

Quite alright. It’s important to ask