OAI/NumberTheory/Ostmann/Arithmetic/PrimeIntegerTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_prior_integer_extension line 12
2. theorem OAI.Ostmann.prime_integer_transfer_bound line 35

   Source documentation

   This is the finite version of the prime-to-integer extension in equation (53), using the original reciprocal-prime prior exactly.

   theorem prime_integer_transfer_bound (S T : Finset ℕ) (hST : S ⊆ T)
       (w : ℝ → ℝ) (Z u : ℝ) (hZ : 0 ≤ Z) (hu : 0 ≤ u)
       (hpos : ∀ p ∈ S, p ≠ 0) (hw : ∀ n ∈ T, 0 ≤ w (Real.log n))
       (hmass : (∑ p : S, primeSamplePrior S w Z p) = 1)
       {A : S → Type*} [∀ p, Fintype (A p)]
       (row coefficient : ∀ p, A p → ℂ)
       (hrow : ∀ p : S, (∑ a, ‖row p a‖ ^ 2) ≤ ((p : ℕ) : ℝ) * u)
       (F : ℕ → ℝ) (hF : ∀ n ∈ T, 0 ≤ F n)
       (hcoeff : ∀ p : S, (∑ a, ‖coefficient p a‖ ^ 2) ≤ F p) :
       ‖∑ p : S, (primeSamplePrior S w Z p : ℂ) * ∑ a, row p a * coefficient p a‖ ^ 2 ≤
         Z * ∑ n ∈ T, w (Real.log n) * u * F n := by
   …

   Mentions: OAI.Ostmann.primeSamplePrior