OAI/MathematicalPhysics/PEPSFilters/CrossingEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Operator expectation expansions and regularized single-crossing energy bounds.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.inner_sum_real_smul line 28
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.eigenvector_sum line 38
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.similarity_expectation_expansion line 43
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitian_coefficients line 72
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.tensorState_smul_left line 85
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.physical_one_crossing line 92
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.reducedDensity_real_smul line 172
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.normalized_density_diagonal line 181
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.norm_normalized line 195
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.clipped_power_log_ratio line 199
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.log_scaled_difference line 210
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.inverse_conjugate_diagonal line 215
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.regularized_one_crossing line 226