Interest in Optics

Stream: PhysLean

[ZhiKai Pong]

Hi, I'm a PhD student in optical engineering writing up my thesis, and I've been wanting to try my hands at lean for a while now but haven't really got the time. The mathematical side of formalization does seem to be a bit too intimidating especially for someone without proper mathematical training like myself, and I came across PhysLean which looks much more familiar to what I know. Joseph just posted #PhysLean > Mini projects a couple days ago, I had a look at the linked page and I'm curious as to whether it is something suitable for a beginner to get started.

To be more specific, what is the expected expertise to start working on such a project? Is there a concrete plan on what is expected to be formalized, and how would one begin to contribute to this project? Many thanks!

[Joseph Tooby-Smith]

Hey @ZhiKai Pong, nice to meet you! I you are doing a phd in optical engineering I think you have more than enough expertise to start this project! I think it would be good for a beginner because a lot of the 'translating things into type theory' has been done for you.

There is a corresponding paper here: https://arxiv.org/pdf/1403.3039

I think as a first goal formalizing the definitions and results from this paper (/convert them into lean) and build the corresponding theorems and lemmas and documentation around it would be good! Although you probably know more about the area then I do - so perhaps there is more interesting things to be done here.

No one else that I know of has started this, so its really up to you how you start.

As a starting step, one could write the results into PhysLean using informal_lemma and informal_definition. These can be used to write english versions of the results and plan what needs doing without having

I would recommend contributing to PhysLean in small steps - don't wait until the end to PR it. I'm happy to help in anyway I can :)

[ZhiKai Pong]

Thanks Joseph! I'm submitting my thesis end of April (fingers crossed) and I hope to start working on this afterwards, will try to read the paper as a starting point and see how it goes from there!

[Joseph Tooby-Smith]

Good luck with your thesis! :)

[Alex Meiburg]

Nice! I'm also happy to try to offer some support if necessary. :) I glanced at your Google Scholar profile a bit. Do you have a particular idea of things you'd like to try to write down?

I'm not in optics, but maybe something like - a theory of some basic optical field configurations, some operations on them, and then some proofs about how they compose? (Like how polarizers compose etc.)
Looking at https://www.nature.com/articles/s41377-024-01659-z it would be very cool to formalize some ideas about topologically protected states, like formalizing the notion of Skyrmion number. You could plug into the rich topology theory in Mathlib. I'm sure there are other mathy people that would be happy to help with that too

[ZhiKai Pong]

Thanks Alex, I wasn't prepared to be scrutinized so soon haha! the short story is that my PhD topic (on direct laser writing) isn't actually on this, instead I'm going to join the team afterwards as a postdoc and work on developing the theory and applications for optical Skyrmions.

Part of my motivation to do lean is to actually make sure I go through the maths here :sweat_smile: I'm only scratching the surface of the maths side of this area and still have a lot more to learn, so I'm not sure when I'll be able to actually formalize these results. Nevertheless, the maths required (I believe) is actually laid out quite detailedly in the methods section of the paper, so yes that's a goal that hopefully I'll be able to formalize that in the not-too-distant future. From my observation this is still a relatively new area where the people working on it don't really understand the maths, and people who know the maths aren't in this area, so maybe having lean say "look this is proven correct" would make the results more convincing.

I'd imagine what I want to do for a short term goal is something like this:

Starting from Maxwell's equations ->
define free space propagation (wave equations etc.) ->
define polarization in terms of Stokes parameters and Muller matrices ->
define optical components (polarizers, waveplates etc.) in terms of Muller matrices and show that their action on stokes parameter is as expected

and then maybe move on to more fancy stuff like topological properties of optical Skyrmions. otherwise it might also be possible to try something that's more established such as OAM light via Laguerre–Gaussian modes.

Another branch of optics that I'm interested in is waveguide theory, but I feel that's much more complicated (Bessel functions, boundary conditions etc.) and might leave that for later.

Given this I'm probably more interested in wave and electromagnetic optics, but if there's interest in geometrical/quantum optics I'm open to discussions and see how I can contribute as well :)

