OAI/MathematicalPhysics/PEPSSubvolume/KernelPerturbation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Zero-eigenspace perturbations and superquadratic normalization.

  1. def OAI.PolynomialPEPS.Subvolume.KernelPerturbation.kernel line 19
  2. def OAI.PolynomialPEPS.Subvolume.KernelPerturbation.magnitude line 22
  3. def OAI.PolynomialPEPS.Subvolume.KernelPerturbation.phaseValue line 25
  4. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.phaseValue_unitary line 29
  5. def OAI.PolynomialPEPS.Subvolume.KernelPerturbation.perturbUnitary line 51
  6. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.magnitude_nonneg line 57
  7. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.magnitude_posSemidef line 64
  8. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.perturb_factorization line 72
  9. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.magnitude_power_sum line 94
  10. def OAI.PolynomialPEPS.Subvolume.KernelNormalization.scale line 114
  11. theorem OAI.PolynomialPEPS.Subvolume.KernelNormalization.scale_pos line 116
  12. theorem OAI.PolynomialPEPS.Subvolume.KernelNormalization.scale_power line 119
  13. theorem OAI.PolynomialPEPS.Subvolume.KernelNormalization.power_sum line 125
  14. theorem OAI.PolynomialPEPS.Subvolume.KernelNormalization.scale_inv_sq_le line 131
  15. theorem OAI.PolynomialPEPS.Subvolume.KernelNormalization.norm_sq_bound line 145
  16. def OAI.PolynomialPEPS.Subvolume.KernelPerturbation.cost line 165
  17. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.one_le_cost line 169
  18. def OAI.PolynomialPEPS.Subvolume.KernelPerturbation.normalized line 175
  19. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.normalized_posSemidef line 178
  20. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.normalized_capacity line 188
  21. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.normalized_eq_smul line 200
  22. theorem OAI.PolynomialPEPS.Subvolume.KernelPerturbation.normalized_factorization line 210