OAI/Analysis/ForestSpace/Coordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ForestSpace.coordinate_squares_le line 16
  2. theorem OAI.ForestSpace.norm_sum_coordinates_le line 30
  3. theorem OAI.ForestSpace.norm_sum_eX_le line 43
  4. theorem OAI.ForestSpace.dual_vectors_squares_le line 48
  5. theorem OAI.ForestSpace.weakNull_of_l2_bound line 71
  6. theorem OAI.ForestSpace.weakNull_coordinates line 83
  7. theorem OAI.ForestSpace.norm_segment_functional_le line 90
  8. theorem OAI.ForestSpace.norm_segment_functional line 100
  9. theorem OAI.ForestSpace.norm_segment_eX line 107
  10. theorem OAI.ForestSpace.ancestors_isSegment line 112
  11. def OAI.ForestSpace.pathVector line 123
  12. theorem OAI.ForestSpace.norm_pathVector line 126