General questions

Stream: PhysLean

[ZhiKai Pong]

I hope it's ok to start a general questions thread similar to #new members or #Is there code for X? but for PhysLean specifically. If some questions are better asked over there please do point that out.

[ZhiKai Pong]

I wanted to start with showing the (free space) wave equation follows from Maxwell's, and wonder how much vector calculus do we have in PhysLean. As far as I can tell spaceDiv and spaceCurl are defined here without much API around it, should I have a go at showing some of the common vector calculus identities?

https://en.wikipedia.org/wiki/Vector_calculus_identities

[ZhiKai Pong]

(Do the maths people care about vector calculus in 3D in this sense? I don't know enough about mathlib to know whether they have this or it follows from some more fancy notion (of differential forms?))

[Joseph Tooby-Smith]

Yes, I think increasing the API around spaceDiv and spaceCurl etc. would be very useful.

Even in Mathlib does have this in a fancy notation, I don't it hurts to have a more specialized version in PhysLean which is easier to use for physicists and physics.
Naturally though we shouldn't go around making long proofs of things which already have proofs in Mathlib.

[ZhiKai Pong]

import PhysLean.Relativity.SpaceTime.Basic

theorem div_of_curl_eq_zero (x : SpaceTime): ∀ A: SpaceTime → EuclideanSpace ℝ (Fin 3), ∇⬝(∇×A) x = 0 := by
  sorry

First attempt at stating something: Tried my best to understand the types defined in div and curl, seems like they're defined through a function (A) that takes SpaceTime and returns a vector in the usual sense? currently this gives an error saying expected token, would appreciate guidance as to how to fix and tips on understanding the setup.

[ZhiKai Pong]

ah I have to open SpaceTime

[Joseph Tooby-Smith]

Ah, ok this is annoying that this doesn't work. This is down to two things:

1. The fact that you need the spacing e.g. ∇× A instead of ∇×A or∇ × A .
2. A precedence issue with the notation meaning you need some more brackets.

I think they should both be easy fixes.

But for now you can do:

theorem div_of_curl_eq_zero (x : SpaceTime)
    (A : SpaceTime → EuclideanSpace ℝ (Fin 3)) : (∇⬝ (∇× A)) x = 0 := by
  sorry

[ZhiKai Pong]

import PhysLean.Relativity.SpaceTime.Basic

open SpaceTime

theorem div_of_curl_eq_zero (x : SpaceTime) (A : SpaceTime → EuclideanSpace ℝ (Fin 3)) : (∇⬝ (∇× A)) x = 0 := by
  sorry

I think this works now. How would I proceed from here? I imagine I'd need to unwrap the definition until the fderiv level for a bunch of simp and rws, is there a straightforward way of doing that?

[Joseph Tooby-Smith]

I would first prove in a separate lemma that two SpaceTime.deriv commute with one another. This probably involves unwrapping the definitions there to fderiv and using properties thereof. You may also need to assume differentiability of the functions. This would be a useful lemma to have anyway.

From this I think div_of_curl_eq_zero is more straight forward.

[ZhiKai Pong]

Joseph Tooby-Smith said:

This probably involves unwrapping the definitions there to fderiv and using properties thereof.

how do I do that?

[Joseph Tooby-Smith]

This is a start:

lemma deriv_commute {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    {d : ℕ} (μ ν : Fin (1 + d)) (f : SpaceTime d → M) :
    deriv μ (deriv ν f) = deriv ν (deriv μ f) := by
  funext y
  rw [deriv, deriv]
  sorry

From there I think it's a case of looking to see what we can use from mathlib.

[ZhiKai Pong]

I have to admit after the rw the proof state is impenetrable to me

(fderiv ℝ (∂_ ν f) y) (((realLorentzTensor d).tensorBasis ![realLorentzTensor.Color.up]) fun x => Fin.cast ⋯ μ) =
  (fderiv ℝ (∂_ μ f) y) (((realLorentzTensor d).tensorBasis ![realLorentzTensor.Color.up]) fun x => Fin.cast ⋯ ν)

From what I gathered mathlib should have what we need here but how to proceed afterwards is beyond my reach.

[ZhiKai Pong]

there's some relevant discussions in this thread and I'm trying to understand @Tomas Skrivan's recent post #new members > partial derivative of a vector field @ 💬.

[ZhiKai Pong]

Going a bit off on a tangent here: If the answer is "I should go ahead and try to understand how fderiv works" I can try that, but at the same time I feel like in Physics a lot of things are implicitly assumed (Most things are continuous etc.) and I would think it might also be possible to expose just the "high level API" at the level of usual undergraduate students which makes everything much more accessible and readable (e.g. I probably don't need any knowledge about manifolds to work with most physics in "normal 3D space", and I haven't heard of Fréchet derivatives until I started looking at lean.) Maybe this is just a matter of the API and "packaging" in PhysLean isn't quite there yet and I hope this will become easier as time goes on.

[Tomas Skrivan]

Here is the full proof that space time derivatives commute up to the proof of Differentiable ℝ (fderiv ℝ f) which I didn't manage to find in mathlib.

import PhysLean
import Mathlib.Analysis.Calculus.FDeriv.Symmetric

open PhysLean
open SpaceTime

noncomputable
def baseVector {d : ℕ} (μ : Fin (1 + d)) : SpaceTime d :=
  ((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ))

theorem deriv_def {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → M) :
    deriv μ f = (fderiv ℝ f · (baseVector μ)) := by rfl

lemma deriv_commute {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {d : ℕ} (μ ν : Fin (1 + d)) (f : SpaceTime d → M) (hf : ContDiff ℝ ⊤ f) :
    deriv μ (deriv ν f) = deriv ν (deriv μ f) := by
  funext y
  simp [deriv_def]
  have : Differentiable ℝ (fderiv ℝ f) := sorry
  simp (disch:=fun_prop) [fderiv_clm_apply (c:=(fderiv ℝ f))]
  rw[IsSymmSndFDerivAt.eq]
  apply ContDiffAt.isSymmSndFDerivAt_of_omega
  apply hf.contDiffAt

I added a custom "unfolding" theorem for SpaceTime.deriv such that the result is more readable.

[Tomas Skrivan]

The goals after simp [deriv_def] says

(fderiv ℝ (fun x => (fderiv ℝ f x) (baseVector ν)) y) (baseVector μ) =
    (fderiv ℝ (fun x => (fderiv ℝ f x) (baseVector μ)) y) (baseVector ν)

rather than

 (fderiv ℝ
        (fun y =>
          (fderiv ℝ f y) (((realLorentzTensor d).tensorBasis ![realLorentzTensor.Color.up]) fun x => Fin.cast ⋯ ν))
        y)
      (((realLorentzTensor d).tensorBasis ![realLorentzTensor.Color.up]) fun x => Fin.cast ⋯ μ) =
    (fderiv ℝ
        (fun y =>
          (fderiv ℝ f y) (((realLorentzTensor d).tensorBasis ![realLorentzTensor.Color.up]) fun x => Fin.cast ⋯ μ))
        y)
      (((realLorentzTensor d).tensorBasis ![realLorentzTensor.Color.up]) fun x => Fin.cast ⋯ ν)

if you call unfold SpaceTime.deriv

[Tomas Skrivan]

ZhiKai Pong said:

Going a bit off on a tangent here: If the answer is "I should go ahead and try to understand how fderiv works" I can try that, but at the same time I feel like in Physics a lot of things are implicitly assumed (Most things are continuous etc.) and I would think it might also be possible to expose just the "high level API" at the level of usual undergraduate students which makes everything much more accessible and readable (e.g. I probably don't need any knowledge about manifolds to work with most physics in "normal 3D space", and I haven't heard of Fréchet derivatives until I started looking at lean.) Maybe this is just a matter of the API and "packaging" in PhysLean isn't quite there yet and I hope this will become easier as time goes on.

Yeah this is a bit unfortunate state of the affairs, even in mathlib if you want to introduce vector space you need to write {X} [AddCommGroup X] [Module Real X] and if you want to differentiate over it you have to write {X} [NormedAddCommGroup X] [NormedSpace Real X] and so on.
I also hope that things will be easier and more familiar to beginners but it is lots of really hard work and somewhat incompatible when you are also trying to figure out the fundamentals on top of which you can do even the really advanced stuff. So at this point one has to spend some time and learn all the Lean/mathlib/PhysLean idiosyncrasies.

[ZhiKai Pong]

thanks a lot, having something as an example should make it much easier to understand, I'll try my best to work through this!

[ZhiKai Pong]

Tomas Skrivan said:

lemma deriv_commute {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {d : ℕ} (μ ν : Fin (1 + d)) (f : SpaceTime d → M) (hf : ContDiff ℝ ⊤ f) :
    deriv μ (deriv ν f) = deriv ν (deriv μ f) := by
  funext y
  simp [deriv_def]
  have : Differentiable ℝ (fderiv ℝ f) := sorry
  simp (disch:=fun_prop) [fderiv_clm_apply (c:=(fderiv ℝ f))]
  rw[IsSymmSndFDerivAt.eq]
  apply ContDiffAt.isSymmSndFDerivAt_of_omega
  apply hf.contDiffAt

the simp after have throws an error
failed to synthesize NormedAddCommGroup M

[Tomas Skrivan]

ZhiKai Pong said:

the simp after have throws an error
failed to synthesize NormedAddCommGroup M

I can't reproduce this, the mwe I posted works for me fine. Do you have other imports, variables etc. in the file?

[Joseph Tooby-Smith]

Tomas Skrivan said:

Here is the full proof that space time derivatives commute up to the proof of Differentiable ℝ (fderiv ℝ f) which I didn't manage to find in mathlib.

import PhysLean
import Mathlib.Analysis.Calculus.FDeriv.Symmetric

open PhysLean
open SpaceTime

noncomputable
def baseVector {d : ℕ} (μ : Fin (1 + d)) : SpaceTime d :=
  ((realLorentzTensor d).tensorBasis _ (fun x => Fin.cast (by simp) μ))

theorem deriv_def {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    {d : ℕ} (μ : Fin (1 + d)) (f : SpaceTime d → M) :
    deriv μ f = (fderiv ℝ f · (baseVector μ)) := by rfl

lemma deriv_commute {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M]
    {d : ℕ} (μ ν : Fin (1 + d)) (f : SpaceTime d → M) (hf : ContDiff ℝ ⊤ f) :
    deriv μ (deriv ν f) = deriv ν (deriv μ f) := by
  funext y
  simp [deriv_def]
  have : Differentiable ℝ (fderiv ℝ f) := sorry
  simp (disch:=fun_prop) [fderiv_clm_apply (c:=(fderiv ℝ f))]
  rw[IsSymmSndFDerivAt.eq]
  apply ContDiffAt.isSymmSndFDerivAt_of_omega
  apply hf.contDiffAt

I added a custom "unfolding" theorem for SpaceTime.deriv such that the result is more readable.

The lemma deriv_commute may also work if Differentiable ℝ (fderiv ℝ f) is not true, right? Since I think then both sides may go to zero.

[Tomas Skrivan]

I don't think so because the statement contains fderiv R (fun x => fderiv R f x u) x v and not fderiv R (fderiv R f) x u v

[ZhiKai Pong]

Tomas Skrivan said:

ZhiKai Pong said:

the simp after have throws an error
failed to synthesize NormedAddCommGroup M

I can't reproduce this, the mwe I posted works for me fine. Do you have other imports, variables etc. in the file?

ah I noticed the version I copied had [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] instead of [NormedAddCommGroup M] [NormedSpace ℝ M], might have copied before you finished editing, works fine now

[Kevin Buzzard]

Tomas Skrivan said:

Yeah this is a bit unfortunate state of the affairs, even in mathlib if you want to introduce vector space you need to write {X} [AddCommGroup X] [Module Real X] and if you want to differentiate over it you have to write {X} [NormedAddCommGroup X] [NormedSpace Real X] and so on.
I also hope that things will be easier and more familiar to beginners but it is lots of really hard work and somewhat incompatible when you are also trying to figure out the fundamentals on top of which you can do even the really advanced stuff. So at this point one has to spend some time and learn all the Lean/mathlib/PhysLean idiosyncrasies.

I am guessing that lean's flexibility will enable you to fix all this at your end, you just define VectorSpace \R V to be the thing you want vector space to mean and write a couple of demo files to show people how to use it. Can variable? help you?

People are constantly asking about PDEs and have been for years (and these people are often not hardcore pure mathematicians and are bewildered by what they find in mathlib). I have found that teaching by writing demo files stuffed full of comments works well.

[ZhiKai Pong]

It seems to me that PhysLean often has to rebuild, I'm not sure exactly when but probably when I change imports? is this because lake exe cache get only works for mathlib? is there a way to speed this up?

[Kevin Buzzard]

lake exe cache get costs money because you're hosting a lot of files. It doesn't work for FLT so I just bought a new laptop so I can compile it more quickly.

[Joseph Tooby-Smith]

I'm surprised it is having to rebuild that often - especially if you are working in one file.

What are you doing when it has to rebuild, are you in VSCode clicking restart file or running lake build?

If the former are you working on two files separated by a large chain of imports?
If so then it may be rebuilding all the imports between the files to make sure nothing breaks.

[ZhiKai Pong]

Sometimes I create a new temporary file to create some adhoc examples for testing etc., I guess that's not always a good idea then. What's the suggested work flow for testing then?

[Joseph Tooby-Smith]

What are you importing into these files?

[ZhiKai Pong]

Say I had a file that was importing PhysLean.ClassicalMechanics.Space.Basic. I changed it to import PhysLean.Relativity.SpaceTime.Basic, then it says I'll need to restart file

[Joseph Tooby-Smith]

When you click restart file it takes a long time?

Every time you change the imports like this you have to restart file. But it shouldn't be rebuilding all of the files in PhysLean, it should be rebuilding any files
import PhysLean.Relativity.SpaceTime.Basic depends on which you have changed (and any files downstream of that).

The SpaceTime file depends on a lot of Tensor stuff, but I suspect you are not modifying this, so I don't think this should take a long time.

[ZhiKai Pong]

ah I checked again seems like just changing this is fine, its when after I sync with the remote repository that triggers a full rebuild

[Joseph Tooby-Smith]

Ok I think either one of two things is happening:

1. I recently bumped PhysLean (a couple of days a go) - this will have triggered the need for a complete rebuild of PhysLean and Mathlib.
2. If more recent, it probably not doing a full rebuild, it's probably rebuilding some of the stuff my PRs have changed, which have been fairly low-level (i.e. lots of files depend on them) and therefore its been rebuilding all the files downstream of this.

[Joseph Tooby-Smith]

Also SpaceTime is fairly low level (i.e. lots of things depend on it) so it could be down to just changes in that

[ZhiKai Pong]

I don't have a good grasp of these kinds of things yet so I'll keep an eye out for what's triggering what, thanks for the explanation!

[Matteo Cipollina]

for emergencies or to check vs the latest Physlean bump you can always use https://live.physlean.com

[Joseph Tooby-Smith]

Matteo Cipollina said:

for emergencies or to check vs the latest Physlean bump you can always use https://live.physlean.com

As of today, this is updating nightly (all being well ) with the latest version of PhysLean.

(Note of warning though: Its a really small server so can't cope with lots of people (= more than one person) using it at the same time. Currently this is ok and not something to worry about when using it.)

[Jeremy Lindsay]

Looks like the reference linked on the lorentz group page is dead and should be changed from http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf to https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf

[Jeremy Lindsay]

happy to make a quick PR

[Joseph Tooby-Smith]

If you could fix this - that would be great :). Maybe it would be a good idea to make it a proper reference to avoid link rot - i.e. put the author, the name of the note etc.

[Jeremy Lindsay]

I'm having a bit of trouble showing (Additive.toMul 1)⁻¹ = Additive.toMul 1 where 1 : ZMod 2. I've left a comment on https://github.com/HEPLean/PhysLean/pull/515 at the relevant code. Any tips are appreciated :)

[Kevin Buzzard]

Can you post a #mwe? I can't make your question typecheck and don't really want to clone the repo on coffeeshop wifi

[Joseph Tooby-Smith]

Ugh, I've had trouble with this in the past (probably in the same file you are editing). I don't think I found a satisfying solution :(.

[Jeremy Lindsay]

EDIT: I need to think about this a bit more.

MWE on Lean web editor

import Mathlib

-- We want to use multiplicative notation for ZMod 2:
local notation "ℤ₂" => Multiplicative (ZMod 2)

-- But there is no "-1" notation
#check (1 : ℤ₂)
#check (-1 : ℤ₂) -- error

-- So we use this instead:
#check (Additive.toMul (1 : ZMod 2))

-- I cannot figure out how to write the inverse properly:
#check (Additive.toMul (1 : ZMod 2))⁻¹ -- error

-- ...in order to show something like this:
#check (Additive.toMul (1 : ZMod 2))⁻¹ = Additive.toMul (1 : ZMod 2)

[Joseph Tooby-Smith]

Something like the following?

possible solution

import Mathlib

-- We want to use multiplicative notation for ZMod 2:
local notation "ℤ₂" => Multiplicative (ZMod 2)

-- But there is no "-1" notation
#check (1 : ℤ₂)
#check (-1 : ℤ₂) -- error

-- So we use this instead:
#check (Additive.toMul (1 : ZMod 2))

-- I cannot figure out how to write the inverse properly:
#check (Additive.toMul (1 : ℤ₂))⁻¹ -- error

-- ...in order to show something like this:
#check (Additive.toMul (1 : ℤ₂))⁻¹ = Additive.toMul (1 : ℤ₂)

[Jeremy Lindsay]

Joseph Tooby-Smith said:

Something like the following?

EDIT: I was a bit confused about what Additive.toMul does; will play around a bit more.

But (1 : ℤ₂) (multiplicative) is the identity while (1 : ZMod 2) (additive) isn't, right?

Header

example : Additive.toMul (1 : ℤ₂) = Additive.toMul (1 : ZMod 2) := by rfl -- fails

[Yakov Pechersky]

import Mathlib

local notation "Z" => Multiplicative (ZMod 2)

example : (.ofAdd 1 : Z)⁻¹ = .ofAdd 1 := by
  rw [← @ofAdd_neg] -- via rw?
  rw [ZMod.neg_eq_self_mod_two] -- via rw?

[Yakov Pechersky]

toMul 1 = 0:

import Mathlib

local notation "Z" => Multiplicative (ZMod 2)

example : (1 : Z) = .ofAdd 0 := rfl

[Kevin Buzzard]

The goal at the sorry in the repo (which I've now downloaded) is not well-typed, so something has gone wrong. The goal is

⊢ Additive.toMul 1 ^ (-1) = Additive.toMul 1

but Additive.toMul : Additive (Fin 2) ≃ Fin 2 and 1 : Fin 2 so there is some defeq abuse going on which will inevitably make things harder.

It looks to me like the defeq abuse is introduced in the line

have hΛ_neg_1 : orthchroRep Λ = Additive.toMul (1 : ZMod 2)

. This should surely say

have hΛ_neg_1 : orthchroRep Λ = Multiplicative.ofAdd (1 : ZMod 2) := by...

Once this change is made, everything is type correct and the proof of the goal at the sorry is just rfl.

[ZhiKai Pong]

I'm having some trouble to state what I want and would like some suggestions.

I want to state that

In an electromagnetic planewave, the

ElectricField (E)
MagneticField (B)
propagation direction (s)

form an orthogonal triad.

I'm following this part of Born and Wolf
image.png

And I have proved (omitting constants etc.)

theorem 4.1 (hBwave : B = magneticPlaneWave B₀ c s hs) :
    ∃ constE, (E t x) = -  s ×₃ (B t x)) + constE

theorem 4.2 (hEwave : E = electricPlaneWave E₀ c s hs) :
    ∃ constB, (B t x) = s ×₃ (E t x)) + constB

4.1 says "if the MagneticField is a planewave, then the ElectricField is equal to -s ×₃ B + a constant field that does not depend on B" which I think is physically correct and similarly for 4.2 says the same thing for the case when ElectricField is a planewave.

However, up to this point those are two separate cases, and I'm not sure how to reconcile them. To be more precise, I think I want to define ElectromagneticPlaneWave as one entity, which simultaneously satisfies 4.1 and 4.2 without the constants. In physics I guess we just say "it follows that the EMwave is consistent with 4.1 and 4.2 and it is self-sustaining etc." but there is a logical gap here which I don't know how to fill in.

Here are some thoughts of mine:

1. is there some way of saying "in the case that constB = 0, 4.2 simplifies to B = s ×₃ E which means an electricPlaneWave travels with an associated MagneticField." This may seem to suggest a causal relationship between E and B which I don't think is the best way to state this.
2. is there some way of coupling 4.1 and 4.2 together and say "an EMwave is consistent with these equations and logically follows as a result".
3. Maybe this chain of reasoning is not how I should have approached this, and maybe I should "define the EMwave as an object with E = electricPlaneWave and B = magneticPlaneWave in the first place, then prove those relations hold".

I'm not sure whether this is a question related to difficulty of formalizing or maybe I just haven't learnt physics correctly, but would appreciate any hints or advice on how to tackle this :)

[Matteo Cipollina]

if I understand it correctly the definition of an 'Electromagnetic Plane Wave basically says: 'We are interested in solutions where E is a plane wave, B is a plane wave, and they satisfy Maxwell equations together, and this is the case where those additive constants are zero. if this is correct, I think you may try to define Electromagnetic Plane Wave  as E(u) and B(u) (where u=r·s-vt) that simultaneously satisfy Maxwell's equations. This definition means 'no static fields' (integration constants = 0), from this the orthogonal triad properties can be derived, and not used as assumptions

[ZhiKai Pong]

ah so instead of having 4.1 and 4.2 separately, I should have both at the some time i.e.

theorem 4 (hBwave : B = magneticPlaneWave B₀ c s hs) (hEwave : E = electricPlaneWave E₀ c s hs) :
    (E t x) = -  s ×₃ (B t x))

and use the other assumption to "force" the static field to 0. I'll give this a try, thanks!

[Joseph Tooby-Smith]

If you can I think it would be worth keeping 4.1 and 4.2 in their own right aswell - seems like they are nice little theorems :).

[ZhiKai Pong]

I think I realize where the problem lies - just having this

ZhiKai Pong said:

theorem 4 (hBwave : B = magneticPlaneWave B₀ c s hs) (hEwave : E = electricPlaneWave E₀ c s hs) :
    (E t x) = -  s ×₃ (B t x))

is not sufficient to preclude the possibility of a constant field, as a constant field still satisfies E = E(r·s-vt). In other words, it is not possible from this alone to decouple the constant field from s ×₃ B. the "no static field" assumption has to be artificially imposed (or with other assumptions e.g. Time average goes to zero) rather than as a consequence of this general form of plane wave. In other words I think the orthogonal triad property is also not something that can be derived form this alone otherwise there's some circular argument going on.

This isn't really a problem when dealing with concrete waves (e.g. time harmonic waves of the form cos(r·s-vt)) but it's the ambiguity of the general form that causes problems. I think I'll just define an object EMWave while specifying the triad, then show this is equivalent to the case where the static fields is 0.

[Joseph Tooby-Smith]

Maybe the following theorem is true:

For E and B plane waves w.r.t. s, there are constant fields constE and constB such that E - constE and B - constB form an orthogonal triad.

(Not saying you should necessarily go along these lines)

[Joseph Tooby-Smith]

(Pretty sure the above theorem is true, and one can actually make it stronger by letting constE = 0).

It is unclear to me if this is a useful theorem though, and your suggestion @ZhiKai Pong might be more useful for other things.

[Joseph Tooby-Smith]

(sorry thinking aloud)

I think the above theorem is useful in the following regard: Define EMWave as suggestioned by @ZhiKai Pong , then my theorem above is equivalent to the statement that:

If E and B are plane waves, they are formed from the addition of an EMWave and two static fields constEand constB. The choice of how you split things into an EMWave and static fields is not unique (I don't think).

[ZhiKai Pong]

The immediate goal is to show that electromagnetic plane waves are transverse. Maybe the notion of "transversality" already implies picking a reference frame?

I'm thinking maybe it should be done the other way round : I specify an orthogonal triad first, then any component that's not transverse is constant.

[ZhiKai Pong]

I can even define the rotation first, and rotate the frame such that s coincides with the z-axis, then argue that fields not in the x-y plane must be constant. This is probably how I'd imagine it if taught in physics, but I assume this is less nice if want to stick to generality

[Joseph Tooby-Smith]

I don't think transversality requires a reference frame here - you already have a specified direction s.

I'm thinking maybe it should be done the other way round : I specify an orthogonal triad first, then any component that's not transverse is constant.

Something like this?

theorem 4.3 (hBwave : B = magneticPlaneWave B₀ c s hs) (hEwave : E = electricPlaneWave E₀ c s hs) :
    ∃ (Ep : ℝ), (E t x) = -  s ×₃ (B t x)  + Ep • s

[Joseph Tooby-Smith]

Actually, this doesn't hold for constant fields so something like:

theorem 4.3 (hBwave : B = magneticPlaneWave B₀ c s hs) (hEwave : E = electricPlaneWave E₀ c s hs) :
    ∃ (Ep : ℝ), (E t x) ⬝ s  = Ep

[ZhiKai Pong]

Joseph Tooby-Smith said:

Actually, this doesn't hold for constant fields so something like:

theorem 4.3 (hBwave : B = magneticPlaneWave B₀ c s hs) (hEwave : E = electricPlaneWave E₀ c s hs) :
    ∃ (Ep : ℝ), (E t x) ⬝ s  = Ep

sorry I'm confused, what do you mean by this?

[Joseph Tooby-Smith]

Yeah, sorry this is my fault, feel free to ignore all my messages in this thread. I was guilty of derailing the conversation a bit :).

What I meant was the following: You said:

I'm thinking maybe it should be done the other way round : I specify an orthogonal triad first, then any component that's not transverse is constant.

I assume the second part of this is referring to when you have plane waves, and I was trying give the corresponding theorem.

[ZhiKai Pong]

I agree that having an s should be enough to define transversality - but I'm not sure if it is sufficient to separate the constant field. you can still superpose an arbitrary constant field that's transverse to s and not affect any of the equations since s ×₃ Ep is just another constant field that can be added to B. Maybe something along the lines of your first idea

theorem 4.3 (hBwave : B = magneticPlaneWave B₀ c s hs) (hEwave : E = electricPlaneWave E₀ c s hs) :
    ∃ (Ep : ℝ3), (E t x) = -  s ×₃ (B t x)  + Ep  ∧ (E - Ep) ⬝ s = 0

might be provable, I'll try and see whether this works.

Formalizing this is making me appreciate we're assuming a lot of things in physics class :)

[Joseph Tooby-Smith]

Yeah, I think something like this should be true :).

[ZhiKai Pong]

asking here since @Joseph Tooby-Smith probably has a good idea of what I'm trying to do.

import Mathlib

example (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f0 : ℝ → EuclideanSpace ℝ (Fin 3))
    (hf : ∀ t x, f t x = f0 (inner ℝ x s - c * t)) (h : ∀ t x, fderiv ℝ (fun u => f0 u) (inner ℝ x s - c * t) = 0):
    ∃ (Ecu : ℝ → EuclideanSpace ℝ (Fin 3)), ∀ t x, f t x = Ecu (inner ℝ x s - c * t) := by
  let u : ℝ → EuclideanSpace ℝ (Fin 3) → ℝ := fun t x => (inner ℝ x s - c * t)
  have hderiv : ∀ t x, fderiv ℝ (fun u => f0 u) (u t x) = 0 := by -- how to state this for is_const_of_fderiv_eq_zero?
    intro t x
    rw [h]
  apply is_const_of_fderiv_eq_zero at hderiv

can't quite wrap my head around change of variables, I want u here to be the variable to take the antiderivative against such that I have Ecu that depends on u, but u = (inner ℝ x s - c * t) itself is a function of t and x and I'm not sure how to restate this in a form that works.

[Joseph Tooby-Smith]

I'm slightly confused about this because what you are trying to proof trivially follows from your assumptions:

import Mathlib

example (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f0 : ℝ → EuclideanSpace ℝ (Fin 3))
    (hf : ∀ t x, f t x = f0 (inner ℝ x s - c * t)) (h : ∀ t x, fderiv ℝ (fun u => f0 u) (inner ℝ x s - c * t) = 0):
    ∃ (Ecu : ℝ → EuclideanSpace ℝ (Fin 3)), ∀ t x, f t x = Ecu (inner ℝ x s - c * t) := by
  use f0

[Joseph Tooby-Smith]

But, assuming you need this for something, then assuming that s and c are not both zero, then x t => (inner ℝ x s - c * t) surjects. Hence

(h : ∀ t x, fderiv ℝ (fun u => f0 u) (inner ℝ x s - c * t) = 0)

implies that

 ∀ u, fderiv ℝ (fun u => f0 u) u = 0

from which you should be able to use is_const_of_fderiv_eq_zero.

[ZhiKai Pong]

Indeed I might have completely overthinked this - I'll check to make sure this is indeed stating what I want. just for completeness, I still don't quite get how the second statement works:

import Mathlib

example (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f0 : ℝ → EuclideanSpace ℝ (Fin 3))
    (hf : ∀ t x, f t x = f0 (inner ℝ x s - c * t)) (h : ∀ t x, fderiv ℝ (fun u => f0 u) (inner ℝ x s - c * t) = 0):
    ∃ (Ecu : ℝ → EuclideanSpace ℝ (Fin 3)), ∀ t x, f t x = Ecu (inner ℝ x s - c * t) := by
  have hu : ∀ u, fderiv ℝ (fun u => f0 u) u = 0 := by
    intro u --this u is just a constant not the u I defined

[Joseph Tooby-Smith]

import Mathlib

example (f : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f0 : ℝ → EuclideanSpace ℝ (Fin 3))
    (hf : ∀ t x, f t x = f0 (inner ℝ x s - c * t)) (h : ∀ t x, fderiv ℝ (fun u => f0 u) (inner ℝ x s - c * t) = 0):
    ∃ (Ecu : ℝ → EuclideanSpace ℝ (Fin 3)), ∀ t x, f t x = Ecu (inner ℝ x s - c * t) := by
  have hc : c ≠ 0 := by sorry
  have hu : ∀ u, fderiv ℝ (fun u => f0 u) u = 0 := by
    intro u
    obtain ⟨x, t, rfl⟩ : ∃ x t, u = inner ℝ x s - c * t := ⟨0, (-u / c), by field_simp⟩
    exact h t x
  sorry

(edit: Golfed, just found out you can do obtain _ : _ := by .... :))

[ZhiKai Pong]

Is it not a good idea to do import Mathlib in PhysLean? I've created a new file for some testing, and its taking forever to build. I understand that it has to be rebuilt after physlean is bumped to a new version, but it still feels like it takes longer than usual. Is this to be expected? I'm not sure if there's a difference between doing this in Mathlib itself or in PhysLean (the file has nothing other than import Mathlib)

[Joseph Tooby-Smith]

Have you tried running lake exe cache get? PhysLean should never have to build Mathlib files.

[Joseph Tooby-Smith]

Also if you run lake build, rather than relying on the info-view, you should be able to see what is being built, and maybe what is slow.

[ZhiKai Pong]

Joseph Tooby-Smith said:

Also if you run lake build, rather than relying on the info-view, you should be able to see what is being built, and maybe what is slow.

I'm running lake build now and it seems much faster than clicking Restart File in the info view :thinking: are they not doing the same thing?

[ZhiKai Pong]

image.png
lake build (in the command line) has already surpassed the infoview

[Joseph Tooby-Smith]

Maybe this is something to do with parallelization?

But this also shows me that it is building mathlib here - which it shouldn't.

[Joseph Tooby-Smith]

I wonder if this is to do with our bump to a non-tagged version of mathlib.

[ZhiKai Pong]

image.png
I'm not sure what I messed up, but now if I restart VScode and open any file it just asks me to click the button which goes into rebuilding Mathlib

[Joseph Tooby-Smith]

Ok, so I got your file running from scratch in less than a minute. Here is what I did:

• I deleted my local version of PhysLean and recloned it.
• I ran lake update
• Then I created your file (in the Optics directory) and restarted it, and it worked.

This is a bit of a nuclear option, and if you follow it you will have to rebuild PhysLean lake build - which should take around 20min.

[Tomas Skrivan]

When this happens I usually just delete the whole .lake directory :) and run lake update followed by lake build. Faster than figuring out what is wrong :slight_smile:

[ZhiKai Pong]

hmm my local copy of mathlib also has the same problem, no idea what's wrong... I guess I'll just reclone both repos :( thanks!