OAI/MathematicalPhysics/PEPSSubvolume/Transition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Local transition functionals and descending trace stripping.

  1. def OAI.PolynomialPEPS.Subvolume.ActualTransition.replacementOutput line 26
  2. theorem OAI.PolynomialPEPS.Subvolume.ActualTransition.optimizer_moment_commute line 42
  3. theorem OAI.PolynomialPEPS.Subvolume.ActualTransition.mixed_kernel_moment_zero line 83
  4. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.orderedPrefix_split line 118
  5. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.orderedPrefix_shift_head line 126
  6. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.orderedPrefix_replace_split line 137
  7. def OAI.PolynomialPEPS.Subvolume.TraceStripping.insertedProduct line 153
  8. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.insertedProduct_at_end line 156
  9. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.insertedProduct_right line 159
  10. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.insertedProduct_left line 167
  11. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.strip_outer line 175
  12. theorem OAI.PolynomialPEPS.Subvolume.TraceStripping.optimizer_strip_outer line 192