OAI/MathematicalPhysics/PEPSSubvolume/ModularScalar.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Dimension-free row-column and scalar modular distortion bounds.

  1. lemma OAI.PolynomialPEPS.Subvolume.MatrixRows.column_l2 line 24
  2. lemma OAI.PolynomialPEPS.Subvolume.MatrixRows.row_l2 line 38
  3. lemma OAI.PolynomialPEPS.Subvolume.MatrixRows.row_product line 42
  4. lemma OAI.PolynomialPEPS.Subvolume.MatrixRows.column_product line 47
  5. theorem OAI.PolynomialPEPS.Subvolume.MatrixRows.weighted_sum line 52
  6. theorem OAI.PolynomialPEPS.Subvolume.MatrixRows.coefficient_sum line 70
  7. lemma OAI.PolynomialPEPS.Subvolume.ModularScalar.even_exp_remainder line 97
  8. lemma OAI.PolynomialPEPS.Subvolume.ModularScalar.polynomial_exp_decay line 131
  9. theorem OAI.PolynomialPEPS.Subvolume.ModularScalar.quadratic_log_ratio line 140
  10. lemma OAI.PolynomialPEPS.Subvolume.ModularScalar.positive_weight_bound line 172
  11. def OAI.PolynomialPEPS.Subvolume.ModularScalar.modularCoefficient line 206
  12. lemma OAI.PolynomialPEPS.Subvolume.ModularScalar.modularCoefficient_nonneg line 209
  13. theorem OAI.PolynomialPEPS.Subvolume.ModularScalar.modularCoefficient_bound line 224
  14. lemma OAI.PolynomialPEPS.Subvolume.ModularScalar.modularCoefficient_formula line 238