ConcreteSubsetEnergyBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The centered-subset budget with all extension weights discharged

theorem OAI.Ostmann.floor_product_half_bound line 10

theorem OAI.Ostmann.concrete_subset_energy_budget line 23

Source documentation

The finite form of (5.4), before specializing the logarithmic budget. Its multiplier lower bound is proved from squarefreeness, divisibility counts and Markov's inequality; it is not an additional analytic assumption.

theorem concrete_subset_energy_budget (ls : PublishedAdditiveLargeSieve)
    {n M Q : ℕ} (p : Fin n → ℕ) [∀ i, Fact (p i).Prime]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (S : ∀ i, Finset (ZMod (p i))) (hS : ∀ i, (S i).Nonempty)
    (κ : ℕ → ℝ) (hκ : ∀ q ∈ Finset.univ.image p, 0 < κ q)
    (hκS : ∀ i, κ (p i) = (p i : ℝ) / (S i).card - 1)
    (hQ : 1 ≤ Q) (hM : 1 ≤ M)
    (hcover : ∀ q, Nat.Prime q → q ≤ Q → ∃ i, p i = q)
    (A : Finset (Fin M)) (hA : A.Nonempty) (J : ℤ)
    (ha : ∀ x ∈ A, ∀ i, ((J + (x.val : ℤ) : ℤ) : ZMod (p i)) ∈ S i)
    (F : Finset (Finset (Fin n)))
    (hprod : ∀ T ∈ F, (∏ i ∈ T, p i) ≤ Q)
…

Mentions: OAI.Ostmann.PublishedAdditiveLargeSieve