OAI/Combinatorics/Sidorenko/Signs.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.characterSignIndicator line 12
  2. theorem OAI.SidorenkoCounterexample.characterSignIndicator_nonneg line 15
  3. theorem OAI.SidorenkoCounterexample.characterSignIndicator_le_one line 17
  4. theorem OAI.SidorenkoCounterexample.characterSignIndicator_formula line 20
  5. theorem OAI.SidorenkoCounterexample.uniformMean_singleton line 29
  6. theorem OAI.SidorenkoCounterexample.uniformMean_nonzero line 33
  7. theorem OAI.SidorenkoCounterexample.uniformMean_character line 41
  8. theorem OAI.SidorenkoCounterexample.uniformMean_characterSignIndicator line 48
  9. def OAI.SidorenkoCounterexample.scalarAffineEquiv line 57
  10. theorem OAI.SidorenkoCounterexample.uniformMean_affine line 64
  11. def OAI.SidorenkoCounterexample.symmetricSingularProb line 71
  12. def OAI.SidorenkoCounterexample.symmetricSignProb line 73
  13. theorem OAI.SidorenkoCounterexample.border_singularMean line 76
  14. theorem OAI.SidorenkoCounterexample.border_signMean line 83
  15. theorem OAI.SidorenkoCounterexample.symmetricSingularProb_nonneg line 90
  16. theorem OAI.SidorenkoCounterexample.symmetricSingularProb_zero line 93
  17. theorem OAI.SidorenkoCounterexample.symmetricSingularProb_succ line 97
  18. theorem OAI.SidorenkoCounterexample.symmetricSingularProb_bound line 123
  19. theorem OAI.SidorenkoCounterexample.symmetricSignProb_nonneg line 134
  20. theorem OAI.SidorenkoCounterexample.symmetricSignProb_le_one line 137
  21. theorem OAI.SidorenkoCounterexample.symmetricSignProb_succ_error line 140
  22. theorem OAI.SidorenkoCounterexample.symmetricSignProb_error line 177
  23. theorem OAI.SidorenkoCounterexample.discriminantSign_nondegenerate line 205

    Source documentation

    For a nondegenerate form, the radical quotient definition reduces to its ordinary determinant character in any basis.

    theorem discriminantSign_nondegenerate (B : LinearMap.BilinForm K V)
    (hBs : B.IsSymm) (hB : B.Nondegenerate)
    {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι K V) :
    discriminantSign B hBs = quadraticChar K (B.toMatrix b).det := by
…

    Mentions: OAI.SidorenkoCounterexample.discriminantSign

  24. def OAI.SidorenkoCounterexample.orthogonalSumForm line 217
  25. theorem OAI.SidorenkoCounterexample.orthogonalSumForm_apply line 222
  26. theorem OAI.SidorenkoCounterexample.orthogonalSumForm_isSymm line 226
  27. theorem OAI.SidorenkoCounterexample.orthogonalSumForm_nondegenerate line 233
  28. theorem OAI.SidorenkoCounterexample.orthogonalSumForm_matrix line 254
  29. theorem OAI.SidorenkoCounterexample.discriminantSign_add line 267

    Source documentation

    When the ranks add without loss and the sum is nondegenerate, determinant characters multiply. The proof uses the actual radical quotients.

    theorem discriminantSign_add (A B : LinearMap.BilinForm K V)
    (hA : A.IsSymm) (hB : B.IsSymm) (hS : (A+B).Nondegenerate)
    (hdim : finrank K (V ⧸ A.ker) + finrank K (V ⧸ B.ker) = finrank K V) :
    discriminantSign (A+B) (hA.add hB) = discriminantSign A hA * discriminantSign B hB := by
