OAI/Combinatorics/Sidorenko/Nullity.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.subspace_count_lower line 11

    Source documentation

    The elementary matching lower Grassmann bound.

    theorem subspace_count_lower (k : ℕ) (hk : k ≤ finrank K V) :
    (Fintype.card K : ℝ)^(k*(finrank K V-k)) ≤ Nat.card (DimSubspace K V k) := by
…

    Mentions: OAI.SidorenkoCounterexample.DimSubspace

  2. theorem OAI.SidorenkoCounterexample.containment_quotient_finrank line 41
  3. def OAI.SidorenkoCounterexample.containingSubspaceEquiv line 48
  4. theorem OAI.SidorenkoCounterexample.containingSubspace_card_bounds line 69
  5. abbrev OAI.SidorenkoCounterexample.SubspaceTripleProfile line 93
  6. abbrev OAI.SidorenkoCounterexample.PairSubspaceConfig line 99
  7. abbrev OAI.SidorenkoCounterexample.SubspaceTripleCompletion line 102
  8. theorem OAI.SidorenkoCounterexample.triple_pairwise_disjoint line 107
  9. def OAI.SidorenkoCounterexample.subspaceProfile_to_config line 118
  10. theorem OAI.SidorenkoCounterexample.subspaceProfile_to_config_injective line 128
  11. theorem OAI.SidorenkoCounterexample.disjoint_sup_finrank line 136
  12. theorem OAI.SidorenkoCounterexample.pairSubspaceConfig_card_upper line 143
  13. theorem OAI.SidorenkoCounterexample.subspaceTripleCompletion_card_upper line 164
  14. def OAI.SidorenkoCounterexample.subspaceTripleExponent line 187
  15. theorem OAI.SidorenkoCounterexample.subspaceTripleProfile_card_upper line 191
  16. def OAI.SidorenkoCounterexample.restrictDimSubspace line 223
  17. def OAI.SidorenkoCounterexample.restrictTripleProfile line 227
  18. abbrev OAI.SidorenkoCounterexample.SubspaceTripleSpanProfile line 252
  19. def OAI.SidorenkoCounterexample.spanProfileInjection line 256
  20. theorem OAI.SidorenkoCounterexample.spanProfileInjection_injective line 263
  21. theorem OAI.SidorenkoCounterexample.subspaceTripleSpanProfile_card_upper line 288
  22. theorem OAI.SidorenkoCounterexample.subspace_span_cost_identity line 324
  23. theorem OAI.SidorenkoCounterexample.subspace_span_probability_bound line 339
  24. theorem OAI.SidorenkoCounterexample.coannihilator_finrank line 373
  25. def OAI.SidorenkoCounterexample.dualDimSubspaceEquiv line 378
  26. theorem OAI.SidorenkoCounterexample.coannihilator_common_finrank line 391
  27. def OAI.SidorenkoCounterexample.dualGraph line 398
  28. theorem OAI.SidorenkoCounterexample.dualGraph_vertical_dim line 402
  29. theorem OAI.SidorenkoCounterexample.dualGraph_vertical_subspace line 410
  30. theorem OAI.SidorenkoCounterexample.dualGraph_common_zero line 431
  31. theorem OAI.SidorenkoCounterexample.symmetric_nullity_probability_bound_all line 452
  32. theorem OAI.SidorenkoCounterexample.planted_nullity_probability_bound_all line 471
  33. theorem OAI.SidorenkoCounterexample.lift_pair_profile_probability_bound_all line 501
  34. abbrev OAI.SidorenkoCounterexample.DualProfileForms line 542
  35. abbrev OAI.SidorenkoCounterexample.DualLiftEvent line 545
  36. theorem OAI.SidorenkoCounterexample.dualProfileForms_card line 552
  37. theorem OAI.SidorenkoCounterexample.dual_lift_probability_bound line 563
  38. theorem OAI.SidorenkoCounterexample.subspace_profile_constraints line 599
  39. theorem OAI.SidorenkoCounterexample.center_stratum_cube line 640
  40. theorem OAI.SidorenkoCounterexample.dual_lift_sum_probability_bound line 648
  41. abbrev OAI.SidorenkoCounterexample.CenterStratum line 690
  42. def OAI.SidorenkoCounterexample.dualPairStratumEquiv line 693
  43. theorem OAI.SidorenkoCounterexample.dualPairStratumEquiv_apply line 699
  44. abbrev OAI.SidorenkoCounterexample.DualBaseTriple line 703
  45. abbrev OAI.SidorenkoCounterexample.DualBaseForms line 705
  46. def OAI.SidorenkoCounterexample.dualBaseTripleGraph line 707
  47. def OAI.SidorenkoCounterexample.dualTripleStratumEquiv line 711
  48. theorem OAI.SidorenkoCounterexample.dualTripleStratumEquiv_graph line 724
  49. theorem OAI.SidorenkoCounterexample.dualGraph_pair_finrank_ge line 729
  50. abbrev OAI.SidorenkoCounterexample.CanonicalLiftProfile line 737
  51. theorem OAI.SidorenkoCounterexample.coannihilator_pair_finrank line 753
  52. theorem OAI.SidorenkoCounterexample.dualGraph_pair_finrank_le line 761
  53. theorem OAI.SidorenkoCounterexample.dualGraph_pair_extra_feasible line 770
  54. theorem OAI.SidorenkoCounterexample.dual_common_pair_extra_feasible line 781
  55. abbrev OAI.SidorenkoCounterexample.FourDims line 821
  56. def OAI.SidorenkoCounterexample.BaseFeasible line 822
  57. abbrev OAI.SidorenkoCounterexample.BaseParameters line 830
  58. def OAI.SidorenkoCounterexample.canonicalLiftFourDims line 832
  59. def OAI.SidorenkoCounterexample.canonicalLiftSubspaces line 843
  60. theorem OAI.SidorenkoCounterexample.canonicalLift_feasible line 850
  61. theorem OAI.SidorenkoCounterexample.dualGraph_pair_gap_bound line 863
  62. def OAI.SidorenkoCounterexample.dualLift_of_exactDims line 873
  63. def OAI.SidorenkoCounterexample.canonicalLiftCoding line 886
  64. theorem OAI.SidorenkoCounterexample.canonicalLiftCoding_injective line 895
  65. abbrev OAI.SidorenkoCounterexample.CenterTripleProfile line 906
  66. def OAI.SidorenkoCounterexample.canonicalCenterProfileEquiv line 913
  67. instance OAI.SidorenkoCounterexample.baseParametersFintype line 924
  68. def OAI.SidorenkoCounterexample.reducedPlantedExponent line 926
  69. def OAI.SidorenkoCounterexample.reducedPlantedConstant line 933
  70. theorem OAI.SidorenkoCounterexample.reducedPlanted_bound_one line 939
  71. theorem OAI.SidorenkoCounterexample.canonical_center_profile_probability_bound line 977