OAI/Combinatorics/Sidorenko/Projections.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.FormSelfAdjoint line 13
  2. theorem OAI.SidorenkoCounterexample.selfAdjoint_projection_ker line 16
  3. theorem OAI.SidorenkoCounterexample.selfAdjoint_projection_nondegenerate line 31
  4. def OAI.SidorenkoCounterexample.formProjection line 39
  5. theorem OAI.SidorenkoCounterexample.formProjection_idempotent line 43
  6. theorem OAI.SidorenkoCounterexample.formProjection_range line 47
  7. theorem OAI.SidorenkoCounterexample.formProjection_selfAdjoint line 51
  8. def OAI.SidorenkoCounterexample.SelfAdjointIdempotent line 71
  9. def OAI.SidorenkoCounterexample.selfAdjointProjectionEquiv line 74
  10. theorem OAI.SidorenkoCounterexample.matrix_formSelfAdjoint_iff line 104
  11. theorem OAI.SidorenkoCounterexample.matrix_selfAdjoint_of_symmetric line 112
  12. theorem OAI.SidorenkoCounterexample.matrix_projection_idempotent line 117
  13. def OAI.SidorenkoCounterexample.CenterProjection line 124
  14. def OAI.SidorenkoCounterexample.centerToProjection line 127
  15. theorem OAI.SidorenkoCounterexample.projection_to_center_symmetric line 132
  16. theorem OAI.SidorenkoCounterexample.projection_to_center_identity line 145
  17. def OAI.SidorenkoCounterexample.centerProjectionEquiv line 155
  18. def OAI.SidorenkoCounterexample.centerSubspaceEquiv line 171
  19. theorem OAI.SidorenkoCounterexample.matrix_toLin_surjective line 192
  20. theorem OAI.SidorenkoCounterexample.matrix_mul_range line 200
  21. theorem OAI.SidorenkoCounterexample.centerSubspaceEquiv_val line 205
  22. theorem OAI.SidorenkoCounterexample.center_restriction_nondegenerate line 209
  23. theorem OAI.SidorenkoCounterexample.center_form_pullback line 216
  24. theorem OAI.SidorenkoCounterexample.center_second_equation line 222
  25. theorem OAI.SidorenkoCounterexample.center_discriminant line 251
  26. theorem OAI.SidorenkoCounterexample.discriminantSign_complements line 282
  27. theorem OAI.SidorenkoCounterexample.center_complement_equation line 303
  28. theorem OAI.SidorenkoCounterexample.center_complement_ranges line 310
  29. theorem OAI.SidorenkoCounterexample.center_complement_orthogonal line 324
  30. theorem OAI.SidorenkoCounterexample.quadraticChar_inverse line 340
  31. theorem OAI.SidorenkoCounterexample.center_complement_sign line 345
  32. def OAI.SidorenkoCounterexample.dualKerEquiv line 381
  33. theorem OAI.SidorenkoCounterexample.dualKerEquiv_apply line 394
  34. def OAI.SidorenkoCounterexample.rankOneForm line 397
  35. theorem OAI.SidorenkoCounterexample.rankOneForm_apply line 399
  36. theorem OAI.SidorenkoCounterexample.dualKer_finrank line 402
  37. def OAI.SidorenkoCounterexample.dualKerBasis line 411
  38. theorem OAI.SidorenkoCounterexample.dualKerBasis_inl line 415
  39. theorem OAI.SidorenkoCounterexample.dualKerBasis_inr line 419
  40. theorem OAI.SidorenkoCounterexample.rankOne_shift_matrix line 424
  41. theorem OAI.SidorenkoCounterexample.rankOne_shift_mean line 457