Cosmology Project and dependencies

Stream: PhysLean

[Pedro Bessa]

Hello, I'm a postdoc working in gravitation, cosmology and astrophysics and I got quite interested in the PhysLean project after reading about it on linkedin. I'm able to start working here and there with the Cosmology project, since that is my main background.

I also have a background in mathematics since I started with a B.Sc. in maths, and kept my interest in formalization and axiomatization throughout my change to physics research, so I am not completely unfamiliar to Lean and the proposals. I am new to the Lean 4 language itself, which I'm currently reading and learning to properly start the project, but I think there's nothing better than a project to learn a new language.

What I am most confused about is how we should build the projects from the ground. In particular, I've seen that there is no Riemannian (or Lorentzian) geometry library in mathlib, and although there is very complete Special Relativity library, to properly develop the Cosmology project one would need at least the notions of metric and Levi-Civita connection.

My question then boils down to this: How much should I worry about dependencies before I start working out the fundamentals for the project (Robertson-Walker metric, Friedmann equations, density and pressure terms)? Can I first implement the basics without invoking math dependencies to the underlying structure, such as just describing the systems in terms of the scale factor, density and pressure; or should I first lay the groundwork by defining the Robertson-Walker Lorentzian manifold and describing its connection?

I hope I was able to properly express my doubts and am excited to help with physLean!

[Joseph Tooby-Smith]

Hi Pedro!

Nice to meet you and thank you for your interest in the project!

To answer your main question:

How much should I worry about dependencies before I start working out the fundamentals for the project (Robertson-Walker metric, Friedmann equations, density and pressure terms)? Can I first implement the basics without invoking math dependencies to the underlying structure, such as just describing the systems in terms of the scale factor, density and pressure; or should I first lay the groundwork by defining the Robertson-Walker Lorentzian manifold and describing its connection?

Yes you can implement the basics without invoking the math dependencies to the underlying structure. Indeed, I think if we didn't do this the project overall would become fairly stagnant which is not desirable at this stage (IMO having something is better than having nothing).

When implementing the basics though I would be mindful that in the future we will want the underlying math structure there, so doing it in a way where we can easily refactor to include the underlying math structure when needed will be helpful in the long term. I have done the same with e.g. the Higgs field, really mathematically we would want this defined in a vector bundle associated to the principal bundle of the Standard Model gauge group - but mathlib isn't there just yet - so I did the basics knowing one day it will be refactored.

...to properly develop the Cosmology project one would need at least the notions of metric and Levi-Civita connection.

I note that PhysLean has index notation (which I'm currently trying to improve) so I actually I don't think defining metrics, Christoffel symbols, the Levi-Civita connection etc. would be that hard. Although nevertheless this may not be the best place to start.

Best wishes,
Joseph.

[Joseph Tooby-Smith]

I'm not sure if this helps or hinders - if the latter feel free to complete ignore these. But I've added some informal results related to the FLRW metric. For example:

• semiformal_result (6ZZLH): SpatialGeometry

The others can be found at the same place.

[Pedro Bessa]

Hello Joseph,

Thank you for the clarification, I believe I understand more or less how to proceed then - modularity should be the way then, since we want to be flexible enough so that our codes can later depend on more involved definitions.
I believe I can write out the basics needed for a full description of the Friedmann equations and some of the main results coming from the dynamics. I'll try to structure the main results more or less in the same fashion as you did in the TODO list.

Joseph Tooby-Smith said:

I'm not sure if this helps or hinders - if the latter feel free to complete ignore these. But I've added some informal results related to the FLRW metric. For example:

• semiformal_result (6ZZLH): SpatialGeometry

The others can be found at the same place.

Can I add TODO items and informal definitions? Or is the procedure to first git branch the code and then merge?

Thank you and I hope I can be of help to the project,

Pedro

[Joseph Tooby-Smith]

Hi @Pedro Bessa , great!

Please do add TODO items and informal definitions!

You can either fork the repo and make a pull-request that way, or I can give you write access so you can make a brach and make pull-requests from branches. If the latter works better for you - could you let me know your GitHub username.

In either case, please do make pull-requests even if they only contain TODO items and informal definitions. This is still extremely useful.

Thanks,
Joseph.

[Winston Yin (尹維晨)]

@Pedro Bessa I just saw your message and wanted to say hi! My PhD was in cosmology as well (I develop statistical/observational methods for measuring birefringence), so our interests may align. I've thought throughout my PhD if I could incorporate formalisation in my work somehow, but the goals of the two communities seem to have little overlap as of now.

In terms of Lean work, my approach has been to lay the mathematical groundwork for stating advanced things in physics. That's why I'm building up the differential geometry and dynamical systems libraries. We don't even have solutions to various standard differential equations! I agree with @Joseph Tooby-Smith that the deficiency of such libraries should not block applications to physics, but it does mean that certain problems / statements in physics are more immediately amenable to formalisation than others.

Please keep us updated on your formalisation attempts!

[Kevin Buzzard]

This feels a bit like how mathlib felt when I started doing mathematics; it was a million miles away from anything I found interesting. Maybe choose some appropriate cool targets, solve them, and advertise their solutions in the physics commodity in an attempt to get more adherents?

[Joseph Tooby-Smith]

I have added some of the stuff in this discussion to the "Project ideas" page on the website: https://physlean.com/ProjectIdeas

[Luis Gabriel Bariuan]

Hi all, My name is Luis. I am a PhD student at Berkeley in the intersection of quantum gravity, quantum information, and cosmology. I am pretty new to Lean, but I am really excited to learn. I am currently planning to start working on the cosmology side of things. I will try my best to make an attempt to fill out some of the informal statements! :)

