structure AnalyticNumberTheory.LargeSieve.ProductionConductorBlockGeometry (N Q C : ℕ) : Type

Purely finite block geometry. cell i is a conductor block with lower endpoint i.

• index : Finset ℕ
• cell : ℕ → Finset ℕ
• lower_pos (i : ℕ) : i ∈ self.index → 0 < i
• levels (i : ℕ) : i ∈ self.index → ∀ d ∈ self.cell i, i ≤ d
• pairwise : (↑self.index).PairwiseDisjoint self.cell
• cover : self.index.biUnion self.cell = highConductorSet N Q C
• inv_lower_sum_le : ∑ i ∈ self.index, (↑i)⁻¹ ≤ 2 / ↑(logConductorThreshold N C)
• lower_sum_le : ∑ i ∈ self.index, ↑i ≤ 2 * ↑Q

noncomputable def AnalyticNumberTheory.LargeSieve.productionConductorBlockGeometry (N Q C : ℕ) (hR : 0 < logConductorThreshold N C) : ProductionConductorBlockGeometry N Q C

Canonical production dyadic conductor geometry. Its cells are R*2^j < d ≤ min (2*R*2^j) Q, intersected with the production high-conductor set.

Equations

• AnalyticNumberTheory.LargeSieve.productionConductorBlockGeometry N Q C hR = { index := AnalyticNumberTheory.LargeSieve.dyadicLowers✝ (AnalyticNumberTheory.LargeSieve.logConductorThreshold N C) Q, cell := AnalyticNumberTheory.LargeSieve.dyadicCell✝ N Q C, lower_pos := ⋯, levels := ⋯, pairwise := ⋯, cover := ⋯, inv_lower_sum_le := ⋯, lower_sum_le := ⋯ }

theorem AnalyticNumberTheory.LargeSieve.productionConductorBlockGeometry_cell_subset_Ioc (N Q C : ℕ) (hR : 0 < logConductorThreshold N C) (i : ℕ) : (productionConductorBlockGeometry N Q C hR).cell i ⊆ Finset.Ioc i (2 * i)

Every cell of the canonical production geometry lies in its literal dyadic conductor interval. This is a property of the concrete canonical construction, not an additional premise of ProductionConductorBlockGeometry.

theorem AnalyticNumberTheory.LargeSieve.productionConductorBlockGeometry_index_card_le_log2 (N Q C : ℕ) (hR : 0 < logConductorThreshold N C) (hQ : Q ≤ N) : (productionConductorBlockGeometry N Q C hR).index.card ≤ N.log2 + 1

The concrete dyadic conductor geometry has at most one index per binary scale up to N.