OAI/NumberTheory/Ostmann/Construction/RoundedCellTargets.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.nat_lattice_rounddown line 9
2. theorem OAI.Ostmann.dense_cell_approximate_sum line 25

   Source documentation

   An interior real target can be realized to bounded accuracy. The error bound depends only on the density of good cells, not on their scale.

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

   Mentions: OAI.Ostmann.cellDifferences