[Luis Gabriel Bariuan]

Hi all, I am currently working through formalizing the first Lemma in the file which is the statement that k sinh(r/k) tends to r in the limit that k goes to infinity. I wanted to double-check my approach since it is beginning to appear rather complicated to implement

My strategy for this is to use sinh(r/k) k goes to r at the limit k goes to infinity. To do this, I will use L'Hopital's rule by rewriting it as sinh(ry)/y and approach 0, but I think before this I need to show that the derivatives of sinh(ry) and y exists?

One of my main confusions is how to invoke L'Hopital's rule in the proof https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/LHopital.html#HasDerivAt.lhopital_zero_left_on_Ioc

It seems that Mathlib has many variations for this depending on how you want to approach the point I guess in this case we should approach from the right, but I am quite confused overall as to which tactic allows me to insert that or if I am missing an implementation that allows me to circumvent a lot of the complications

I should add that this how I am stating the goal
lemma limit_S_saddle(r : ℝ) (h : y = 1 / k) : Tendsto (fun k : ℝ => k * Real.sinh (r / k)) atTop (𝓝 r) := by sorry

[Joseph Tooby-Smith]

Some small comments for now:

1. I think your lemma looks correct!
2. Proofing that the derivatives of sinh(ry) and y exist should just be a case of using the tactic fun_prop.
3. It looks like the version of L'Hopital's rule you need would be deriv.lhopital_zero_atTop
4. Maybe see if you can rearrange (fun k : ℝ => k * Real.sinh (r / k)) to be (fun k : ℝ => Real.sinh (r / k)/ ((1/k))), and then L'Hopital's may be applied using apply .... (I'm worrying about k=0 though)

[Joseph Tooby-Smith]

If you want making a mwe will make it easier for people on here to see and interact with your code.

[Luis Gabriel Bariuan]

Thanks! I was able to rearrange the function to sinh(r/k)/(1/k) via 2 lemmas. It might be worth making a pull request to save this?

Now I am at the stage of writing the main lemma and I am somewhat struggling with being able to apply L'Hopital's rule. After using apply, I end up with 5 goals which form the hypothesis for deriv.lhopital_zero_atTop, but I am not really quite sure what tactic could be potentially used to show them

Here is an MWE of my current progress (it works up until the main lemma)

import Mathlib
import PhysLean.Meta.Informal.SemiFormal
import PhysLean.SpaceAndTime.Space.Basic


open Filter
open scoped Topology
/-!

# The Friedmann-Lemaître-Robertson-Walker metric

Parts of this file is currently informal or semiformal.
-/

namespace Cosmology

/-- The inductive type with three constructors:
- `Spherical (k : ℝ)`
- `Flat`
- `Saddle (k : ℝ)` -/
@[sorryful]
-- def SpatialGeometry : Type := sorry
inductive SpatialGeometry : Type where
  | Spherical (k : ℝ) (h: k < 0)
  | Flat (k : ℝ) (h: k = 0)
  | Saddle (k : ℝ) (h : k > 0)



namespace SpatialGeometry

/-- For `s` corresponding to
- `Spherical k`, `S s r = k * sin (r / k)`
- `Flat`, `S s r = r`,
- `Saddle k`, `S s r = k * sinh (r / k)`.
-/

noncomputable def S (s : SpatialGeometry) : ℝ → ℝ :=
  fun r =>
    match s with
    | SpatialGeometry.Spherical k _ => k * Real.sin (r / k)
    | SpatialGeometry.Flat _ _      => r
    | SpatialGeometry.Saddle k _    => k * Real.sinh (r / k)

/-- The limit of `S (Saddle k) r` as `k → ∞` is equal to `S (Flat) r`. -/
--/ First show that k*sinh(r/k) = sinh(r/k)/(1/k) pointwise.
lemma mul_sinh_as_div (r k : ℝ) :
  k * Real.sinh (r / k) = Real.sinh (r / k) / (1 / k) := by calc
    k * Real.sinh (r / k) = Real.sinh (r / k) * k := by simp [mul_comm]
                        _ = Real.sinh (r / k) / (1 / k) := by simp
--/ Then show that k*sinh(r/k) = sinh(r/k)/(1/k) pointwise for the whole function.
lemma fun_mul_sinh_as_div (r : ℝ) : (fun k : ℝ => k * Real.sinh (r / k)) = (fun k : ℝ => Real.sinh (r / k) / (1 / k)) := by
  funext k
  simp [mul_sinh_as_div]


lemma limit_S_saddle(r : ℝ) : Tendsto (fun k : ℝ => k * Real.sinh (r / k)) atTop (𝓝 r) := by
  rw [fun_mul_sinh_as_div r]
  set f := fun x : ℝ => Real.sinh (r / x)
  set g := fun x : ℝ => 1 / x
  apply deriv.lhopital_zero_atTop

[Joseph Tooby-Smith]

Looking at the 5 goals you get, I don't think deriv.lhopital_zero_atTop is the right version. This is my bad - sorry. In particular one of those goals says that fun x => x tends to zero at infinity, which it doesn't. (ignore this, made a mistake) BTW if you remove the

import PhysLean.Meta.Informal.SemiFormal
import PhysLean.SpaceAndTime.Space.Basic

from your mwe then it is even better, as people can open it online by clicking one of the buttons in the top right corner of your code snippet.

I think making a PR with what you have already one looks good! I would replace the proof of limit_S_saddle with sorry and add a @[sorryful] attribute to it so that it passes the linters.

[Kevin Buzzard]

import Mathlib

lemma mul_sinh_as_div (r k : ℝ) :
    k * Real.sinh (r / k) = Real.sinh (r / k) / (1 / k) := by
  field

[Joseph Tooby-Smith]

I think the correct way to convert from (fun k : ℝ => k * Real.sinh (r / k))
to (fun x : ℝ => (1/x)* Real.sinh (r * x)) is to use Filter.Tendsto.comp and the result Kevin just wrote :). This should then give you a Filter.Tendsto which is to zero rather than to infinity.

