OAI/Probability/SignedSweeps/ProvedRanges4.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SignedSweeps.missingCellFactor_le_exp_holes line 12
  2. def OAI.SignedSweeps.splitBinary line 30
  3. def OAI.SignedSweeps.sweepBoard line 37
  4. def OAI.SignedSweeps.columnGroup line 41
  5. def OAI.SignedSweeps.rowGroup line 44
  6. lemma OAI.SignedSweeps.first_layer_le_columns line 47
  7. lemma OAI.SignedSweeps.last_layer_le_rows line 63
  8. def OAI.SignedSweeps.columnSweep line 78
  9. def OAI.SignedSweeps.rowSweep line 81
  10. theorem OAI.SignedSweeps.sweepOperator_split line 84
  11. lemma OAI.SignedSweeps.columnSweep_contraction line 91
  12. lemma OAI.SignedSweeps.rowSweep_contraction line 99
  13. lemma OAI.SignedSweeps.trace_product_pow_cycle line 118
  14. lemma OAI.SignedSweeps.trace_positiveSquare_orientations line 138
  15. lemma OAI.SignedSweeps.trace_positiveSquare_product line 143
  16. def OAI.SignedSweeps.columnSquarePower line 161
  17. def OAI.SignedSweeps.rowSquarePower line 164
  18. lemma OAI.SignedSweeps.columnSquarePower_positive line 167
  19. lemma OAI.SignedSweeps.rowSquarePower_positive line 172
  20. lemma OAI.SignedSweeps.sweepSquare_trace_split line 175
  21. lemma OAI.SignedSweeps.exists_unit_eigenvector line 193
  22. lemma OAI.SignedSweeps.orthonormal_head_complement line 205
  23. theorem OAI.SignedSweeps.exists_schur_basis line 220
  24. lemma OAI.SignedSweeps.upper_triangular_mul_diagonal line 297
  25. lemma OAI.SignedSweeps.upper_triangular_pow_diagonal line 307
  26. lemma OAI.SignedSweeps.schur_trace_power line 328
  27. lemma OAI.SignedSweeps.quadratic_power_spectral line 337
  28. lemma OAI.SignedSweeps.quadratic_power_jensen line 354
  29. lemma OAI.SignedSweeps.unit_diagonal_power_le line 368
  30. theorem OAI.SignedSweeps.trace_even_power_le_square line 382
  31. lemma OAI.SignedSweeps.trace_product_double_le line 392
  32. theorem OAI.SignedSweeps.dyadic_trace_product_le line 403
  33. theorem OAI.SignedSweeps.sweepSquare_dyadic_trace_split line 424