PrimeProductNormTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Taking the even root of the finite prime-product moment bound

theorem OAI.Ostmann.prime_product_family_norm_transfer line 13

Source documentation

This finite inequality keeps the square and nonsquare contributions separate, so their numerical estimates can be supplied independently.

theorem prime_product_family_norm_transfer (hB : PublishedBonamiBound)
    {I : Type*} [Fintype I] (P S R : Finset ℕ)
    (hS : ∀ s ∈ S, Squarefree s) (hR : ∀ s ∈ S, s.primeFactors ⊆ R)
    (hP : ∀ p ∈ P, p.Prime) (hodd : ∀ p ∈ P, Odd p)
    (U Z k l : ℕ) (hU : ∀ s ∈ S, s ≤ U) (hZ : ∀ p ∈ P, p ≤ Z)
    (hl : 0 < l) (hk : 1 ≤ k) (hsize : 2 * k ^ 2 ≤ P.card)
    (b : I → S → ℂ) (pick : ℕ → I) (E A B δ : ℝ)
    (hE : 0 ≤ E) (hB0 : 0 ≤ B) (hδ : 0 ≤ δ)
    (henergy : ∀ i, (∑ s : S, ((2 * l - 1 : ℕ) : ℝ) ^ s.val.primeFactors.card * ‖b i s‖ ^ 2) ≤ E)
    (hmass : ∀ i, (∑ s : S, ‖b i s‖) ≤ A)
    (hsquare : (2 * (k.factorial : ℝ) / (P.card : ℝ) ^ k) *
      ((Fintype.card I : ℝ) * (2 : ℝ) ^ (2 * l)) * ((Z ^ k + 1 : ℕ) : ℝ) ≤ B ^ (2 * l))
…

Mentions: OAI.Ostmann.PublishedBonamiBound