OAI/MathematicalPhysics/PEPSSubvolume/TensorDecomposition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded decomposition of local support across a contour.

  1. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.lift_split_tensor line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.liftLocal_compl_join line 43
  3. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.tensorAcross_one_left line 65
  4. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.tensorAcross_eq_product line 75
  5. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.liftBetween_norm_le line 84
  6. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.opNorm_liftLocal line 89
  7. theorem OAI.PolynomialPEPS.Subvolume.LocalTensorDecomposition.exists_local_tensor_decomposition line 96