OAI/MathematicalPhysics/PEPSFilters/PinnedEntropy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Pinned-sector interpolation and the original-state entropy upper comparison.

  1. def OAI.PolynomialPEPS.PinnedEntropy.localMapCLM line 21
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.localMapCLM_apply line 28
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_norm line 32
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_inner_hermitian line 35
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.liftLocal_hermitian line 39
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.inner_projection line 44
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.inner_projection_commute line 49
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.pinned_norm_sq line 56
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.regionCorner_calculus line 71
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.original_support_fixes line 80
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.corner_power_fixes line 85
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.ground_log_expectation line 97
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Spectral.applyFn_smul line 116
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.corner_right_projection line 128
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.corner_log_derivative line 134
  16. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.pinned_sector_comparison line 161
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.asMap_sum line 263
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.pinned_expectation_sum line 269
  19. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.upperComparison_zero line 298