OAI/Geometry/RCD/Harmonic/VanishingVariationAffineLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Affine limits from locally vanishing integrated second variation

  1. theorem OAI.RegularPointCoordinates.integrated_derivative_oscillation line 14
  2. theorem OAI.RegularPointCoordinates.chord_error_le_of_derivative_oscillation line 32
  3. theorem OAI.RegularPointCoordinates.chord_eq_of_vanishing_second_variation line 58
  4. theorem OAI.RegularPointCoordinates.affine_of_vanishing_second_variation line 102