OAI/NumberTheory/Ostmann/Supply/CenteredProjection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Supply.centeredSpace line 11
  2. def OAI.Ostmann.Supply.centeredProjection line 27
  3. def OAI.Ostmann.Supply.uniformVector line 29
  4. theorem OAI.Ostmann.Supply.uniformVector_apply line 33
  5. theorem OAI.Ostmann.Supply.sum_uniformVector line 37
  6. theorem OAI.Ostmann.Supply.uniformVector_inner line 43
  7. theorem OAI.Ostmann.Supply.uniformVector_orthogonal line 49
  8. theorem OAI.Ostmann.Supply.point_sub_uniform_mem line 56
  9. theorem OAI.Ostmann.Supply.centeredProjection_single line 66
  10. theorem OAI.Ostmann.Supply.centeredProjection_norm_le line 74
  11. theorem OAI.Ostmann.Supply.centeredProjection_gram line 77