theorem G12SafeGridBudget.absorb_constant (C : ℝ) (B : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, C * (↑N / Real.log ↑N ^ (B + 1)) ≤ ↑N / Real.log ↑N ^ B

theorem G12SafeGridBudget.fixed_prefix_log {e : ℝ} (he : 0 < e) : ∀ᶠ (N : ℕ) in Filter.atTop, 1 ≤ Real.log ↑N ∧ ∀ (x : ℝ), e * ↑N ≤ x → Real.log ↑N / 2 ≤ Real.log x

theorem G12SafeGridBudget.scaled_discrepancy (A : ℕ) {n x : ℝ} (hn : 0 ≤ n) (hl : 0 < Real.log n) (hx : x ≤ 4 * n) (hxl : Real.log n / 2 ≤ Real.log x) : x / Real.log x ^ A ≤ 4 * 2 ^ A * (n / Real.log n ^ A)

theorem G12SafeGridBudget.small_numerical (B : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ Q ≤ ↑N, 8000 * ↑⌈√Q⌉₊ ≤ 16000 * (↑N / Real.log ↑N ^ B)

theorem G12SafeGridBudget.indices_card_log {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} (hl : 1 ≤ Real.log ↑N) : ↑(G12FineGrid.indices ρ N).card ≤ (1 / Real.log ρ + 2) ^ 2 * Real.log ↑N ^ 2

The literal production index set, including repeated and empty endpoint cells.