LargeCellTargets.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing the number of cell labels for a large target

The number of labels is the floor of the target divided by the midpoint of the extreme cell indices. All constants depend only on the density.

theorem OAI.Ostmann.dense_cell_large_target line 15

Source documentation

A dense set of positive cell indices realizes all sufficiently large real targets, with a number of labels comparable to target divided by scale.

theorem dense_cell_large_target (δ : ℝ) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (I : Finset ℕ) (a b : ℕ),
      a < b → a ∈ I → b ∈ I → (∀ x ∈ I, a ≤ x ∧ x ≤ b) →
      δ * b + 2 ≤ I.card → ∀ T : ℝ, C * b ≤ T →
      ∃ (n : ℕ) (w : List ℕ), w.length = n ∧ (∀ x ∈ w, x ∈ I) ∧
        |(w.sum : ℝ) - T| < δ⁻¹ ∧ (n : ℝ) * b ≤ 2 * T ∧ T < (n + 1 : ℕ) * b := by
…