OAI/Geometry/EinsteinFour/MetricChartPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A chart differential bound converts the length of an actual smooth path into a Euclidean endpoint bound. This is the reverse estimate needed to establish positive local Hausdorff mass.

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