OAI/NumberTheory/Ostmann/Supply/TensorOperators.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Supply.TensorOperators.FiniteHilbertSpace line 9
  2. instance OAI.Ostmann.Supply.TensorOperators.(instance at line 18) line 18
  3. def OAI.Ostmann.Supply.TensorOperators.FiniteHilbertSpace.of line 22
  4. def OAI.Ostmann.Supply.TensorOperators.FiniteHilbertSpace.tensor line 25
  5. instance OAI.Ostmann.Supply.TensorOperators.FiniteHilbertSpace.(instance at line 28) line 28
  6. def OAI.Ostmann.Supply.TensorOperators.tensorSpace line 33
  7. def OAI.Ostmann.Supply.TensorOperators.tensorOp line 37
  8. def OAI.Ostmann.Supply.TensorOperators.pureTensor line 42
  9. theorem OAI.Ostmann.Supply.TensorOperators.tensorOp_pureTensor line 47
  10. theorem OAI.Ostmann.Supply.TensorOperators.norm_tensorOp_le line 57
  11. theorem OAI.Ostmann.Supply.TensorOperators.norm_tensorOp_le_of_local line 69
  12. theorem OAI.Ostmann.Supply.TensorOperators.norm_pureTensor line 76
  13. theorem OAI.Ostmann.Supply.TensorOperators.pureTensor_inner line 86
  14. def OAI.Ostmann.Supply.TensorOperators.evalLinearMap line 104
  15. lemma OAI.Ostmann.Supply.TensorOperators.evalLinearMap_apply line 107
  16. lemma OAI.Ostmann.Supply.TensorOperators.eval_single line 110
  17. lemma OAI.Ostmann.Supply.TensorOperators.eval_sum line 117
  18. lemma OAI.Ostmann.Supply.TensorOperators.mapL_sum_left line 130
  19. lemma OAI.Ostmann.Supply.TensorOperators.mapL_sum_right line 137
  20. def OAI.Ostmann.Supply.TensorOperators.tensorPolynomial line 144
  21. theorem OAI.Ostmann.Supply.TensorOperators.eval_tensorPolynomial line 150
  22. def OAI.Ostmann.Supply.TensorOperators.tensorFamilyPolynomial line 172
  23. theorem OAI.Ostmann.Supply.TensorOperators.eval_tensorFamilyPolynomial line 178
  24. theorem OAI.Ostmann.Supply.TensorOperators.norm_eval_tensorFamilyPolynomial_le line 193
  25. theorem OAI.Ostmann.Supply.TensorOperators.norm_eval_tensorFamilyPolynomial_le_of_local line 200
  26. theorem OAI.Ostmann.Supply.TensorOperators.tensorFamily_coefficient_norm_le line 208
  27. theorem OAI.Ostmann.Supply.TensorOperators.tensorFamily_rectangular_error_le line 219
  28. lemma OAI.Ostmann.Supply.TensorOperators.eval_add line 237
  29. def OAI.Ostmann.Supply.TensorOperators.projectionPolynomial line 242
  30. theorem OAI.Ostmann.Supply.TensorOperators.eval_projectionPolynomial line 249
  31. lemma OAI.Ostmann.Supply.TensorOperators.eval_projectionPolynomial_one line 262
  32. theorem OAI.Ostmann.Supply.TensorOperators.norm_eval_projectionPolynomial_le line 267