OAI/MathematicalPhysics/PEPSSubvolume/FlatDirection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Flat second variations and vanishing optimizing kernel directions.

  1. theorem OAI.PolynomialPEPS.Subvolume.OptimizerFlatDirection.second_variation line 22
  2. theorem OAI.PolynomialPEPS.Subvolume.OptimizerFlatDirection.first_direction_vanishes line 64
  3. theorem OAI.PolynomialPEPS.Subvolume.OptimizerFlatDirection.mixed_direction_vanishes line 71
  4. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.affine_output line 96
  5. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.perturbation_envelope line 107
  6. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.kernel_output_zero line 153