OAI/Combinatorics/InfiniteMatroid/BlockDensity.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InfiniteMatroidCounterexample.dBlock line 12
  2. def OAI.InfiniteMatroidCounterexample.wBlock line 15
  3. lemma OAI.InfiniteMatroidCounterexample.mem_dBlock line 17
  4. lemma OAI.InfiniteMatroidCounterexample.mem_wBlock line 28
  5. lemma OAI.InfiniteMatroidCounterexample.card_dBlock line 31
  6. lemma OAI.InfiniteMatroidCounterexample.card_wBlock line 34
  7. lemma OAI.InfiniteMatroidCounterexample.dBlock_disjoint line 37
  8. lemma OAI.InfiniteMatroidCounterexample.wBlock_disjoint line 42
  9. def OAI.InfiniteMatroidCounterexample.blockPrefix line 47
  10. lemma OAI.InfiniteMatroidCounterexample.mem_prefix line 50
  11. lemma OAI.InfiniteMatroidCounterexample.prefix_mono line 54
  12. lemma OAI.InfiniteMatroidCounterexample.card_prefix line 58
  13. lemma OAI.InfiniteMatroidCounterexample.block_growth line 62
  14. lemma OAI.InfiniteMatroidCounterexample.block_prefix_growth line 76
  15. def OAI.InfiniteMatroidCounterexample.traceFinset line 85
  16. lemma OAI.InfiniteMatroidCounterexample.mem_traceFinset line 89
  17. lemma OAI.InfiniteMatroidCounterexample.traceFinset_subset line 94
  18. lemma OAI.InfiniteMatroidCounterexample.traceFinset_mono line 98
  19. lemma OAI.InfiniteMatroidCounterexample.traceFinset_empty line 104
  20. lemma OAI.InfiniteMatroidCounterexample.traceFinset_univ line 108
  21. lemma OAI.InfiniteMatroidCounterexample.traceFinset_union line 112
  22. lemma OAI.InfiniteMatroidCounterexample.traceFinset_disjoint line 118
  23. def OAI.InfiniteMatroidCounterexample.finiteDensity line 124

    Source documentation

    Counting density inside a finite block.

    noncomputable def finiteDensity {α : Type*} (s : Finset α) (X : Set α) : ℝ :=
…
  24. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_nonneg line 127
  25. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_le_one line 132
  26. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_mono line 137
  27. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_union_le line 143
  28. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_compl line 152
  29. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_union line 165
  30. def OAI.InfiniteMatroidCounterexample.density line 171
  31. def OAI.InfiniteMatroidCounterexample.Small line 173
  32. lemma OAI.InfiniteMatroidCounterexample.small_empty line 175
  33. lemma OAI.InfiniteMatroidCounterexample.small_subset line 180
  34. lemma OAI.InfiniteMatroidCounterexample.small_union line 183
  35. lemma OAI.InfiniteMatroidCounterexample.finite_subset_prefix line 188
  36. lemma OAI.InfiniteMatroidCounterexample.small_finite line 196
  37. lemma OAI.InfiniteMatroidCounterexample.small_univ_false line 210
  38. def OAI.InfiniteMatroidCounterexample.SameClass line 220
  39. lemma OAI.InfiniteMatroidCounterexample.sameClass_refl line 222
  40. lemma OAI.InfiniteMatroidCounterexample.sameClass_symm line 225
  41. lemma OAI.InfiniteMatroidCounterexample.sameClass_trans line 228
  42. lemma OAI.InfiniteMatroidCounterexample.sameClass_interval line 231
  43. def OAI.InfiniteMatroidCounterexample.tailSup line 240
  44. def OAI.InfiniteMatroidCounterexample.tailInf line 241
  45. lemma OAI.InfiniteMatroidCounterexample.tail_nonempty line 243
  46. lemma OAI.InfiniteMatroidCounterexample.le_tailSup line 246
  47. lemma OAI.InfiniteMatroidCounterexample.tailInf_le line 250
  48. lemma OAI.InfiniteMatroidCounterexample.tailSup_le_add line 254
  49. lemma OAI.InfiniteMatroidCounterexample.tailInf_le_add line 262
  50. lemma OAI.InfiniteMatroidCounterexample.tailSup_mono line 273
  51. lemma OAI.InfiniteMatroidCounterexample.tailInf_mono line 278
  52. lemma OAI.InfiniteMatroidCounterexample.tailSup_lipschitz line 283
  53. lemma OAI.InfiniteMatroidCounterexample.tailInf_lipschitz line 299
  54. lemma OAI.InfiniteMatroidCounterexample.tailSup_neg line 315
  55. lemma OAI.InfiniteMatroidCounterexample.tailInf_neg line 323
  56. def OAI.InfiniteMatroidCounterexample.dProbe line 332

    Source documentation

    The block-density difference d_m^T(X).

    noncomputable def dProbe (T X : Set E0) (m : ℕ) : ℝ := density X m - density T m

    Mentions: OAI.InfiniteMatroidCounterexample.E0, OAI.InfiniteMatroidCounterexample.density

  57. def OAI.InfiniteMatroidCounterexample.pProbe line 335

    Source documentation

    The finite-prefix count difference p_n^T(X).

    noncomputable def pProbe (T X : Set E0) (n : ℕ) : ℝ :=
…

    Mentions: OAI.InfiniteMatroidCounterexample.E0

  58. def OAI.InfiniteMatroidCounterexample.fProbe line 338
  59. lemma OAI.InfiniteMatroidCounterexample.dProbe_bounds line 341
  60. lemma OAI.InfiniteMatroidCounterexample.dProbe_bddAbove line 349
  61. lemma OAI.InfiniteMatroidCounterexample.dProbe_bddBelow line 354
  62. lemma OAI.InfiniteMatroidCounterexample.dProbe_mono line 359
  63. lemma OAI.InfiniteMatroidCounterexample.pProbe_mono line 362
  64. lemma OAI.InfiniteMatroidCounterexample.fProbe_mono line 368
  65. lemma OAI.InfiniteMatroidCounterexample.traceFinset_insert line 375
  66. lemma OAI.InfiniteMatroidCounterexample.traceFinset_insert_of_notMem line 387
  67. lemma OAI.InfiniteMatroidCounterexample.traceFinset_of_agree line 398
  68. lemma OAI.InfiniteMatroidCounterexample.trace_card_insert_le line 404
  69. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_insert_le line 413
  70. lemma OAI.InfiniteMatroidCounterexample.fProbe_insert_le line 419
  71. lemma OAI.InfiniteMatroidCounterexample.finite_change_eventually line 467
  72. lemma OAI.InfiniteMatroidCounterexample.dProbe_compl line 501
  73. lemma OAI.InfiniteMatroidCounterexample.pProbe_compl line 507
  74. lemma OAI.InfiniteMatroidCounterexample.fProbe_compl line 517
  75. lemma OAI.InfiniteMatroidCounterexample.finiteDensity_interval line 521
  76. lemma OAI.InfiniteMatroidCounterexample.sameClass_gap line 536
  77. lemma OAI.InfiniteMatroidCounterexample.fProbe_variation line 543
  78. lemma OAI.InfiniteMatroidCounterexample.fProbe_block_continuity line 566