OAI/MathematicalPhysics/PEPSFilters/ContourEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Propagated site and edge energy estimates across nested contours.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.regularized_edge_crossing line 30
  2. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.Crosses line 65
  3. instance OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.(instance at line 68) line 68
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.crossing_before_disjoint line 71
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.crossing_after_contains line 88
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.not_crossing_classify line 103
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.propagate_site_expectation line 118
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.propagate_edge_no_crossing line 132
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.regularized_propagated_edge line 147