OAI/MathematicalPhysics/PEPSFilters/SchmidtPairing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Quadratic and weighted row-column estimates for Schmidt coefficients.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.clipped_log_lipschitz line 23
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.convexOn_sinh_nonneg line 39
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.sinh_mul_le line 49
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.cosh_mul_sub_one_le line 55
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.sqrt_mul_cosh_half_log line 70
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.quadratic_coefficient line 82
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.orthonormal_column_sq line 110
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.orthonormal_row_sq line 117
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.row_column_product line 128
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.weighted_row_column line 148
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.weighted_product_bound line 162
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.hermitian_pairing line 174
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.quadratic_coefficient_nonneg line 200
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.quadratic_product_sum line 219
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.one_crossing_schmidt_bound line 243