OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternPrimeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_original_prime_bound line 46

   Source documentation

   The original Page/spectator kernel now has a signed bound under its literal deleted prime prior. Its frequency and pointwise spectator bounds are derived; the remaining local signed mean is exactly the quartet input.

   theorem PublishedProgressionInput.movingPattern_original_prime_bound
       [NeZero (∏ i, bulkResidueModuli r p i)]
       (r₀ : ℕ) (hsmallLen : ∀ b, MovingLeafLengthLE n (small b) r₀)
       (hy : 0 ≤ y) (hQ : 2 ≤ Q) (hMQ : (∏ i, bulkResidueModuli r p i) ≤ Q)
       (hpage : pageAtModulus (∏ i, bulkResidueModuli r p i) (selectedPageZero P Q) =
         pageAtModulus r (selectedPageZero P 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)
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.MovingLeafLengthLE, OAI.Ostmann.pageAtModulus, OAI.Ostmann.selectedPageZero, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeLogCellSet