Create PseudoRiemannian

[or4nge19]

This PR is divided in 2 parts. Next is Riemannian Metric (with implementation)

[or4nge19]

after completing the PR I will ask for feedback/criticisms in Zulip

[or4nge19]

discussion here:
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.28Pseudo.29.20Riemannian.20metric

and here:

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Don't.20understand.20TangentBundle.20.26.20sections

[jstoobysmith]

Can we remove this space. Maybe run #min_imports at the bottom of the file aswell to minimize the imports needed.

[or4nge19]

yes, I forgot to update it after running #min_imports on PseudoRiemannian :)

[jstoobysmith]

I tried to download your branch to experiment with things - but I think it is still on an older version of lean and mathlib
(which might be why the instances are needed).

If you want to update I think you can:

1. merge Master into this branch.
2. run:

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

(which might take ~20min depending on your computer)

[jstoobysmith]

I've dealt with the instances - let me know if you strongly disagree with my changes. Won't make any more changes for the time-being.

[idontgetoutmuch]

I don't understand what this has to do with Riemannian metrics.

[jstoobysmith]

@or4nge19 I think we can probably revert this change, right? It is probably overhang from the different versions of Mathlib.

But yes @idontgetoutmuch - this has nothing to do with Riemannian metrics :).

[or4nge19]

yes, it's because i forgot to update to the latest mathlib version. I had t replace some deprecated lemmas to make the PhysLean.lean main file compile with the Riemannian PR

[or4nge19]

will revert!

[jstoobysmith]

I fixed the reverts.

Basically I ran locally the following commands:

git checkout Master -- ./PhysLean/StringTheory/FTheory/SU5U1/PhenoConstraints/Basic.lean

on the affected files.

The following comments still need addressing:

• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)
• Create PseudoRiemannian #501 (comment)

[or4nge19]

Thanks!

[or4nge19]

have added PseudoRiemannian/Chart.lean and relative submodules. This defines chartMetric, which expresses a pseudo-Riemannian metric in local chart coordinates, and proves its transformation properties under coordinate changes. Next file in the PseudoRiemannian namespace will prove the equivalence: smooth_in_charts_iff_contDiffOn