OAI/MathematicalPhysics/PEPSSubvolume/MixedKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Mixed singular residual bounds from simultaneous perturbations.

  1. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.real_complex_smul line 24
  2. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.two_affine_output line 28
  3. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.two_affine_kernel_output line 44
  4. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.mixed_scalar_bound line 61
  5. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.mixed_normalized_bound line 74
  6. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.mixed_envelope line 146
  7. theorem OAI.PolynomialPEPS.Subvolume.ActualKernel.mixed_transition_zero line 192