[Alex Meiburg]

It looks like Bessel functions aren't even in Mathlib! Which is kinda funny. I guess they feel kind of "old school" math in certain ways - and they're very useful for numerics and asymptotic analysis, but I guess they're not so crucial for mathematical proofs (in the sense of Mathlib) as much.

Like I said, I don't know much about optics ... I didn't know what Muller matrices were until you mentioned them. (Although, upon a quick Google, they look familiar...) I think defining them and proving basic facts about them would be a great and easy first item. Then you could prove how they work with Maxwell's equations, "linking up" different topics. Of course that's just my suggestion, no need to do that necessarily

[Alex Meiburg]

Like, you could prove that a series of perfect linear polarizers leads has 0 transmission, if and only if some adjacent pair of polarizers is off by 90 degrees. That would be cool

[Alex Meiburg]

I mean, very basic fact. But I think it'd be cool!

[ZhiKai Pong]

Alex Meiburg said:

Like, you could prove that a series of perfect linear polarizers leads has 0 transmission, if and only if some adjacent pair of polarizers is off by 90 degrees. That would be cool

Muller matrices (or Jones matrices) is a tool that allows you to do exactly that! Your statement is equivalent to stating a product of matrices

$$\left(\begin{matrix}\cos^2(\theta_1) \quad \cos(\theta_1)\sin(\theta_1)\\ \cos(\theta_1)\sin(\theta_1) \quad \sin^2(\theta_1)\end{matrix}\right)\left(\begin{matrix}\cos^2(\theta_2) \quad \cos(\theta_2)\sin(\theta_2)\\ \cos(\theta_2)\sin(\theta_2) \quad \sin^2(\theta_2)\end{matrix}\right)\cdots\left(\begin{matrix}\cos^2(\theta_n) \quad \cos(\theta_n)\sin(\theta_n)\\ \cos(\theta_n)\sin(\theta_n) \quad \sin^2(\theta_n)\end{matrix}\right) = \left(\begin{matrix}0 \quad 0 \\ 0 \quad 0\end{matrix}\right)$$

if and only if there exists a pair of $\theta_a, \theta_{a+1}$ with $\lvert\theta_a - \theta_{a+1}\rvert = \pi/2$

So the mathematical language for stating these kinds of scenarios is actually there I just have to figure out how to translate it into lean!

[Kevin Buzzard]

Bessel functions will be needed for non-holomorphic modular forms but we're only just getting our head around the holomorphic case for now

[ZhiKai Pong]

Hi @Joseph Tooby-Smith , I'm trying to set up PhysLean, when I run "lake exe cache get" I got an error saying

 error: compiled configuration is invalid; run with '-R' to reconfigure

Is this a repository issue or a lean issue? there's some related discussion at #mathlib4 > lake exe cache get error but there doesn't seem to be an explicit fix, let me know if I should ask over there.

[Joseph Tooby-Smith]

I don't think this is a PhysLean issue. The penultimate comment to the discussion you linked to said says that removing the .lake might work, so something like:

rm -rf .lake
lake update
lake exe cache get
lake build

[ZhiKai Pong]

oh nevermind, just running lake update works

[ZhiKai Pong]

A more general question: I had a look at SciLean and seems like it could be useful (say working with differential equations), but it's still relatively empty at the moment. May I ask is SciLean expected to be part of the ecosystem, or is it better to stick with what mathlib offers for the time being?

[Joseph Tooby-Smith]

Hey! So ideally I think PhysLean should sit downstream of SciLean and have it be part of the ecosystem.

I think right now there are two technical barriers that I see to including it right now (maybe this is something @Tomas Skrivan can also comment on) .