[Joseph Tooby-Smith]

One of the arguments to docs#Filter.Tendsto.comp should likely be docs#tendsto_inv_atTop_zero(found using loogle, edited with correct version).

[Luis Gabriel Bariuan]

Hi Kevin, Thanks. Just to double check should the strategy be by field_simp instead? I can't get by field to work but I might have misunderstood

[Kevin Buzzard]

field is brand new, I was just demoing its capabilities. If it doesn't work for you, it will work the next time PhysLean is bumped.

[Luis Gabriel Bariuan]

Hi all,
Thanks. I cleaned up some of the stuff I had and made a PR (not sure if it worked since Git is still somewhat confusing for me, but I thought it might just be good practice to try it now with small changes). I am still working on showing the main lemma. I added another intermediate lemma (yet to be shown) sinh(r x)/x goes to r at x goes to zero. I will do some more readings in the next couple days to really dig deeper and see if I can expand on all the previous lemmas I did not complete

[Joseph Tooby-Smith]

Hi Luis! Thanks for your PR! It looks great.

Before it can be merged it has to pass some checks called 'github workflows', these are essentially scripts that check for things like "do all definitions have doc-strings", "are there any unexpected spaces" etc. The easiest way to check if your PR satisfies these checks is to run them locally:

lake exe lint_all
./scripts/lint-style.sh

The last two steps of the former takes a long time, and they can be skipped using

lake exe lint_all --fast

and manually 'replicated' by putting '#lint' at the bottom of any edited files fixing the error and then removing it.

The first step of lake exe lint_all can be run by itself using lake exe style_lint (hopefully this will make sense once you have run it).

I understand this is a bit of an 'extra' burden to make a commit to a PR, but hopefully you can see the benefit, and it becomes easier to manage once you've done it a number of times.

[Luis Gabriel Bariuan]

