MovingPatternMixedPrimeNormBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The norm estimate for the literal mixed-giant prime mean

theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_original_mixed_prime_norm_bound line 47

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_mixed_prime_norm_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)
    (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