Todo #6YB2U: the force corresponding to the harmonic oscillator potential

[LodeVermeulen]

This PR derives the force that is the consequence of the harmonic oscillator potential, alongside some useful API lemmas.

Suggestions on improvements are appreciated, especially on some of the have statements that derive really basic stuff.

[github-actions]

Thank you for your PR! The following checklist can be used to ensure that the PR is as helpful as possible and to help maintain the quality of the project.

This checklist is experimental and can be ignored if you wish.
Feel free to ask if anything is unclear, or make suggestions.

Documentation

• I have updated the module doc-strings of any modules modified, or this comment is not relevant.
• I created a new module doc-string for any new modules created, including an overall description of the module and the main results, or this comment is not relevant.
• I have changed all doc-string occurances of decleration names which I have changed, or this comment is not relevant.
• For definitions and key theorems I have added, I have added an english-readable statement of the result, which is as self-contained as possible, and where appropriate contain a readable UTF-8 version of the result.
• Where appropriate and helpful I have included references to the original source of results in the module doc-string.

Lemmas and theorems

• I have ensured that the theorem key word is reserved for important theorems, and lemma is used for everything else.
• I have ensured that no lemmas or definitions are duplications of other results.

Layout

• I have ensured that results are in the appropriate modules.

Usage of AI

Please tick one that applies to this PR:

• I have not used any AI to generate code.
• I have used basic AI coding assistance (e.g. Copilot) to generate repeative bits of code, but the lemmas and definitions are my own.
• I used AI to generate the structure of the code and/or guide its organization, but I have checked it for corectness.
• Other (please specify with a comment).

[jstoobysmith]

you could do rw [show (2 : ℕ) • (2⁻¹ : ℝ) • S.k • x = (2 : ℝ) • (2⁻¹ : ℝ) • S.k • x by norm_cast] here instead of the have, but yeah I don't think there is a simpler way.

[zhikaip]

shouldn't the grad_inner have (2:ℝ) in the definition which avoids this?

[jstoobysmith]

Yeah, I think that would be an option.

[jstoobysmith]

Would probably make things easier in the long run aswell

[jstoobysmith]

Concerning the linters, let me point out that they can be run locally using lake exe lint_all and ./scripts/lint-style.sh. Running them locally is quicker than waiting for github to pull up the errors.
(you may already know this, but just in case, I like to point it out as I think it's useful to know. :)).

[LodeVermeulen]

Concerning the linters, let me point out that they can be run locally using lake exe lint_all and ./scripts/lint-style.sh. Running them locally is quicker than waiting for github to pull up the errors. (you may already know this, but just in case, I like to point it out as I think it's useful to know. :)).

Thanks, I was actually looking for a way to run them locally but couldn't find it. I will do this shortly.

[LodeVermeulen]

This took me a lot of time and effort but everything should be sorry free. I highly suspect a lot of the results can be golfed still, but I will mark this PR as ready for review now.

[jstoobysmith]

Great! This looks really great to me! Thank you for putting in the effort to do this! I don't see any needed changes so have approved this PR - feel free to merge (let me know if you can't).

Once again thanks for this!