OAI/Probability/SignedSweeps/SupportInverse.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.basisDiagonal line 14
  2. lemma OAI.SignedSweeps.basisDiagonal_apply_basis line 19
  3. lemma OAI.SignedSweeps.basisDiagonal_toMatrix line 24
  4. lemma OAI.SignedSweeps.basisDiagonal_positive line 34
  5. lemma OAI.SignedSweeps.basisDiagonal_mul line 42
  6. def OAI.SignedSweeps.positiveRoot line 51
  7. def OAI.SignedSweeps.supportInverseRoot line 55
  8. def OAI.SignedSweeps.spectralSupport line 59
  9. lemma OAI.SignedSweeps.positiveRoot_positive line 63
  10. lemma OAI.SignedSweeps.supportInverseRoot_positive line 67
  11. lemma OAI.SignedSweeps.spectralSupport_positive line 71
  12. lemma OAI.SignedSweeps.positiveRoot_square line 77
  13. lemma OAI.SignedSweeps.supportInverseRoot_mul_root line 86
  14. lemma OAI.SignedSweeps.root_mul_supportInverseRoot line 96
  15. lemma OAI.SignedSweeps.supportInverseRoot_normalize line 103
  16. lemma OAI.SignedSweeps.spectralSupport_idempotent line 119
  17. lemma OAI.SignedSweeps.spectralSupport_mul line 126
  18. def OAI.SignedSweeps.densityMean line 135
  19. lemma OAI.SignedSweeps.densityMean_positive line 139
  20. lemma OAI.SignedSweeps.densityMean_sum line 147
  21. lemma OAI.SignedSweeps.normalizedDensity_positive line 151
  22. lemma OAI.SignedSweeps.normalizedDensity_sum line 160
  23. def OAI.SignedSweeps.densityCell line 168
  24. lemma OAI.SignedSweeps.densityCell_nonneg line 174
  25. lemma OAI.SignedSweeps.densityCell_sum_le line 179
  26. theorem OAI.SignedSweeps.normalized_density_product_bound line 192
  27. lemma OAI.SignedSweeps.positiveRoot_quadratic line 200
  28. lemma OAI.SignedSweeps.positive_quadratic_zero_iff line 208
  29. lemma OAI.SignedSweeps.densityMean_kernel line 217
  30. lemma OAI.SignedSweeps.density_right_support line 227
  31. lemma OAI.SignedSweeps.density_left_support line 241
  32. lemma OAI.SignedSweeps.norm_sq_le_positiveSquare_trace line 249
  33. lemma OAI.SignedSweeps.densityCell_norm_bound line 271
  34. theorem OAI.SignedSweeps.normalized_density_norm_product_bound line 295