OAI/Analysis/ModularRecovery/PositiveKernels.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Positive operator kernels, matrix pairings, and norm bounds.

  1. lemma OAI.BoundedRecovery.nonneg_of_jordan_pairing line 19
  2. def OAI.BoundedRecovery.weightedMatrixFunctional line 48
  3. lemma OAI.BoundedRecovery.weightedMatrixFunctional_star_mul line 56
  4. lemma OAI.BoundedRecovery.weightedMatrixFunctional_nonneg line 63
  5. lemma OAI.BoundedRecovery.weightedMatrixFunctional_faithful line 70
  6. instance OAI.BoundedRecovery.vonNeumannAlgebra_complete line 92
  7. def OAI.BoundedRecovery.StandardModularData.phi line 97
  8. lemma OAI.BoundedRecovery.StandardModularData.phi_star_mul line 102
  9. lemma OAI.BoundedRecovery.StandardModularData.phi_nonneg line 108
  10. lemma OAI.BoundedRecovery.StandardModularData.phi_faithful line 111
  11. lemma OAI.BoundedRecovery.StandardModularData.phi_star line 118
  12. def OAI.BoundedRecovery.StandardModularData.commutingPairing line 124
  13. lemma OAI.BoundedRecovery.StandardModularData.commutingPairing_star line 130
  14. def OAI.BoundedRecovery.StandardModularData.modularLift line 140
  15. lemma OAI.BoundedRecovery.StandardModularData.modularLift_xi line 145
  16. lemma OAI.BoundedRecovery.StandardModularData.eq_of_xi line 149
  17. lemma OAI.BoundedRecovery.StandardModularData.modularLift_add line 157
  18. lemma OAI.BoundedRecovery.StandardModularData.modularLift_smul line 166
  19. lemma OAI.BoundedRecovery.StandardModularData.modularLift_weakEquation line 175
  20. lemma OAI.BoundedRecovery.StandardModularData.weakEquation_zero line 205
  21. lemma OAI.BoundedRecovery.StandardModularData.eq_of_weakEquation line 217
  22. def OAI.BoundedRecovery.StandardModularData.modularKernel line 228
  23. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_add line 232
  24. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_smul line 237
  25. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_weakEquation line 244
  26. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_star line 251
  27. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_one line 270
  28. lemma OAI.BoundedRecovery.weightedMatrixFunctional_jordan line 293
  29. instance OAI.BoundedRecovery.vonNeumannAlgebra_cstar line 306
  30. lemma OAI.BoundedRecovery.vonNeumannAlgebra_sqrt_mem line 309
  31. lemma OAI.BoundedRecovery.sqrt_factor_eq line 316
  32. instance OAI.BoundedRecovery.vonNeumannAlgebra_starOrdered line 321
  33. lemma OAI.BoundedRecovery.StandardModularData.commuting_apply line 336
  34. lemma OAI.BoundedRecovery.StandardModularData.commutingPairing_gram line 342
  35. def OAI.BoundedRecovery.StandardModularData.modularGram line 356
  36. lemma OAI.BoundedRecovery.StandardModularData.modularGram_apply line 360
  37. lemma OAI.BoundedRecovery.StandardModularData.modularGram_selfAdjoint line 364
  38. lemma OAI.BoundedRecovery.StandardModularData.modularGram_equation line 372
  39. lemma OAI.BoundedRecovery.StandardModularData.modularGram_pairing line 393
  40. lemma OAI.BoundedRecovery.StandardModularData.modularGram_nonneg line 417
  41. lemma OAI.BoundedRecovery.cstarMatrix_norm_le_sum line 447
  42. instance OAI.BoundedRecovery.vonNeumannAlgebra_realCFC line 464
  43. instance OAI.BoundedRecovery.vonNeumannAlgebra_nonnegSpectrum line 469
  44. def OAI.BoundedRecovery.kernelScalar line 472
  45. lemma OAI.BoundedRecovery.kernelScalar_pos line 474
  46. lemma OAI.BoundedRecovery.kernelScalar_le line 475
  47. def OAI.BoundedRecovery.StandardModularData.kernelMatrix line 484
  48. lemma OAI.BoundedRecovery.StandardModularData.kernelMatrix_apply line 488
  49. lemma OAI.BoundedRecovery.StandardModularData.kernelMatrix_nonneg line 492
  50. lemma OAI.BoundedRecovery.StandardModularData.kernelMatrix_add line 498
  51. lemma OAI.BoundedRecovery.StandardModularData.kernelMatrix_smul line 505
  52. lemma OAI.BoundedRecovery.StandardModularData.kernelMatrix_mono line 512
  53. lemma OAI.BoundedRecovery.StandardModularData.modularKernel_one' line 520
  54. lemma OAI.BoundedRecovery.StandardModularData.norm_kernelMatrix_one_le line 525
  55. lemma OAI.BoundedRecovery.StandardModularData.norm_modularKernel_of_nonneg line 537