Hi Joe,
Thanks for this. I think I was able to successfully remove the errors from the lint checker. I commited all the changes to my fork and it added to the pull request. The final commit I made has a comment Formalized basic definitions in FLRW. Introduced intermediatte lemmata. I am not sure if there is still anything else I have to do? Sorry for all the git questions I am still getting rather used to this workflow

[Joseph Tooby-Smith]

Awesome, I think it may still be pulling up some linting issues. I am happy to help fix these, but for some reason can't download your PR. I think it is because you closed it and then opened it again. Would you mind doing the following:
Put

#min_imports

at the bottom of the file, and replace import Mathlib with the things it says there, then remove the #min_imports. Then commit these changes to the PR.

[Joseph Tooby-Smith]

Hi Luis, ok ignore the message above. I managed to download your PR (I think likely something to what you have done). I fixed all the linters locally. I tried to rename my commits in line with what I was doing, e.g. what linter I was fixing, so I think it would be a good learning step for you to take a look. But in case, there is nothing you need to do more on this PR. Thanks for making it :tada:.

The linters on github are in a state of disarray (#general > runLinter in github workflow not terminating ), so I am not so worried about those right now.

[Luis Gabriel Bariuan]

Hi Joe, I had some time today and wrote up the first-order Friedmann equation, Hubble constant and the deceleration parameter and made another PR (I think I am starting to get the hang of the github workflow. The push, pull and merging was quite confusing for me :sweat_smile: ). I will try to work on the last set of informal lemmas + add the second order Friedmann and other results tomorrow if I get a chance.

In this case, I skipped defining the FLRW metric for now since I don't think there is a way yet to have general metrics in curved spacetime? Actually I would love to chat with people about ideas in GR too.

On the local vscode side, one thing I noticed that I have to for some reason restart every file when accessing them. I don't think I remember seeing this a couple of days ago but I might have missed something?

Thanks

[Matteo Cipollina]

Luis Gabriel Bariuan ha scritto:

In this case, I skipped defining the FLRW metric for now since I don't think there is a way yet to have general metrics in curved spacetime? Actually I would love to chat with people about ideas in GR too.

Hi!. Indeed in PhysLean we have this, which tries to formalize a (pointwise) metric tensor g is in general relativity (in finite dimension): a smoothly varying, non-degenerate, symmetric bilinear form on the tangent spaces of a manifold, with a constant signature (e.g., (+, -, -, -) for Lorentzian metrics). To use it you should instatiate (g : PseudoRiemannianMetric E H M n I). However I have left a PR halfway completing the smoothness properties because meanwhile RiemannianBundle has been added to mathlib (infinite dimension) , while Levi-Civita connection is being developed too, and I was planning at some point of thinking of the best way to integrate the PhysLean one with these.

some useful discussion here:
#general > (Pseudo) Riemannian metric
#new members > Bennett Chow @ 💬
#rss > Recent Commits to mathlib4:master @ 💬
#PR reviews > #26221 Towards geodesics and the Levi-Civita connection

[Joseph Tooby-Smith]

Awesome Luis! Your PR looks great. There are some linting things that need fixing on your PR, and I made a comment there. Good to know you are getting more use to the github workflow :) - yeah, it can be confusing to start with.

I personally haven't noticed any difference with vscode, but we did recently bump PhysLean to a newer version of Lean, so this might explain any differences you are seeing. Is it something that is e.g. taking a long time or noticeably slows things down? If so it is probably not due to this update.

No worries about skipping the defining of the metric for now, as Matteo says we do have a way in which it may be included, and there is a lot of great development in this direction :).

[Luis Gabriel Bariuan]

Hi all,
I am currently working on the lemma that derive the time evolution of the Hubble constant in terms of the Hubble constant and the deceleration parameter, but I seem to be running into a subtle issue with not being able to apply the definition I established earlier. In this case, is there a reason why I am not allowed to use the rewrite tactic to perform the substitution of the def. of the hubble constant within the first step?

Edit: I tried to use Time earlier, but I am not sure how to invoke PhysLean here, so I reverted t : Time to t : ℝ for now

import Mathlib
open Filter
open scoped Topology
open Real

namespace Cosmology

@[simp] noncomputable def hubbleConstant (a : ℝ → ℝ) (t : ℝ) : ℝ :=
    deriv a t / a t
@[simp] noncomputable def decelerationParameter (a : ℝ → ℝ) (t : ℝ) : ℝ :=
    - (deriv (deriv a) t * a t) / (deriv a t)^2
