OAI/MathematicalPhysics/PEPSSubvolume/PhysicalModular.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Physical tensor products and symmetric modular discrepancies.

  1. def OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_join line 33
  3. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.asMap_tensorAcross_join line 42
  4. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.inner_tensorAcross line 53
  5. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_mul line 76
  6. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_one line 85
  7. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_smul line 89
  8. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_add line 100
  9. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_sub line 111
  10. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.rpow_filter_recovery line 122
  11. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.tensorAcross_sandwich line 136
  12. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.physical_product_error_le line 145
  13. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.inner_star_re line 185
  14. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.inner_symmetrize_re line 194
  15. def OAI.PolynomialPEPS.Subvolume.PhysicalModular.modularError line 212
  16. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.modularError_sum line 215
  17. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.physical_sum_error_le line 221
  18. theorem OAI.PolynomialPEPS.Subvolume.PhysicalModular.modularError_real line 248