OAI/Analysis/TriangularHilbert/Support.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularHilbert.MatrixEnergy.sqrt_mul_eq_zero_of_mul_eq_zero line 14
  2. lemma OAI.TriangularHilbert.MatrixEnergy.mul_sqrt_eq_zero_of_mul_eq_zero line 23
  3. lemma OAI.TriangularHilbert.MatrixEnergy.sqrt_add_projection line 33
  4. lemma OAI.TriangularHilbert.MatrixEnergy.energy_add_projection line 44
  5. lemma OAI.TriangularHilbert.MatrixEnergy.energyGradient_add_projection line 52
  6. lemma OAI.TriangularHilbert.MatrixEnergy.hessianCost_add_projection line 59
  7. lemma OAI.TriangularHilbert.MatrixEnergy.exists_kernel_projection line 95
  8. lemma OAI.TriangularHilbert.MatrixEnergy.deriv_mul_projection_eq_zero line 147
  9. lemma OAI.TriangularHilbert.MatrixEnergy.projection_mul_deriv_eq_zero line 154
  10. lemma OAI.TriangularHilbert.MatrixEnergy.hermitian_mul_zero_flip line 162
  11. def OAI.TriangularHilbert.MatrixEnergy.hessianPair line 167
  12. lemma OAI.TriangularHilbert.MatrixEnergy.hessianPair_eq_PD line 170
  13. lemma OAI.TriangularHilbert.MatrixEnergy.hessianPair_add_projection line 179
  14. theorem OAI.TriangularHilbert.MatrixEnergy.energy_supported_path_hasDerivAt line 190
  15. theorem OAI.TriangularHilbert.MatrixEnergy.energyGradient_supported_path_hasDerivAt line 209