OAI/Combinatorics/Progressions/Geometry/MarkedLocalObservableMetric.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realMarkedParameterDirection_coordinate_norm_le line 17
  2. theorem OAI.Erdos3.normalizedMarkedPhase_coordinate_norm_le line 42
  3. def OAI.Erdos3.markedPhaseRemovalLinear line 55
  4. theorem OAI.Erdos3.markedPhaseRemovalLinear_apply line 61
  5. theorem OAI.Erdos3.markedPhaseRemovalLinear_coordinate_norm_le line 66
  6. theorem OAI.Erdos3.markedPhaseRemovalLinear_coordinate_dist_le line 87
  7. theorem OAI.Erdos3.normalizedMarkedRetraction_coord line 102
  8. theorem OAI.Erdos3.normalizedMarkedRetraction_coordinate_dist_le line 106
  9. theorem OAI.Erdos3.normalizedMarkedRetraction_coordinate_norm_le line 136
  10. def OAI.Erdos3.markedRetractionBoxConstant line 167
  11. def OAI.Erdos3.markedEvaluationBoxRadius line 172
  12. def OAI.Erdos3.markedLocalBoxConstant line 175
  13. theorem OAI.Erdos3.markedLocalCoefficientValue_norm_le line 188
  14. theorem OAI.Erdos3.markedLocalCoefficientValue_coordinate_dist_le line 194