Skip to content

feat: Adds a diffeormorphism for the harmonic oscillator#1004

Open
jstoobysmith wants to merge 4 commits into
masterfrom
harmonic-oscillator-diffeo
Open

feat: Adds a diffeormorphism for the harmonic oscillator#1004
jstoobysmith wants to merge 4 commits into
masterfrom
harmonic-oscillator-diffeo

Conversation

@jstoobysmith

Copy link
Copy Markdown
Member

Adds a diffeomorphism for the harmonic oscillator configuration space.

invFun := toRealCLM
left_inv := by
intro t
cases t

@zhikaip zhikaip Mar 25, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
cases t

shouldn't need cases t here
(goes into CauSeq.Completion.Cauchy abs which is totally irrelevant here)

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks - agreed. I also realised it is probably a bit stupid to add this and not simultaneously convert to EuclideanSpace. So will do that as well here.

@zhikaip zhikaip left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

minor comment above

@jstoobysmith jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 26, 2026
@Bergschaf

Bergschaf commented Jun 12, 2026

Copy link
Copy Markdown
Contributor

It might be possible to use Homeomorph.chartedSpace and Homeomorph.isManifold (from this pr) instead of defining the chartedSpace manually. (The result that this Homeomorphism is then also a Diffeomorphism could probably also fit into mathlib...)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants