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.