OAI/Analysis/TracialSplitting/SpectralLayers.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.scalar_inv_sqrt_near_one line 18
  2. lemma OAI.CurrentMain.selfAdjoint_spectrum_near_one line 45
  3. lemma OAI.CurrentMain.inv_sqrt_near_one line 55
  4. lemma OAI.CurrentMain.normalize_near_isometry line 82
  5. lemma OAI.CurrentMain.traceTwoNorm_sq_real_smul line 105
  6. lemma OAI.CurrentMain.traceTwoNorm_sq_partition_left line 112
  7. lemma OAI.CurrentMain.traceTwoNorm_sq_partition_right line 119
  8. lemma OAI.CurrentMain.traceTwoNorm_sq_partition line 130
  9. lemma OAI.CurrentMain.spectral_commutator_energy line 136
  10. lemma OAI.CurrentMain.traceTwoNorm_sq_unitary_mul line 153
  11. lemma OAI.CurrentMain.traceTwoNorm_sq_mul_unitary line 158
  12. lemma OAI.CurrentMain.traceTwoNorm_sq_projection line 164
  13. lemma OAI.CurrentMain.projection_combination_mul line 176
  14. lemma OAI.CurrentMain.projection_mul_combination line 187
  15. lemma OAI.CurrentMain.projection_combination_nonneg line 196
  16. lemma OAI.CurrentMain.sqrt_projection_combination line 200
  17. lemma OAI.CurrentMain.weighted_spectral_cauchy line 213
  18. lemma OAI.CurrentMain.traceTwoNorm_sq_partition_unitary_row line 239
  19. lemma OAI.CurrentMain.traceTwoNorm_sq_partition_unitary_col line 245
  20. lemma OAI.CurrentMain.trace_projection_combination line 253
  21. lemma OAI.CurrentMain.spectral_root_sum_le line 258
  22. lemma OAI.CurrentMain.sqrt_unitary_conjugate line 284
  23. lemma OAI.CurrentMain.root_commutator_sq_le line 293
  24. theorem OAI.CurrentMain.finite_spectral_energy line 310
  25. def OAI.CurrentMain.cutCoefficient line 350
  26. lemma OAI.CurrentMain.cutCoefficient_nonneg line 353
  27. lemma OAI.CurrentMain.cutCoefficient_mono line 358
  28. def OAI.CurrentMain.layerCoefficient line 367
  29. lemma OAI.CurrentMain.layerCoefficient_nonneg line 369
  30. lemma OAI.CurrentMain.layerCoefficient_mono line 373
  31. lemma OAI.CurrentMain.cut_difference_sum_of_le line 379
  32. lemma OAI.CurrentMain.cut_difference_sum line 392
  33. def OAI.CurrentMain.upperLayerCut line 405
  34. lemma OAI.CurrentMain.upperLayerCut_projection line 407
  35. lemma OAI.CurrentMain.layer_decomposition line 416
  36. theorem OAI.CurrentMain.layer_energy line 423
  37. theorem OAI.CurrentMain.layer_energy_le line 441
  38. def OAI.CurrentMain.orderedLayerWeights line 457
  39. lemma OAI.CurrentMain.orderedLayerValues_mono line 460
  40. lemma OAI.CurrentMain.orderedLayerWeights_nonneg line 473
  41. lemma OAI.CurrentMain.orderedLayerWeights_le line 480
  42. lemma OAI.CurrentMain.layerCoefficient_orderedLayerWeights line 488
  43. lemma OAI.CurrentMain.projection_sum_mul_atom line 506
  44. lemma OAI.CurrentMain.projection_atom_mul_sum line 511
  45. def OAI.CurrentMain.completeResolution line 516
  46. lemma OAI.CurrentMain.completeResolution_projection line 519
  47. lemma OAI.CurrentMain.completeResolution_orthogonal line 529
  48. lemma OAI.CurrentMain.completeResolution_sum line 548
  49. lemma OAI.CurrentMain.upperLayerCut_completeResolution_succ line 552
  50. theorem OAI.CurrentMain.layer_energy_le_of_orthogonal line 560
  51. lemma OAI.CurrentMain.normalize_near_partial_isometry line 586