OAI/Analysis/TracialSplitting/TraceEstimates.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentMain.IsFull line 18
  2. def OAI.CurrentMain.uniformTwoNorm line 21
  3. def OAI.CurrentMain.uniformHalvingError line 24
  4. lemma OAI.CurrentMain.trace_projection_corner line 32
  5. lemma OAI.CurrentMain.trace_unitary_conjugate line 37
  6. lemma OAI.CurrentMain.trace_unitary_commutator_square line 42
  7. lemma OAI.CurrentMain.traceTwoNorm_sq line 85
  8. lemma OAI.CurrentMain.traceTwoNorm_smul line 89
  9. lemma OAI.CurrentMain.trace_norm_mul_le line 93
  10. lemma OAI.CurrentMain.unitary_commutator_energy line 101
  11. lemma OAI.CurrentMain.trace_commutator_square_expansion line 115
  12. lemma OAI.CurrentMain.trace_cross_compression_square line 138
  13. lemma OAI.CurrentMain.orthogonal_pair_energy_identity line 154
  14. lemma OAI.CurrentMain.orthogonal_pair_energy_le line 172
  15. theorem OAI.CurrentMain.orthogonal_sum_energy_le line 180
  16. def OAI.CurrentMain.weightedAverage line 214
  17. lemma OAI.CurrentMain.weightedAverage_nonneg line 217
  18. lemma OAI.CurrentMain.weightedAverage_le_one line 222
  19. lemma OAI.CurrentMain.trace_mul_nonneg line 245
  20. lemma OAI.CurrentMain.trace_projection_mul_bounds line 255
  21. lemma OAI.CurrentMain.weightedAverage_mass line 263
  22. def OAI.CurrentMain.traceOneNorm line 308
  23. lemma OAI.CurrentMain.traceOneNorm_nonneg line 311
  24. lemma OAI.CurrentMain.trace_selfAdjoint_contraction_mul_le line 314
  25. lemma OAI.CurrentMain.trace_square_sub_le_abs line 335
  26. def OAI.CurrentMain.regularizedSign line 356
  27. lemma OAI.CurrentMain.continuous_regularizedSign line 359
  28. lemma OAI.CurrentMain.regularizedSign_selfAdjoint line 365
  29. lemma OAI.CurrentMain.regularizedSign_norm_le line 369
  30. lemma OAI.CurrentMain.regularizedSign_commute line 379
  31. lemma OAI.CurrentMain.regularizedSign_scalar_error line 383
  32. lemma OAI.CurrentMain.regularizedSign_error line 394
  33. lemma OAI.CurrentMain.trace_square_difference_sign line 409
  34. lemma OAI.CurrentMain.trace_square_sub_le_oneNorm line 423
  35. theorem OAI.CurrentMain.powers_stormer line 459
  36. lemma OAI.CurrentMain.traceOneNorm_le_of_pairing line 467
  37. lemma OAI.CurrentMain.traceOneNorm_add_le line 483
  38. lemma OAI.CurrentMain.traceOneNorm_neg line 492
  39. lemma OAI.CurrentMain.traceTwoNorm_projection_sq line 503
  40. lemma OAI.CurrentMain.trace_sandwich_pairing_le line 507
  41. def OAI.CurrentMain.sandwichMultilinear line 526
  42. lemma OAI.CurrentMain.sandwichMultilinear_apply line 536
  43. def OAI.CurrentMain.traceSandwichMultilinear line 539
  44. lemma OAI.CurrentMain.traceSandwichMultilinear_apply line 545
  45. lemma OAI.CurrentMain.traceSandwichMultilinear_bound line 549
  46. def OAI.CurrentMain.traceSandwichContinuous line 556
  47. lemma OAI.CurrentMain.traceSandwichContinuous_norm_le line 562
  48. lemma OAI.CurrentMain.trace_projective_sandwich_le line 568
  49. lemma OAI.CurrentMain.traceOneNorm_projective_sandwich_le line 585
  50. lemma OAI.CurrentMain.traceOneNorm_projective_sandwich_mul_unitary_le line 601
  51. def OAI.CurrentMain.inclusionTensorMap line 626
  52. lemma OAI.CurrentMain.inclusionTensorMap_norm_le line 631
  53. def OAI.CurrentMain.tensorPair line 645
  54. lemma OAI.CurrentMain.inclusionTensorMap_tensorPair line 649
  55. lemma OAI.CurrentMain.sandwich_tensorPair line 657
  56. def OAI.CurrentMain.diagonalCommutator line 664
  57. lemma OAI.CurrentMain.sandwich_diagonalCommutator line 670
  58. lemma OAI.CurrentMain.weightedAverage_central line 684