OAI/Analysis/TensorLp.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TensorLp.H line 19
  2. theorem OAI.TensorLp.hasSum_square line 21
  3. theorem OAI.TensorLp.tensor_mem line 24
  4. def OAI.TensorLp.tensor line 31
  5. theorem OAI.TensorLp.tensor_apply line 32
  6. theorem OAI.TensorLp.tensor_norm_sq line 35
  7. theorem OAI.TensorLp.tensor_norm line 43
  8. theorem OAI.TensorLp.slice_mem line 48
  9. def OAI.TensorLp.slice line 54
  10. theorem OAI.TensorLp.slice_apply line 55
  11. theorem OAI.TensorLp.hasSum_slice_norm_sq line 57
  12. theorem OAI.TensorLp.slice_norm_le line 70
  13. def OAI.TensorLp.sliceCLM line 75
  14. theorem OAI.TensorLp.sliceCLM_apply line 82
  15. def OAI.TensorLp.tensorRight line 89
  16. theorem OAI.TensorLp.tensorRight_apply line 100
  17. def OAI.TensorLp.tensorLeft line 102
  18. theorem OAI.TensorLp.tensorLeft_apply line 113
  19. theorem OAI.TensorLp.inner_tensor line 115
  20. theorem OAI.TensorLp.lift_mem line 135
  21. def OAI.TensorLp.liftVector line 151
  22. theorem OAI.TensorLp.liftVector_apply line 154
  23. theorem OAI.TensorLp.slice_liftVector line 157
  24. theorem OAI.TensorLp.liftVector_norm line 160
  25. def OAI.TensorLp.liftLeft line 175
  26. theorem OAI.TensorLp.liftLeft_apply line 192
  27. theorem OAI.TensorLp.liftLeft_norm line 195
  28. theorem OAI.TensorLp.slice_liftLeft line 199
  29. theorem OAI.TensorLp.hasSum_slice_inner line 203
  30. theorem OAI.TensorLp.liftLeft_symmetric line 212
  31. theorem OAI.TensorLp.liftLeft_positive line 221
  32. theorem OAI.TensorLp.liftLeft_one line 235
  33. theorem OAI.TensorLp.liftLeft_mul line 239