• The rate at which Lean and Mathlib update mean that PhysLean and SciLean are not on the same versions as each other (and I think therefore it won't actually work if you try and import SciLean into PhysLean).
• SciLean introduces some axioms like sorryProofAxiom which circumvent needing proofs. This is fine, but ideally I would like to keep PhysLean sorry free. This is solvable by having linters which check theorems for these axioms, but this is something which would nee implementing.

[Tomas Skrivan]

I think SciLean should as PhysLean just have specific commits that depend on mathlib with a specific tag. This way you should be able to depend on both projects.

[Joseph Tooby-Smith]

This would be good!

The problem I have with these specific tags is that for mathlib they appear quite far apart in terms of development. That is to say, a lot has happened in mathlib between the tag v4.18.0-rc1 (which PhysLean is currently on) and v4.18.0 (which it needs upgrading to), meaning that every time I want to bump PhysLean its a fair amount of work. We could bump PhysLean to one of the nightly builds but then it would potentially become out of 'sync' with other projects (maybe not so much an issue though).

[Kevin Buzzard]

We bump FLT weekly, I think it's the only way to survive. The quicker you bump the fewer problems you have to deal with.

[ZhiKai Pong]

https://www.fields.utoronto.ca/programs/scientific/12-13/Marsden/FieldsSS2-FinalSlidesJuly2012.pdf

I came across this which is certainly out of reach at the moment, but maybe "proper" geometrical optics should be formalized in this way

(just putting this here for easier reference in the future)

[ZhiKai Pong]

For the complex representation of waves, I think what I really want is the analytic representation of a real-valued function.

The construction goes like the following (from Born and Wolf) :

image.png
image.png

Basically given a signal s(t) you construct a complexification s(t) + i * H(s(t)) where H is the Hilbert transform.

This is useful in optics and communication theory, since (1) the mathematical manipulation is simpler, but more importantly (2) the Fourier transform has no negative frequency components which is in some sense more physical.

I'll like to ask for suggestions on how to state this, as far as I can tell docs#fourierIntegral is defined rather generally and I'm not familiar with functional analysis at all (I just take this construction as given and work with it...), so I'm sure there are a lot of nuances to this and any advice would be appreciated :)

(I probably won't be working with the Fourier integrals directly any time soon, but I thought it might still be a good idea to ask how we might want to set this framework up.)

[Joseph Tooby-Smith]

To be taken with a pinch of salt: Seems to me that $a(\nu)$ and $\phi(\nu)$ are the basic underlying objects here. Thus one can define these in a structure, and from that structure define (1), (2), (4), and prove (3) and (5). I think really $a(\nu)$ should be a distribution, so one can have dirac-delta functions etc.

[Joseph Tooby-Smith]

(One could then also define a function which takes a $V(t)$ to this structure and show that under certain conditions it is an inverse of (1)). Again though, just an idea of one possible way.

[ZhiKai Pong]

looks like I should be using docs#SchwartzMap and docs#SchwartzMap.fourierTransformCLM? I'll try to see how much I can pick up from the documentation and hack something together

[ZhiKai Pong]

https://opg.optica.org/josa/abstract.cfm?uri=josa-57-5-613

I thinks this paper sketches out the physical intuition (at least one perspective of it) behind why this representation is useful in optics - not claiming I'm able to formalize all the details, but if the overall reasoning of this can be stated in a way connecting all the way from the maths to the physics hopefully this is a reasonable goal to work towards

[ZhiKai Pong]

is there any examples of variational calculus in physlean?

[Joseph Tooby-Smith]

ZhiKai Pong said:

is there any examples of variational calculus in physlean?

No there aren't. I think @Tomas Skrivan will have more to say on this, and why this is difficult - and I think there are probably discussions in the past on this Zulip which discuss this.

I think the crux of the difficulty is that physicists make variational calculus look easy, but when you actually try and do it properly it is a pain. I think one way around this is, for the time being, just formalize what the physicist actually does.

[Tomas Skrivan]

I have spent quite some time thinking about it. I think lots of the calculation done by physicists can be done formally using the theory of convenient vector spaces. Ideally someone formalizes the first few chapters of The Convenient Setting of Global Analysis. Then I have a rough idea of how to write a tactic to then automate the calculations.

Anyway, do you have a concrete example you would like to formalize/compute that I can have a look at? (Something self-contained, I'm not following this thread very closely)

[ZhiKai Pong]

not at the moment, I'll come back when I have something more concrete

[Joseph Tooby-Smith]

I just had a thought, which may be obvious to some people, or complete nonsense, but it is this:

Variational calculus doesn't have anything to do with physics, it is just a tool one uses to find the extrema of the action.

To give an example, let us consider classical mechanics.

What is physical is the trajectories which are local extrema of the action, although in most cases 'local' is really 'global'.

For example, a trajectory $s(t)$ is a global minimum of the action if for all other trajectories $r(t)$ :

$$\int_{t_0}^{t_1} L(s(t), \dot s(t)) \leq \int_{t_0}^{t_1} L(r(t), \dot r(t)).$$

To state this result in Lean does not require variational calculus.

I could do classical mechanics by just guessing trajectories $s(t)$ and trying to proof in some way that it is an extrema of the action.

Calculus of variations gives you a good way of guessing $s(t)$ (and maybe proving it is an extrema?) but one could skip that step entirely. One could just take the Euler-Lagrange equations solve them for $s(t)$ - take this as the guess for the trajectory and prove it is an extrema, and I wouldn't have missed any physics.

All this to say: I don't think the difficulties around variational calculus need to hinder progress related to extrema of actions.

[Tomas Skrivan]

I'm not sure if I follow. The calculus of variation shows that the stationary point of action is expressed by the Euler-Lagrange equation. There is no guarantee that it is local minimum or maximum and I have read somewhere that it does not have to be either. It is just a stationary point but I do not have a concrete example at hand.

Calculus of variation allows you to derive the differential equation formulation of physical laws from the knowledge of energy or Lagrangian. I think that just working with that inequality would be difficult.

[Joseph Tooby-Smith]

Yeah, ok I agree. All I am saying is the following. Given a function $S[x]$, corresponding to an action. There are two sets of trajectories:

1. Those trajectories $x$ for which $S[x]$ is a stationary point (defined topologically in terms of neighborhoods and inequalities). This includes saddle points as well as maxima and minima.
2. Those trajectories $x$ for which the functional derivative of $S[x]$ vanishes.

I believe (though can't find a proof) that these sets of trajectories are equivalent to one another, as they are for functions. To define the set of functions (1) doesn't require calculus of variations, but to state (2) does - i.e. you need to know how to take functional derivatives.

If the difficulty is defining the functional derivative, then (1) may be easier to work with. But, yeah I agree, the inequalities might be a nightmare - but maybe they're ok in some specific examples.

That said, I don't actually know what is the physically correct set of functions we should be trying to find. It is usually presented as (1), and then some handwaving comes in to get to (2).

(See this link for such handwaving)

[Tomas Skrivan]

How do you define a saddle point with inequalities?

The law of physics:

$$
\delta S = 0
$$

Is expressed using functional derivative.

I think (2) is developed because (1) is impossible to work with.

[Joseph Tooby-Smith]

For isolated saddle points in e.g. 2 or 3d (and I presume higher) by the number of regions around the point with value less then or greater then the value of that point. The case of 1d I don't know :).

The 'law' of physics $\delta S = 0$ comes from the stationary phase approximation of the path integral. What I don't know is if the stationary phase approximation gives you actually this law, or originally (1), which people turn into (2). In any case I think you are probably right that (1) might be impossible to work with :(.

[Joseph Tooby-Smith]

This link would seem to suggestion (2) is the more original one, in line with what you are saying Tomas, thus this invalidates most of what I've said here - sorry. But interesting things to think about here.

[Tomas Skrivan]

Joseph Tooby-Smith said:

The 'law' of physics $\delta S = 0$ comes from the stationary phase approximation of the path integral. What I don't know is if the stationary phase approximation gives you actually this law, or originally (1), which people turn into (2). In any case I think you are probably right that (1) might be impossible to work with :(.

I'm not very familiar with quantum mechanics but in classical mechanics you have the universal law $\delta S = 0$ too. I wrote down few notes on variational calculus in a separate thread