OAI/Geometry/EinsteinFour/MetricLinearChartPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Path-length comparisons after a fixed linear change of chart coordinates. These retain the sharp constants supplied by a frozen orthonormal frame, instead of replacing them by a coarse operator norm.

  1. theorem OAI.PositiveEinsteinFour.Geometry.linear_chart_edist_le_pathELength line 22