OAI/Geometry/RCD/Metric/QuantitativeDimensionalCross.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative completion from the scalar dimensional inequality

The trace and squared norm of an almost orthonormal frame suffice. No invertibility or independently postulated tangent dimension is used.

  1. theorem OAI.RegularPointCoordinates.dimensional_cross_defect line 15
  2. theorem OAI.RegularPointCoordinates.dimensional_cross_abs_defect line 48