OAI/Geometry/RCD/Coordinates/NormalizationComposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Composing exact coordinate normalizations

  1. theorem OAI.RegularPointCoordinates.transformedColumn_comp line 14
  2. theorem OAI.RegularPointCoordinates.exact_mean_normalization_comp line 23
  3. theorem OAI.RegularPointCoordinates.normalization_values_comp line 37
  4. theorem OAI.RegularPointCoordinates.firstOrderSplitting_comp line 48