OAI/MathematicalPhysics/PEPSFilters/SpectralPowers.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Spectral functional calculus, analytic matrix powers and eigenprojectors.

  1. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn line 16
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_mul line 21
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_one line 26
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_star line 30
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_norm line 37
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_unitary line 43
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_positive line 54
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenvalues_conjugate line 61
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.tracePower_conjugate line 69
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.sum_eigenvalues_applyFn line 76
  11. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPower line 94
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPower_entire line 97
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPower_one line 101
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPower_norm_le_one line 111
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_id line 128
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_trace line 131
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.density_eigenvalues_sum line 138
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.density_eigenvalues_le_one line 143
  19. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.spectralCLM line 148
  20. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.spectralCLM_apply line 153
  21. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_differentiable line 156
  22. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_hasDerivAt line 161
  23. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_entire line 167
  24. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_norm_le_one line 171
  25. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_one_positive line 179
  26. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_one_tracePower line 191
  27. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPower_hasDerivAt_zero line 222
  28. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_hasDerivAt_zero line 239
  29. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPhase line 244
  30. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPhase_norm line 247
  31. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPhase_unitary line 252
  32. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.scalarPower_right line 257
  33. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.spectralPhase_unitary line 266
  34. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_right line 270
  35. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_real_eq_cfc line 286
  36. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_complex_parts line 291
  37. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.continuousOn_quasispectrum line 301
  38. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_map line 306
  39. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_zero_mul_self line 323
  40. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_zero_hermitian line 332
  41. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_zero_sq line 340
  42. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.power_mul_zero line 349
  43. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.deriv_mul_zero line 358
  44. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector line 373
  45. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector_positive line 377
  46. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector_sq line 386
  47. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector_trace line 394
  48. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector_sum line 400
  49. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector_mul_self line 411
  50. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.eigenProjector_norm line 423