OAI/Combinatorics/InfiniteMatroid/SparsePerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InfiniteMatroidCounterexample.exists_strictMono_choice line 10
2. lemma OAI.InfiniteMatroidCounterexample.block_card_atTop line 26
3. lemma OAI.InfiniteMatroidCounterexample.exists_small_spikes line 32

   Source documentation

   A sparse collection of finite block selections with prescribed lower spikes.

   lemma exists_small_spikes {G : Set E0} {δ : ℝ} (_hδ : 0 < δ)
       (hG : ∀ N, ∃ m, N ≤ m ∧ δ ≤ density G m)
       (b : ℕ → ℝ) (hbpos : ∀ j, 0 < b j) (hble : ∀ j, b j ≤ δ)
       (hbzero : Tendsto b atTop (𝓝 0)) (N : ℕ → ℕ) :
       ∃ P : Set E0, P ⊆ G ∧ Small P ∧ ∀ j, ∃ m, N j ≤ m ∧ b j ≤ density P m := by
   …

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

4. lemma OAI.InfiniteMatroidCounterexample.strictMono_intervals line 104
5. lemma OAI.InfiniteMatroidCounterexample.spike_probe_bound line 113
6. lemma OAI.InfiniteMatroidCounterexample.positive_pool_add line 134