OpenGA/OpenGALib.lean at main · MathNetwork/OpenGA · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
import OpenGALib.Algebraic
import OpenGALib.Tensor
import OpenGALib.Riemannian
import OpenGALib.GeometricMeasureTheory

/-!
# OpenGALib — Open Geometric Analysis Library

A Lean 4 library of algebraic, tensor, Riemannian-geometry, and
geometric-measure-theory primitives. Layered:

```
Algebraic ← Tensor ← Riemannian ← GeometricMeasureTheory
```

Each sub-namespace is built on Mathlib. Application papers consume this lib
as a separate sub-project (`require OpenGALib from ".."`).

## Sub-namespaces

* `Algebraic`               — field-generic computable algebraic core
                              (bilinear forms + concrete instances) plus
                              `Algebraic/Auxiliary/` combinatorial helpers
                              (Fin / Perm / Kronecker / Shuffle theory)
                              consumed by `Tensor/Alternating`.
* `Tensor`                  — vector-bundle tensor algebra: continuous
                              multilinear / alternating maps, tensor
                              products, differential forms. Independent
                              of metric.
* `Riemannian`              — Levi-Civita connection, Riemann / Ricci /
                              scalar curvature, second fundamental form,
                              manifold gradient, Hessian / Laplacian
                              operators, `(r,s)`-tensor bundle types.
* `GeometricMeasureTheory`  — finite-perimeter, varifolds, stationary,
                              tangent cones, rectifiability, isoperimetric.

## Sorry status

Per `docs/SORRY_CATALOG.md`. The Riemannian package carries zero existence
axioms; ported content carries 5 PRE-PAPER sorrys total (2 in
`Algebraic/Auxiliary/Fin`, 3 in `Algebraic/Auxiliary/ShuffleDeriv`),
all inherited from the external lib.
-/