OAI/Probability/SKRatio/Matrices/Quadratic.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatioGaussian.ComplexSpectral.quadratic line 39
  2. def OAI.SKRatioGaussian.ComplexSpectral.unitSphere line 42
  3. def OAI.SKRatioGaussian.ComplexSpectral.lowerRayleigh line 44
  4. lemma OAI.SKRatioGaussian.ComplexSpectral.continuous_quadratic line 46
  5. lemma OAI.SKRatioGaussian.ComplexSpectral.compact_unitSphere line 51
  6. lemma OAI.SKRatioGaussian.ComplexSpectral.continuous_lowerRayleigh line 53
  7. lemma OAI.SKRatioGaussian.ComplexSpectral.quadratic_neg line 56
  8. lemma OAI.SKRatioGaussian.ComplexSpectral.lowerRayleigh_le line 59
  9. lemma OAI.SKRatioGaussian.ComplexSpectral.lowerRayleigh_ge line 65
  10. lemma OAI.SKRatioGaussian.ComplexSpectral.quadratic_eigenvector line 76
  11. lemma OAI.SKRatioGaussian.ComplexSpectral.eigenvalue_lower_bound line 80
  12. lemma OAI.SKRatioGaussian.ComplexSpectral.eigenvalue_upper_bound line 86
  13. lemma OAI.SKRatioGaussian.ComplexSpectral.spectral_interval_eventually line 93