…

    Mentions: OAI.SidorenkoCounterexample.discriminantSign

  30. theorem OAI.SidorenkoCounterexample.half_rank_pair_sign line 309
  31. theorem OAI.SidorenkoCounterexample.symFormQuotient_nondegenerate_iff line 354
  32. theorem OAI.SidorenkoCounterexample.discriminantSign_pullback_nondegenerate line 370
  33. def OAI.SidorenkoCounterexample.signedRadicalFiberEquiv line 378
  34. def OAI.SidorenkoCounterexample.nonsingularSignedMatrixEquiv line 408
  35. theorem OAI.SidorenkoCounterexample.nonsingularSignedForm_card line 426
  36. theorem OAI.SidorenkoCounterexample.signedRadicalFiber_card line 440
  37. def OAI.SidorenkoCounterexample.signedNullityFiberEquiv line 457
  38. theorem OAI.SidorenkoCounterexample.signedNullityForm_card line 471
  39. def OAI.SidorenkoCounterexample.matrixFormEquiv line 493
  40. theorem OAI.SidorenkoCounterexample.signedLayer_card_exact line 497
  41. theorem OAI.SidorenkoCounterexample.symmetricSignProb_card line 521
  42. theorem OAI.SidorenkoCounterexample.layerMass_exact line 529
  43. theorem OAI.SidorenkoCounterexample.binary_norm_surjective line 556
  44. theorem OAI.SidorenkoCounterexample.nondegenerate_ne_zero_of_pos line 575
  45. theorem OAI.SidorenkoCounterexample.orthogonal_line_finrank line 587
  46. theorem OAI.SidorenkoCounterexample.symmetric_norm_surjective line 595
  47. def OAI.SidorenkoCounterexample.BilinEquivalent line 619
  48. def OAI.SidorenkoCounterexample.scalarBilin line 622
  49. theorem OAI.SidorenkoCounterexample.scalarBilin_apply line 623
  50. theorem OAI.SidorenkoCounterexample.scalarBilin_symm line 627
  51. theorem OAI.SidorenkoCounterexample.scalarBilin_nondegenerate line 630
  52. def OAI.SidorenkoCounterexample.lineOrthogonalEquiv line 635
  53. theorem OAI.SidorenkoCounterexample.lineOrthogonalEquiv_apply line 641
  54. theorem OAI.SidorenkoCounterexample.lineOrthogonalEquiv_form line 645
  55. theorem OAI.SidorenkoCounterexample.discriminantSign_isometry line 657
  56. theorem OAI.SidorenkoCounterexample.discriminantSign_orthogonalSum line 668
  57. theorem OAI.SidorenkoCounterexample.discriminantSign_scalar line 679
  58. theorem OAI.SidorenkoCounterexample.discriminantSign_line_complement line 685
  59. theorem OAI.SidorenkoCounterexample.scalarBilin_equivalent_of_sign line 707
  60. theorem OAI.SidorenkoCounterexample.one_dimensional_form line 722
  61. theorem OAI.SidorenkoCounterexample.one_dimensional_equivalent line 733
  62. theorem OAI.SidorenkoCounterexample.symmetric_equivalent_of_dim_sign line 771
  63. theorem OAI.SidorenkoCounterexample.uniformMean_surjective_linear line 840
  64. instance OAI.SidorenkoCounterexample.symForm_fintype line 863
  65. def OAI.SidorenkoCounterexample.formSignIndicator line 864
  66. def OAI.SidorenkoCounterexample.formSingularIndicator line 867
  67. theorem OAI.SidorenkoCounterexample.formSignIndicator_matrix line 871
  68. theorem OAI.SidorenkoCounterexample.formSingularIndicator_matrix line 883
  69. theorem OAI.SidorenkoCounterexample.formSignIndicator_nonneg line 889
  70. theorem OAI.SidorenkoCounterexample.formSignIndicator_le_one line 892
  71. theorem OAI.SidorenkoCounterexample.formSingularIndicator_nonneg line 896
  72. theorem OAI.SidorenkoCounterexample.formSingularMean_bound line 899
  73. theorem OAI.SidorenkoCounterexample.formSignMean_error line 911
  74. theorem OAI.SidorenkoCounterexample.uniformMean_restrict line 926