OAI/MathematicalPhysics/CriticalSK/MinMax.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.basisSpan line 22
  2. lemma OAI.CriticalSK.basisSpan_finrank line 26
  3. lemma OAI.CriticalSK.basisSpan_repr_zero line 33
  4. lemma OAI.CriticalSK.basisSpan_intersection_unit line 47
  5. def OAI.CriticalSK.basisQuadratic line 65
  6. lemma OAI.CriticalSK.basis_sum_squares line 69
  7. lemma OAI.CriticalSK.basisQuadratic_le line 75
  8. lemma OAI.CriticalSK.basisQuadratic_ge line 88
  9. lemma OAI.CriticalSK.basis_minmax_upper line 100
  10. lemma OAI.CriticalSK.basis_minmax_lower line 120
  11. lemma OAI.CriticalSK.eigenbasisQuadratic_eq line 140
  12. lemma OAI.CriticalSK.eigenvalue_form_comparison line 151