OAI/Combinatorics/Sidorenko/PairBounds.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.real_card_sigma_le line 9
  2. def OAI.SidorenkoCounterexample.pairFormDifference line 23
  3. theorem OAI.SidorenkoCounterexample.pairFormDifference_surjective line 26
  4. theorem OAI.SidorenkoCounterexample.pairFormDifference_graph line 33
  5. theorem OAI.SidorenkoCounterexample.pairFormDifference_nullity_bound line 36
  6. abbrev OAI.SidorenkoCounterexample.SubspacePairProfile line 50
  7. abbrev OAI.SidorenkoCounterexample.PairBaseCode line 52
  8. def OAI.SidorenkoCounterexample.pairBaseCode line 56
  9. theorem OAI.SidorenkoCounterexample.pairBaseCode_injective line 68
  10. theorem OAI.SidorenkoCounterexample.subspacePairProfile_card_upper line 75
  11. theorem OAI.SidorenkoCounterexample.subspacePairProfile_probability_bound line 103
  12. abbrev OAI.SidorenkoCounterexample.PairParameters line 132
  13. instance OAI.SidorenkoCounterexample.pairParametersFintype line 133
  14. abbrev OAI.SidorenkoCounterexample.DualPairBase line 136
  15. abbrev OAI.SidorenkoCounterexample.DualPairForms line 137
  16. abbrev OAI.SidorenkoCounterexample.CanonicalPairProfile line 139
  17. abbrev OAI.SidorenkoCounterexample.DualPairLiftEvent line 142
  18. abbrev OAI.SidorenkoCounterexample.CenterPairProfile line 144
  19. def OAI.SidorenkoCounterexample.dualPairProductEquiv line 147
  20. def OAI.SidorenkoCounterexample.canonicalPairProfileEquiv line 158
  21. def OAI.SidorenkoCounterexample.canonicalPairParameter line 162
  22. theorem OAI.SidorenkoCounterexample.dualGraph_pair_kernel_exact line 173
  23. theorem OAI.SidorenkoCounterexample.dualGraph_pair_kernel_ge line 182
  24. def OAI.SidorenkoCounterexample.canonicalPairCoding line 188
  25. theorem OAI.SidorenkoCounterexample.canonicalPairCoding_injective line 195
  26. theorem OAI.SidorenkoCounterexample.dualPairForms_card line 205
  27. theorem OAI.SidorenkoCounterexample.center_stratum_square line 214
  28. theorem OAI.SidorenkoCounterexample.dualPairLift_probability_bound line 221
  29. theorem OAI.SidorenkoCounterexample.pairPlanted_bound_one line 229
  30. theorem OAI.SidorenkoCounterexample.two_active_gain_bound line 269
  31. theorem OAI.SidorenkoCounterexample.canonical_center_pair_probability_bound line 298
  32. theorem OAI.SidorenkoCounterexample.canonical_center_pair_gain_bound line 315
  33. abbrev OAI.SidorenkoCounterexample.PairCenterSet line 350
  34. abbrev OAI.SidorenkoCounterexample.SymplecticCenterPairProfile line 352
  35. def OAI.SidorenkoCounterexample.symplecticCenterPairProfileEquiv line 355
  36. def OAI.SidorenkoCounterexample.pairCenterIsometryEquiv line 365
  37. def OAI.SidorenkoCounterexample.pairCenterProfileEquiv line 373
  38. theorem OAI.SidorenkoCounterexample.pairCenter_profile_card line 383
  39. theorem OAI.SidorenkoCounterexample.symplectic_center_stratum_card_eq line 399
  40. theorem OAI.SidorenkoCounterexample.symplectic_center_pair_gain_bound line 407
  41. def OAI.SidorenkoCounterexample.pairFaceDensity line 418
  42. theorem OAI.SidorenkoCounterexample.pairFaceDensity_nonneg line 422
  43. theorem OAI.SidorenkoCounterexample.normalized_pair_gain line 426
  44. theorem OAI.SidorenkoCounterexample.pairFaceDensity_gain_bound line 441
  45. theorem OAI.SidorenkoCounterexample.actual_profile_pair_sum_le line 485