OAI/MathematicalPhysics/PEPSSubvolume/ContourEnergy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Total crossing excitation bounds charged by physical boundaries.

  1. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.commute_opposite_lifts line 29
  2. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.commute_of_disjoint line 37
  3. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.region_card_singleton line 48
  4. theorem OAI.PolynomialPEPS.Subvolume.ContourEnergy.edge_decomposition line 52
  5. def OAI.PolynomialPEPS.Subvolume.ContourEnergy.Splits line 82
  6. instance OAI.PolynomialPEPS.Subvolume.ContourEnergy.splitsDecidable line 85
  7. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.not_splits line 90
  8. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.single_not_splits line 101
  9. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.cross_inner_disjoint line 105
  10. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.cross_outer_subset line 116
  11. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.neutral_cut_index line 127
  12. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.no_split_identity line 151
  13. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.edge_splits_iff line 165
  14. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.crossing_edge_error line 172
  15. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.boundary_sum line 203
  16. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.crossing_budget_sum line 209
  17. lemma OAI.PolynomialPEPS.Subvolume.ContourEnergy.edge_error_budget line 221
  18. theorem OAI.PolynomialPEPS.Subvolume.ContourEnergy.optimizer_excitation_bound line 260