Selection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.finite_greedy_packing line 16

Source documentation

Finite greedy packing, with the precise loss supplied by forbidden neighbors.

theorem finite_greedy_packing {α : Type*} [DecidableEq α] (bad : α → α → Prop)
    [DecidableRel bad] (symm : ∀ a b, bad a b → bad b a)
    (refl : ∀ a, bad a a) (S : Finset α) (D : ℕ)
    (bound : ∀ a ∈ S, (S.filter (bad a)).card ≤ D) :
    ∃ N ⊆ S, (N : Set α).Pairwise (fun a b => ¬bad a b) ∧ S.card ≤ D*N.card := by
…

theorem OAI.FiniteFactor.forbidden_frequency_card line 49

Source documentation

A fixed nonzero second frequency excludes at most 2R+1 integers.

theorem forbidden_frequency_card (S : Finset ℤ) (v v' n : ℤ) (R : ℕ) (hv' : v' ≠ 0) :
    (S.filter (fun n' => |v*n+v'*n'| ≤ (R : ℤ))).card ≤ 2*R+1 := by
…

def OAI.FiniteFactor.SamplingConflict line 62
Source documentation
Failure of the full symmetric bounded-frequency separation condition.
```
def SamplingConflict (H R : ℕ) (n n' : ℤ) : Prop :=
…
```
instance OAI.FiniteFactor.(instance at line 67) line 67
theorem OAI.FiniteFactor.samplingConflict_symm line 71
theorem OAI.FiniteFactor.samplingConflict_refl line 76
theorem OAI.FiniteFactor.samplingConflict_card line 84
Source documentation
Total forbidden-neighbor count, with no unspecified asymptotic constant.
```
theorem samplingConflict_card (H R : ℕ) (S : Finset ℤ) (n : ℤ) (hn : (R : ℤ) < n) :
    (S.filter (SamplingConflict H R n)).card ≤ (2*H+1)^2*(2*R+1) := by
…
```
Mentions: OAI.FiniteFactor.SamplingConflict

theorem OAI.FiniteFactor.exists_sampling_separated line 121

Source documentation

Deterministic selection from any positive integer interval above R.

theorem exists_sampling_separated (H R : ℕ) (hH : 1 ≤ H) (S : Finset ℤ)
    (hS : ∀ n ∈ S, (R : ℤ) < n) :
    ∃ N ⊆ S, (N : Set ℤ).Pairwise (fun n n' => ¬SamplingConflict H R n n') ∧
      S.card ≤ ((2*H+1)^2*(2*R+1))*N.card :=
…

Mentions: OAI.FiniteFactor.SamplingConflict