OAI/Computability/DirectedFeedback/Analysis/MatrixNoise.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Fourier.MatrixParityRow.traceCharacter_comp line 20
  2. theorem OAI.DFVSGames.Fourier.MatrixParityRow.traceCharacter_re_add line 26
  3. theorem OAI.DFVSGames.Fourier.MatrixParityRow.row_character_average line 34
  4. theorem OAI.DFVSGames.Fourier.MatrixParityRow.row_spectral_average line 46
  5. theorem OAI.DFVSGames.Fourier.MatrixParityRow.row_fourier_average line 59
  6. theorem OAI.DFVSGames.Fourier.MatrixParityRow.shift_character_average line 70
  7. theorem OAI.DFVSGames.Fourier.MatrixParityRow.shift_fourier_average line 79
  8. theorem OAI.DFVSGames.Fourier.MatrixParityRow.row_shift_fourier_average line 98
  9. theorem OAI.DFVSGames.Fourier.MatrixParityRow.signed_coefficient_le_abs line 110
  10. theorem OAI.DFVSGames.Fourier.MatrixParityRow.coefficient_of_dense_row line 116
  11. theorem OAI.DFVSGames.Fourier.MatrixParityRow.coefficient_of_folded_dense_row line 179
  12. lemma OAI.DFVSGames.Fourier.MatrixParityRow.color_card_bound line 198
  13. lemma OAI.DFVSGames.Fourier.MatrixParityRow.fixed_row_folded line 215
  14. theorem OAI.DFVSGames.Fourier.MatrixParityRow.lemma53_quotient line 229
  15. theorem OAI.DFVSGames.Fourier.MatrixNoise.character_average_shift line 284
  16. def OAI.DFVSGames.Fourier.MatrixNoise.dotCharacter line 299
  17. theorem OAI.DFVSGames.Fourier.MatrixNoise.dotCharacter_apply line 304
  18. theorem OAI.DFVSGames.Fourier.MatrixNoise.dotCharacter_eq_zero_iff line 307
  19. theorem OAI.DFVSGames.Fourier.MatrixNoise.average_dotCharacter line 320
  20. theorem OAI.DFVSGames.Fourier.MatrixNoise.average_rankOne_character line 328
  21. def OAI.DFVSGames.Fourier.MatrixNoise.noiseOperator line 335
  22. def OAI.DFVSGames.Fourier.MatrixNoise.noiseEigenvalue line 340
  23. theorem OAI.DFVSGames.Fourier.MatrixNoise.noiseOperator_character line 344
  24. theorem OAI.DFVSGames.Fourier.MatrixNoise.noiseEigenvalue_nonneg line 357
  25. theorem OAI.DFVSGames.Fourier.MatrixNoise.noiseEigenvalue_le_one line 365
  26. def OAI.DFVSGames.Fourier.MatrixNoise.evaluationCharacter line 379
  27. theorem OAI.DFVSGames.Fourier.MatrixNoise.evaluationCharacter_apply line 384
  28. theorem OAI.DFVSGames.Fourier.MatrixNoise.evaluationCharacter_eq_zero_iff line 387
  29. theorem OAI.DFVSGames.Fourier.MatrixNoise.average_evaluationCharacter line 400
  30. theorem OAI.DFVSGames.Fourier.MatrixNoise.average_smulRight_character line 409
  31. def OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseOperator line 417
  32. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseOperator_sum line 421
  33. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseOperator_smul line 430
  34. def OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseEigenvalue line 441
  35. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseOperator_character line 444
  36. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseEigenvalue_nonneg line 458
  37. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseEigenvalue_le_one line 466
  38. def OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator line 477
  39. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_complex line 481
  40. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_eq_re line 493
  41. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_sum line 500
  42. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_smul line 509
  43. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_character line 520
  44. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_expansion line 534
  45. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_pairing line 558
  46. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_selfAdjoint line 578
  47. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_coeff line 598
  48. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_energy line 618
  49. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_nonneg line 625
  50. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearRealNoiseOperator_cross_le line 633
  51. theorem OAI.DFVSGames.Fourier.MatrixNoise.linearNoiseOperator_energy_re line 652