OAI/MathematicalPhysics/PEPSFilters/HamiltonianEnergy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Total crossing energy bounds and Hermitian local Hamiltonian terms.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.propagateConjugation_add line 27
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.propagateConjugation_zero line 34
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.propagateConjugation_sum line 40
  4. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.expectation line 49
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.expectation_add line 51
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.expectation_sum line 55
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.expectation_eigenvalue line 59
  8. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.crossingCount line 64
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.sum_crossings line 67
  10. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.regularized_energy_bound line 77
  11. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart line 148
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_hermitian line 150
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_eq line 155
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_norm_le line 160
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_supported line 167
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_add line 175
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_sum line 179
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitianPart_hamiltonian line 183
  19. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitian_terms_of_grid line 188