CoefficientBins.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite bins for probability coefficients

An integer floor grid partitions the coefficient simplex into finitely many parts of arbitrarily small l1 diameter. The proof uses only the Archimedean property and finite sums, and also applies when the coefficient index is empty.

def OAI.Tingley.CoefficientSimplex line 22
Source documentation
Nonnegative coefficients with total mass one.
```
def CoefficientSimplex (n : ℕ) : Set (Fin n → ℝ) :=
…
```
theorem OAI.Tingley.coefficient_le_one line 25
theorem OAI.Tingley.abs_sub_lt_of_same_floor line 32
theorem OAI.Tingley.exists_coefficient_bins line 52
Source documentation
A finite family of coefficient bins with l1 diameter at most η.
The label type has (K + 1)^n elements. The last coordinate label retains coefficients equal to one. For n = 0, the simplex and all bins are empty; no nonemptiness hypothesis on the coefficient index is needed.
```
theorem exists_coefficient_bins (n : ℕ) (η : ℝ) (hη : 0 < η) :
    ∃ K : ℕ, ∃ bins : (Fin n → Fin (K + 1)) → Set (Fin n → ℝ),
      (∀ w ∈ CoefficientSimplex n, ∃ q, w ∈ bins q) ∧
      (∀ q, ∀ w ∈ bins q, ∀ v ∈ bins q, ∑ i, |w i - v i| ≤ η) := by
…
```
Mentions: OAI.Tingley.CoefficientSimplex