OAI/NumberTheory/Ostmann/Supply/RestrictedSubsetEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.centeredSubsetEnergy_embedding line 11
2. theorem OAI.Ostmann.lowMode_energy_embedding line 27
3. theorem OAI.Ostmann.restricted_lowMode_energy_budget line 49

   Source documentation

   The sparse tensor uses only its selected prime coordinates. Its low-mode energy is bounded by the sieve on the full prime family, with no factor for the number of unused coordinates.

   theorem restricted_lowMode_energy_budget (ls : PublishedAdditiveLargeSieve)
       {n m 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)
       (e : Fin m ↪ Fin n) (K : ℕ)
       (hprod : ∀ T : Finset (Fin m), T.card ≤ K → (∏ i ∈ T, p (e i)) ≤ Q)
   …

   Mentions: OAI.Ostmann.PublishedAdditiveLargeSieve