Bochner's Theorem

Stream: mathlib4

[Zachary Mullaghy]

Hi everyone - I am a bit new here and so I admit some ignorance to how we do things - but I am hopeful that I can be a part of this amazing community. I have encountered the need for Bochner's theorem in my work and I have spent a considerable amount of effort working towards a full biconditional. (not to be confused with bochner's integration file) - I am curious if anyone is already working on this - I am happy to cooperate I am just interested in ensuring this gets added to the repository. Finally - as I am new i am very much still learning - if I did anything wrong please just be patient with me and let me know I am truly doing my best and I will get better over time

Thanks for letting me into your community,
Zach
FourierBochner.lean
(named it fourierbochner to distinguish from the aforementioned bochner integration file)

[Yaël Dillies]

Hey! I too am interested in formalising Bochner's theorem, but for compact (not necessarily abelian) groups. Yours should generalise to locally compact abelian groups instead, but I am not sure the necessary background material has been formalised already.

[Yaël Dillies]

I believe there is no common generalisation to both settings (compact vs locally compact abelian), so your contribution would be very welcome!

[Zachary Mullaghy]

The file isnt quite done - about 4 proofs on the converse left (and they're challenging) and so this post is in reference to two things beyond just finding other people working on this - 1. I added some adjacently related Toeplitz matrix work - I am unsure if this is bad taste as I can easily just send it to other files if needed. 2. If any proofs are related and needed here feel free to let me know

[Zachary Mullaghy]

thank you so much! I will definitely work on the LCA as well

[Yaël Dillies]

Regarding 1, yes, the Toeplitz matrix material will need to move to another file, but that can be dealt with during review

[Zachary Mullaghy]

Awesome - thanks for the review I will definitely make that happen! Happy to meet you :)

[Zachary Mullaghy]

PastedText.txt

I think there’s some really good content in here. I am traveling and cannot clean it up just yet but I really wanted to share.

thankful for you all :folded_hands:

FourierBochner.lean

[Zachary Mullaghy]

If this method is inferior to an LCA method I don’t yet understand please feel free to roast me. I did the proof this way because it lines up with my own needs and it matters to me that I serve the community and not just myself.

[Alex Meiburg]

Hi, I just wanted to comment that we generally encourage people (although it is not a hard rule) to state when they used AI to generate the majority of their code. Not because that's bad - it's good, if it accelerates development! - but it gives a space to comment on how confident you are on these being the best formalizations of topics, how much you tried to clean up statements / proofs yourself, and so on. This looks very LLM generated, so I wanted to ask.

[Zachary Mullaghy]

I appreciate the question and I have definitely used AI. That’s why it has all of these excited comments that are unreasonably hyped :sweat_smile:

it’s important for me that this is a community that can withstand the AI signal to noise ratio! Just standing on what content is good.

I’m actually still improving in lean overall. I’ve taken a year long sequence in functional analysis.

AI likes to try and make you feel special. I’m under no elevated notions of self. Science is a team effort.

Thanks for the question

[Zachary Mullaghy]

So I did some reading and I found a non standard herglotz on the circle proof using a similar strategy

https://bpb-eu-w2.wpmucdn.com/sites.aub.edu.lb/dist/3/101/files/2020/01/herglotzsubject.pdf#:~:text=Theorem%201%20%28Herglotz%29%3A%20Let%20,probability%20measure%20%C2%B5%20on%20S

[Zachary Mullaghy]

I just want to ask if I can extend this easily to a general LCA proof