OAI/MathematicalPhysics/PEPSSubvolume/SchmidtRows.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Normalized Schmidt rows and singular-safe matrix distortion.

  1. def OAI.PolynomialPEPS.Subvolume.NormalizedRows.root line 24
  2. def OAI.PolynomialPEPS.Subvolume.NormalizedRows.inverseRoot line 25
  3. def OAI.PolynomialPEPS.Subvolume.NormalizedRows.kernel line 26
  4. def OAI.PolynomialPEPS.Subvolume.NormalizedRows.rows line 27
  5. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.kernel_hermitian line 30
  6. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.inverseRoot_hermitian line 34
  7. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.kernel_mul_weights line 37
  8. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.kernel_mul_zero line 43
  9. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.root_inverse line 51
  10. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.reconstruction line 63
  11. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.rows_gram line 70
  12. lemma OAI.PolynomialPEPS.Subvolume.NormalizedRows.rows_norm_le line 94
  13. theorem OAI.PolynomialPEPS.Subvolume.NormalizedRows.effective_norm_le line 106
  14. def OAI.PolynomialPEPS.Subvolume.ModularMatrix.weightPower line 124
  15. def OAI.PolynomialPEPS.Subvolume.ModularMatrix.weightInverse line 127
  16. def OAI.PolynomialPEPS.Subvolume.ModularMatrix.distortion line 130
  17. def OAI.PolynomialPEPS.Subvolume.ModularMatrix.bilinearExpectation line 134
  18. lemma OAI.PolynomialPEPS.Subvolume.ModularMatrix.covariance line 138
  19. lemma OAI.PolynomialPEPS.Subvolume.ModularMatrix.entry_identity line 147
  20. theorem OAI.PolynomialPEPS.Subvolume.ModularMatrix.product_error_le line 161
  21. lemma OAI.PolynomialPEPS.Subvolume.ModularMatrix.gram_real_smul line 196
  22. lemma OAI.PolynomialPEPS.Subvolume.ModularMatrix.bilinear_real_smul line 202
  23. theorem OAI.PolynomialPEPS.Subvolume.ModularMatrix.scaled_product_error_le line 213