OAI/Combinatorics/InfiniteMatroid/Columns.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.InfiniteMatroidCounterexample.ColumnTag line 12
2. def OAI.InfiniteMatroidCounterexample.columnString line 14
3. lemma OAI.InfiniteMatroidCounterexample.columnString_injective line 17
4. def OAI.InfiniteMatroidCounterexample.prefixString line 32
5. lemma OAI.InfiniteMatroidCounterexample.eventually_prefix_injective line 34
6. def OAI.InfiniteMatroidCounterexample.column line 48
7. def OAI.InfiniteMatroidCounterexample.dDensity line 50
8. def OAI.InfiniteMatroidCounterexample.DSmall line 52
9. lemma OAI.InfiniteMatroidCounterexample.dBlock_trace_card line 54
10. lemma OAI.InfiniteMatroidCounterexample.dDensity_formula line 74
11. lemma OAI.InfiniteMatroidCounterexample.columns_uniform line 82

    Source documentation

    All finite marginals are uniform once the chosen prefixes separate.

    lemma columns_uniform {A : Type} [Fintype A] [DecidableEq A] (e : A ↪ ColumnTag)
        (P : (A → Bool) → Prop) :
        ∀ᶠ m in atTop,
          dDensity {x : D | P (fun a ↦ x.2 (prefixString (columnString (e a)) x.1))} m =
            (Nat.card {v : A → Bool // P v} : ℝ) /
              Fintype.card (A → Bool) := by
    …

    Mentions: OAI.InfiniteMatroidCounterexample.ColumnTag, OAI.InfiniteMatroidCounterexample.dDensity, OAI.InfiniteMatroidCounterexample.D, OAI.InfiniteMatroidCounterexample.prefixString, OAI.InfiniteMatroidCounterexample.columnString

12. lemma OAI.InfiniteMatroidCounterexample.columns_pattern line 95
13. lemma OAI.InfiniteMatroidCounterexample.dSmall_empty line 107
14. lemma OAI.InfiniteMatroidCounterexample.dSmall_mono line 112
15. lemma OAI.InfiniteMatroidCounterexample.dSmall_union line 115
16. lemma OAI.InfiniteMatroidCounterexample.dSmall_false_of_eventual line 119
17. lemma OAI.InfiniteMatroidCounterexample.pattern_positive line 125