OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternTwoPrimeNormBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_original_two_prime_norm_bound line 48

   Source documentation

   Transfer a retained arithmetic absolute mean to the original prime law, with the sharp window factor in the main term and the established variation budget in the approximation errors.

   theorem PublishedProgressionInput.movingPattern_original_two_prime_norm_bound
       [NeZero (∏ i, bulkResidueModuli r p i)]
       (r₀ : ℕ) (hsmallLen : ∀ b, MovingLeafLengthLE n (small b) r₀)
       (hxg : 0 ≤ xg) (hy : 0 ≤ y) (hQ : 2 ≤ Q) (hMQ : (∏ i, bulkResidueModuli r p i) ≤ Q)
       (u v : (TreeLeafIndex n × Fin m) → Cell → ℝ)
       (hu : ∀ j c, 1 ≤ u j c) (huv : ∀ j c, u j c ≤ v j c)
       (hshort : ∀ j c, v j c ≤ u j c + 1)
       (hmassCell : ∀ j c (a : (ZMod (∏ i, bulkResidueModuli r p i))ˣ),
         ∑ q ∈ primeLogCellSet (∏ i, bulkResidueModuli r p i) a.val.val (u j c) (v j c),
           (q : ℝ)⁻¹ ≤ 2)
       (c₀ : Cell × (ZMod (∏ i, bulkResidueModuli r p i))ˣ)
       (hP : ∀ j, primeCellSupport (∏ i, bulkResidueModuli r p i)
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.MovingLeafLengthLE, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeLogCellSet, OAI.Ostmann.primeCellSupport