OAI/Geometry/RCD/Harmonic/QuantitativeAffineMean.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative affine means without assuming a common value limit

  1. theorem OAI.RegularPointCoordinates.interior_chord_error_tendsto_zero line 12
  2. theorem OAI.RegularPointCoordinates.abs_le_of_chord_error line 36
  3. theorem OAI.RegularPointCoordinates.endpoint_chord_error_of_interior_errors line 56
  4. theorem OAI.RegularPointCoordinates.endpoint_chord_error_tendsto_zero line 133
  5. theorem OAI.RegularPointCoordinates.interior_chord_errors_transfer line 146