OAI/Combinatorics/Sidorenko/LocalMoments.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.uniformMean_mul_card line 15
  2. theorem OAI.SidorenkoCounterexample.restrictionSign_count line 23
  3. def OAI.SidorenkoCounterexample.signedProjectorIsotropicEquiv line 40
  4. def OAI.SidorenkoCounterexample.pairRestrictionFraction line 71
  5. def OAI.SidorenkoCounterexample.isotropicRestrictionFraction line 77
  6. theorem OAI.SidorenkoCounterexample.pairCenter_card line 84
  7. theorem OAI.SidorenkoCounterexample.tripleCenter_card line 98
  8. def OAI.SidorenkoCounterexample.pairCoefficient line 132
  9. def OAI.SidorenkoCounterexample.tripleCoefficient line 136
  10. theorem OAI.SidorenkoCounterexample.pair_exponent_cancel line 141
  11. theorem OAI.SidorenkoCounterexample.triple_exponent_cancel line 148
  12. theorem OAI.SidorenkoCounterexample.pairCoefficient_normalized line 155
  13. theorem OAI.SidorenkoCounterexample.tripleCoefficient_normalized line 168
  14. theorem OAI.SidorenkoCounterexample.pairCoefficient_nonneg line 182
  15. theorem OAI.SidorenkoCounterexample.tripleCoefficient_nonneg line 186
  16. theorem OAI.SidorenkoCounterexample.pairCoefficient_tendsto line 191
  17. theorem OAI.SidorenkoCounterexample.tripleCoefficient_tendsto line 204
  18. theorem OAI.SidorenkoCounterexample.maxOrthogonal_card_lower line 235
  19. theorem OAI.SidorenkoCounterexample.halfIsotropic_card line 243
  20. theorem OAI.SidorenkoCounterexample.pairFamily_card_ge line 252
  21. theorem OAI.SidorenkoCounterexample.isotropicFamily_card_ge line 260
  22. theorem OAI.SidorenkoCounterexample.matrix_restriction_family_L1 line 274
  23. theorem OAI.SidorenkoCounterexample.pairRestrictionFraction_L1 line 294
  24. theorem OAI.SidorenkoCounterexample.isotropicRestrictionFraction_L1 line 304
  25. theorem OAI.SidorenkoCounterexample.uniformMean_sum line 330
  26. theorem OAI.SidorenkoCounterexample.uniformMean_coordinate line 335
  27. theorem OAI.SidorenkoCounterexample.uniformMean_update line 342
  28. theorem OAI.SidorenkoCounterexample.uniformMean_mul_right line 358
  29. theorem OAI.SidorenkoCounterexample.uniformMean_ite_le line 362
  30. def OAI.SidorenkoCounterexample.symmetricInverse line 387

    Source documentation

    Extend inversion by fixing singular forms. Unlike the total matrix inverse, this is a permutation of the entire symmetric-matrix probability space.

    noncomputable def symmetricInverse (D : ℕ) (M : SymMatrix K D) : SymMatrix K D :=
…

    Mentions: OAI.SidorenkoCounterexample.SymMatrix

  31. theorem OAI.SidorenkoCounterexample.symmetricInverse_involutive line 393
  32. def OAI.SidorenkoCounterexample.symmetricInverseEquiv line 407
  33. def OAI.SidorenkoCounterexample.pairLocal line 424
  34. def OAI.SidorenkoCounterexample.tripleLocal line 426
  35. def OAI.SidorenkoCounterexample.pairMatch line 430
  36. def OAI.SidorenkoCounterexample.tripleMatch line 433
  37. theorem OAI.SidorenkoCounterexample.pairLocal_card line 436
  38. theorem OAI.SidorenkoCounterexample.tripleLocal_card line 453
  39. theorem OAI.SidorenkoCounterexample.pairLocal_match line 471
  40. theorem OAI.SidorenkoCounterexample.pairLocal_mismatch line 480
  41. theorem OAI.SidorenkoCounterexample.tripleLocal_mismatch line 496
  42. theorem OAI.SidorenkoCounterexample.inverse_difference_det line 519
  43. theorem OAI.SidorenkoCounterexample.inverse_difference_nondegenerate line 528
  44. theorem OAI.SidorenkoCounterexample.matching_inverse_difference_split line 536
  45. theorem OAI.SidorenkoCounterexample.tripleLocal_match line 557
  46. theorem OAI.SidorenkoCounterexample.uniformMean_le_one line 584
  47. theorem OAI.SidorenkoCounterexample.uniformMean_subLeft line 589
  48. theorem OAI.SidorenkoCounterexample.pairRestrictionFraction_range line 595
  49. theorem OAI.SidorenkoCounterexample.isotropicRestrictionFraction_range line 601
  50. theorem OAI.SidorenkoCounterexample.uniformMean_inverse line 609
  51. theorem OAI.SidorenkoCounterexample.uniformMean_inverse_difference line 614
  52. theorem OAI.SidorenkoCounterexample.scalar_fraction_error line 643
  53. def OAI.SidorenkoCounterexample.matrixSplit line 652
  54. def OAI.SidorenkoCounterexample.pairError line 656
  55. def OAI.SidorenkoCounterexample.tripleError line 658
  56. def OAI.SidorenkoCounterexample.splitFractionError line 662
  57. theorem OAI.SidorenkoCounterexample.splitFractionError_nonneg line 665
  58. theorem OAI.SidorenkoCounterexample.pairError_pointwise line 668
  59. theorem OAI.SidorenkoCounterexample.tripleError_pointwise line 681
  60. theorem OAI.SidorenkoCounterexample.splitFractionError_mean line 706
  61. theorem OAI.SidorenkoCounterexample.pairError_mean line 719
  62. theorem OAI.SidorenkoCounterexample.tripleError_mean line 729
  63. theorem OAI.SidorenkoCounterexample.pairLocal_nonneg line 753
  64. theorem OAI.SidorenkoCounterexample.tripleLocal_nonneg line 755
  65. theorem OAI.SidorenkoCounterexample.pairError_nonneg line 759
  66. theorem OAI.SidorenkoCounterexample.tripleError_nonneg line 761
  67. theorem OAI.SidorenkoCounterexample.pairLocal_bound line 764
  68. theorem OAI.SidorenkoCounterexample.tripleLocal_bound line 772
  69. theorem OAI.SidorenkoCounterexample.localFraction_error_tendsto line 783
  70. theorem OAI.SidorenkoCounterexample.pairError_tendsto line 789
  71. theorem OAI.SidorenkoCounterexample.tripleError_tendsto line 801