lemma time_evolution_hubbleConstant
  (a : ℝ → ℝ) (t : ℝ)
  (ha  : DifferentiableAt ℝ a t)
  (ha' : DifferentiableAt ℝ (deriv a) t)
  (h₁ : a t ≠ 0)
  (h₂ : deriv a t ≠ 0) :
  deriv (fun s => hubbleConstant a s) t
    = - (hubbleConstant a t)^2 * (1 + decelerationParameter a t) := by
    calc
     deriv (fun s => hubbleConstant a s) t = _root_.deriv (fun s => deriv a s / a s) t := by sorry
      _ = - (hubbleConstant a t)^2 * (1 + decelerationParameter a t) := by sorry

[Luis Gabriel Bariuan]

Also I am planning to switch the order of presentation of the two original informal lemmata suggested. I plan to put this lemma first before the one where q =- (1 + (dₜ H)/H^2)

[Luis Gabriel Bariuan]

I also have a couple of results in mind that might be good (i.e. discussing matter, radiation, and inflation). Will have to define a couple more things but I will try to get to them after finishing these two current lemma

[Luis Gabriel Bariuan]

One more thing, my planned strategy for the current lemma I shared is to use product rule, then perform a lot of rearrangements using field to obtain the final result. I think this should work, but I am also open to suggestions about better strategies

[Joseph Tooby-Smith]

Annoyingly the Lean 'playground' doesn't work with PhysLean, so thank you for making a mwe that does work here. (There did use to be a playground that worked for PhysLean, but the cost of hosting it got too much).

Sometimes rw doesn't work on the argument of functions. One way around this is to use conv or conv_lhs or conv_rhs tactics to navigate to the desired place in the expression and then to use rw. For example:

import Mathlib
open Filter
open scoped Topology
open Real

namespace Cosmology

@[simp] noncomputable def hubbleConstant (a : ℝ → ℝ) (t : ℝ) : ℝ :=
    deriv a t / a t
@[simp] noncomputable def decelerationParameter (a : ℝ → ℝ) (t : ℝ) : ℝ :=
    - (deriv (deriv a) t * a t) / (deriv a t)^2
lemma time_evolution_hubbleConstant
  (a : ℝ → ℝ) (t : ℝ)
  (ha  : DifferentiableAt ℝ a t)
  (ha' : DifferentiableAt ℝ (deriv a) t)
  (h₁ : a t ≠ 0)
  (h₂ : deriv a t ≠ 0) :
  deriv (fun s => hubbleConstant a s) t
    = - (hubbleConstant a t)^2 * (1 + decelerationParameter a t) := by
    calc
     deriv (fun s => hubbleConstant a s) t =
          _root_.deriv (fun s => deriv a s / a s) t := by
        conv_lhs =>
          enter [1, t] -- moves to the correct place in the expression
          rw [hubbleConstant]
      _ = - (hubbleConstant a t)^2 * (1 + decelerationParameter a t) := by sorry

Here is one additional suggestion, instead of the assumptions:

(ha  : DifferentiableAt ℝ a t)
 (ha' : DifferentiableAt ℝ (deriv a) t)

It is probably better to have the single assumption (ha : ContDiffAt ℝ 2 a t).

[Daniel Morrison]

I'll add that simp_rw is nice for these kinds of situations, as it also does replacements inside quantifiers and functions:

import Mathlib
open Filter
open scoped Topology
open Real

namespace Cosmology

@[simp] noncomputable def hubbleConstant (a : ℝ → ℝ) (t : ℝ) : ℝ :=
    deriv a t / a t
@[simp] noncomputable def decelerationParameter (a : ℝ → ℝ) (t : ℝ) : ℝ :=
    - (deriv (deriv a) t * a t) / (deriv a t)^2
lemma time_evolution_hubbleConstant
  (a : ℝ → ℝ) (t : ℝ)
  (ha  : DifferentiableAt ℝ a t)
  (ha' : DifferentiableAt ℝ (deriv a) t)
  (h₁ : a t ≠ 0)
  (h₂ : deriv a t ≠ 0) :
  deriv (fun s => hubbleConstant a s) t
    = - (hubbleConstant a t)^2 * (1 + decelerationParameter a t) := by
    calc
     deriv (fun s => hubbleConstant a s) t =
          _root_.deriv (fun s => deriv a s / a s) t := by
        simp_rw [hubbleConstant]
      _ = - (hubbleConstant a t)^2 * (1 + decelerationParameter a t) := by sorry

[Luis Gabriel Bariuan]

Thank you Joe and Daniel for the suggestions! I will take a look later this week. I have been quite swamped these past few days

[Joseph Tooby-Smith]

FYI @Pietro Monticone filled in some of the sorries in this file here PhysLean#810.