OAI/Combinatorics/Sidorenko/Spans.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SidorenkoCounterexample.localSpan line 13

    Source documentation

    The span of the spaces on the edges incident to a given vertex.

    def localSpan (s : Finset (Finset P)) (H : Finset P → Submodule K V) (i : P) :
    Submodule K V := (s.filter fun e => i ∈ e).sup H
…
  2. theorem OAI.SidorenkoCounterexample.localSpan_le line 17
  3. theorem OAI.SidorenkoCounterexample.localSpan_insert line 22
  4. theorem OAI.SidorenkoCounterexample.local_rank_insert line 30
  5. theorem OAI.SidorenkoCounterexample.span_inequality_with_rigidity line 49

    Source documentation

    The dimension bound, together with its equality rigidity. Equality forces the entire edge-space family to be a direct sum.

    theorem span_inequality_with_rigidity (s : Finset (Finset P))
    (H : Finset P → Submodule K V) (hs : ∀ e ∈ s, e.card = 2) :
    2 * finrank K (s.sup H : Submodule K V) ≤ ∑ i, finrank K (localSpan s H i) ∧
    ((∑ i, finrank K (localSpan s H i)) = 2 * finrank K (s.sup H : Submodule K V) →
      s.SupIndep H) := by
…

    Mentions: OAI.SidorenkoCounterexample.localSpan

  6. theorem OAI.SidorenkoCounterexample.span_inequality line 114

    Source documentation

    Exact non-strict span inequality of the manuscript.

    theorem span_inequality (s : Finset (Finset P)) (H : Finset P → Submodule K V)
    (hs : ∀ e ∈ s, e.card = 2) :
    2 * finrank K (s.sup H : Submodule K V) ≤ ∑ i, finrank K (localSpan s H i) :=
…

    Mentions: OAI.SidorenkoCounterexample.localSpan

  7. theorem OAI.SidorenkoCounterexample.strict_span_inequality line 121

    Source documentation

    Exact strict improvement for a nondirect family, including partial intersections. Zero spaces do not affect SupIndep.

    theorem strict_span_inequality (s : Finset (Finset P)) (H : Finset P → Submodule K V)
    (hs : ∀ e ∈ s, e.card = 2) (hn : ¬s.SupIndep H) :
    2 * finrank K (s.sup H : Submodule K V) + 1 ≤ ∑ i, finrank K (localSpan s H i) := by
…

    Mentions: OAI.SidorenkoCounterexample.localSpan

  8. theorem OAI.SidorenkoCounterexample.finrank_finset_sup_le line 136
  9. theorem OAI.SidorenkoCounterexample.finrank_finite_iSup_le line 145
  10. theorem OAI.SidorenkoCounterexample.finrank_finset_sup_direct line 150
  11. def OAI.SidorenkoCounterexample.incidentPairs line 164
  12. def OAI.SidorenkoCounterexample.pairRelated line 165
  13. instance OAI.SidorenkoCounterexample.(instance at line 166) line 166
  14. theorem OAI.SidorenkoCounterexample.pairRelated_symm line 167
  15. theorem OAI.SidorenkoCounterexample.incidentPairs_card line 169
  16. theorem OAI.SidorenkoCounterexample.incidentPairs_card_le line 170
  17. theorem OAI.SidorenkoCounterexample.pair_shared_card line 171
  18. theorem OAI.SidorenkoCounterexample.incident_pair_card line 173
  19. theorem OAI.SidorenkoCounterexample.sum_incident line 177
  20. def OAI.SidorenkoCounterexample.localPairDim line 189
  21. theorem OAI.SidorenkoCounterexample.localPairDim_le line 190
  22. theorem OAI.SidorenkoCounterexample.localPairDim_le_twelve line 194
  23. def OAI.SidorenkoCounterexample.incidentSpan line 200
  24. theorem OAI.SidorenkoCounterexample.incidentSpan_le line 202
  25. theorem OAI.SidorenkoCounterexample.incidentSpan_finrank_le line 208
  26. theorem OAI.SidorenkoCounterexample.incidentSpan_finrank_direct line 213
  27. def OAI.SidorenkoCounterexample.extendPairSpace line 219
  28. theorem OAI.SidorenkoCounterexample.extendPairSpace_apply line 222
  29. theorem OAI.SidorenkoCounterexample.extend_global_span line 225
  30. theorem OAI.SidorenkoCounterexample.extend_local_span line 230
  31. theorem OAI.SidorenkoCounterexample.indexed_strict_span line 235
  32. theorem OAI.SidorenkoCounterexample.pairRelated_self line 256
  33. theorem OAI.SidorenkoCounterexample.related_label_count line 262
  34. theorem OAI.SidorenkoCounterexample.sum_local_products line 286
  35. theorem OAI.SidorenkoCounterexample.sum_local_squares line 310
  36. theorem OAI.SidorenkoCounterexample.sum_localPairDim line 328
  37. theorem OAI.SidorenkoCounterexample.residual_direct_exponent line 331
  38. theorem OAI.SidorenkoCounterexample.degree_choose_sum line 351
  39. theorem OAI.SidorenkoCounterexample.local_choose_sum_bound line 352
  40. theorem OAI.SidorenkoCounterexample.residual_nondirect_exponent line 359
  41. def OAI.SidorenkoCounterexample.pairSpaces line 390
  42. theorem OAI.SidorenkoCounterexample.pairSpaces_le line 392
  43. theorem OAI.SidorenkoCounterexample.incidentPairSpaces_le line 394
  44. theorem OAI.SidorenkoCounterexample.pairSpaces_orthogonal line 397
  45. abbrev OAI.SidorenkoCounterexample.PairDimProfile line 405
  46. abbrev OAI.SidorenkoCounterexample.DirectPairProfile line 407
  47. abbrev OAI.SidorenkoCounterexample.FamilyContainment line 409
  48. def OAI.SidorenkoCounterexample.directPairProfileCoding line 411
  49. theorem OAI.SidorenkoCounterexample.directPairProfileCoding_injective line 416
  50. def OAI.SidorenkoCounterexample.containmentExponent line 422
  51. theorem OAI.SidorenkoCounterexample.familyContainment_card_bound line 425
  52. theorem OAI.SidorenkoCounterexample.directPairProfile_card_bound line 442
  53. abbrev OAI.SidorenkoCounterexample.LocalFamilyStratum line 479
  54. abbrev OAI.SidorenkoCounterexample.PairSpanStratum line 481
  55. def OAI.SidorenkoCounterexample.pairSpanStratumCoding line 484
  56. theorem OAI.SidorenkoCounterexample.pairSpanStratumCoding_injective line 490
  57. theorem OAI.SidorenkoCounterexample.localFamilyStratum_card_bound line 497
  58. theorem OAI.SidorenkoCounterexample.familySpan_exponent_cast line 505
  59. theorem OAI.SidorenkoCounterexample.pairSpanStratum_card_bound line 509
  60. theorem OAI.SidorenkoCounterexample.residual_h_sum_le line 536
  61. theorem OAI.SidorenkoCounterexample.pairProfile_global_dim_le line 540
  62. theorem OAI.SidorenkoCounterexample.pairProfile_local_dim_le line 545
  63. abbrev OAI.SidorenkoCounterexample.ResidualDimensionBox line 548
  64. def OAI.SidorenkoCounterexample.pairProfileDimension line 549
  65. abbrev OAI.SidorenkoCounterexample.NonDirectPairProfile line 556
  66. def OAI.SidorenkoCounterexample.nondirectDimension line 558
  67. def OAI.SidorenkoCounterexample.nondirectFiberInjection line 560
  68. theorem OAI.SidorenkoCounterexample.nondirectFiberInjection_injective line 568
  69. theorem OAI.SidorenkoCounterexample.pairStratum_residual_bound line 574
  70. theorem OAI.SidorenkoCounterexample.nondirectFiber_card_bound line 596
  71. theorem OAI.SidorenkoCounterexample.nondirectPairProfile_card_bound line 635
  72. abbrev OAI.SidorenkoCounterexample.FullTailChoice line 651
  73. def OAI.SidorenkoCounterexample.fullTailConstant line 653
  74. theorem OAI.SidorenkoCounterexample.fullTailConstant_nonneg line 658
  75. def OAI.SidorenkoCounterexample.fullTailMajorant line 665
  76. theorem OAI.SidorenkoCounterexample.fullTailMajorant_nonneg line 668
  77. theorem OAI.SidorenkoCounterexample.fullTailMajorant_eq line 673
  78. theorem OAI.SidorenkoCounterexample.tripleFaceDensity_tail_bound line 699