OAI/MathematicalPhysics/PEPSSubvolume/GroundTilt.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Ground-state Schmidt tilts and scalar zero-weight identities.

  1. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.coefficient_lift line 26
  2. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.reducedDensity_lift line 34
  3. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.coefficient_injective line 41
  4. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.lift_action_eq_of_mul_density line 48
  5. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.spectral_action_eq line 65
  6. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.norm_sq_density_trace line 80
  7. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.trace_spectral line 91
  8. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.spectral_lift_hermitian line 97
  9. lemma OAI.PolynomialPEPS.Subvolume.TiltScalar.tilted_weight line 113
  10. lemma OAI.PolynomialPEPS.Subvolume.TiltScalar.tilt_exponent line 127
  11. lemma OAI.PolynomialPEPS.Subvolume.TiltScalar.tilt_recovery line 130
  12. lemma OAI.PolynomialPEPS.Subvolume.TiltScalar.tilt_inverse_recovery line 134
  13. lemma OAI.PolynomialPEPS.Subvolume.TiltScalar.tilt_pairing line 137
  14. lemma OAI.PolynomialPEPS.Subvolume.TiltScalar.exponent_small line 148
  15. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.spectral_real_star line 171
  16. def OAI.PolynomialPEPS.Subvolume.GroundTilt.tiltFilter line 181
  17. def OAI.PolynomialPEPS.Subvolume.GroundTilt.tilt line 187
  18. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.tilt_density line 192
  19. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.tilt_norm_sq line 210
  20. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.tilt_pairing_eq line 220
  21. lemma OAI.PolynomialPEPS.Subvolume.GroundTilt.untilt line 233