OAI/NumberTheory/Ostmann/Construction/OriginalHarmonicPair.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeSubsetPrior_restrict_sum line 12
2. theorem OAI.Ostmann.twoCoordinateAssignment_map line 17
3. theorem OAI.Ostmann.original_harmonic_pair_bound line 29

   Source documentation

   A uniform long/short-prime estimate is inserted in the complete original expectation. The remaining coordinates retain their individual role priors.

   theorem original_harmonic_pair_bound {V : Type*} [Fintype V]
       (a b : V) (hab : a ≠ b) (P : Finset ℕ) (Q : V → Finset ℕ)
       (hQP : ∀ v, Q v ⊆ P) (hQmass : ∀ v, (∑ q ∈ Q v, (q : ℝ)⁻¹) ≠ 0)
       (F : (V → ℕ) → ℂ) (δ : ℝ) (hδ : 0 ≤ δ)
       (hsection : ∀ outside : OtherVertices a b → P,
         ‖∑ p : Q b, (primeSubsetPrior (Q b) (Q b) p : ℂ) *
           ∑ q : Q a, (primeSubsetPrior (Q a) (Q a) q : ℂ) *
             F (twoCoordinateAssignment a b hab (fun v => (outside v : ℕ)) (q : ℕ) (p : ℕ))‖ ≤ δ) :
       ‖∑ x : V → P, ((∏ v, primeSubsetPrior P (Q v) (x v) : ℝ) : ℂ) *
         F (fun v => (x v : ℕ))‖ ≤ δ := by
   …

   Mentions: OAI.Ostmann.OtherVertices, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.twoCoordinateAssignment