OAI/Probability/SignedSweeps/SpectralAngle.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.trace_spectral line 14
  2. lemma OAI.SignedSweeps.quadratic_spectral line 18
  3. lemma OAI.SignedSweeps.eigenvector_mem_range line 34
  4. lemma OAI.SignedSweeps.trace_product_spectral line 42
  5. lemma OAI.SignedSweeps.positive_trace_product_nonneg line 53
  6. lemma OAI.SignedSweeps.positive_trace_product_le_squared_angle line 62
  7. lemma OAI.SignedSweeps.fixed_squared_inner_le_composition line 92
  8. lemma OAI.SignedSweeps.positive_trace_product_le_three_projection_norm line 106
  9. lemma OAI.SignedSweeps.symmetric_projection_contraction line 122
  10. lemma OAI.SignedSweeps.positive_projection_trace_le line 135
  11. lemma OAI.SignedSweeps.positive_commuting_projection line 153
  12. lemma OAI.SignedSweeps.positive_global_projection_trace_bound line 163