MovingPrimePageCRT.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Both giant prime coordinates in the exact arithmetic CRT average

theorem OAI.Ostmann.crtUnitPairEquiv_to_external line 12

Source documentation

Restricting the first external CRT coordinate to a unit gives the original two-prime CRT coordinates.

theorem crtUnitPairEquiv_to_external {B : Type*} [Fintype B] (a : B → ℕ)
    (hc : Pairwise (fun i j => (a i).Coprime (a j)))
    (z : (ZMod (∏ i, a i))ˣ × (ZMod (∏ i, a i))ˣ) (i : B) :
    crtExternalPairEquiv a hc ((z.1 : ZMod (∏ i, a i)), z.2) i =
      ((crtUnitPairEquiv a hc z i).1.val, (crtUnitPairEquiv a hc z i).2) := by
…

Mentions: OAI.Ostmann.crtExternalPairEquiv, OAI.Ostmann.crtUnitPairEquiv

def OAI.Ostmann.movingArithmeticPrimePageFactor line 24

Source documentation

Both Page factors stay in the frequency block; the other blocks have exactly their uniform two-unit laws.

noncomputable def movingArithmeticPrimePageFactor {I : Type*}
    (r : ℕ) (q : I → ℕ) (P : Finset ℕ) (S : Finset I)
    (input : PublishedProgressionInput) (Q : ℕ) (x y : ℝ)
    (f : ∀ b, ZMod (movingArithmeticModuli r q P S b) ×
      (ZMod (movingArithmeticModuli r q P S b))ˣ → ℂ) :
    ∀ b, (ZMod (movingArithmeticModuli r q P S b))ˣ ×
      (ZMod (movingArithmeticModuli r q P S b))ˣ → ℂ
  | .inl u, z => f (.inl u) (z.1.val, z.2) *
      pageGiantWeight input Q r (show (ZMod r)ˣ from z.1).val.val x *
      pageGiantWeight input Q r (show (ZMod r)ˣ from z.2).val.val y
  | .inr b, z => f (.inr b) (z.1.val, z.2)

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.pageGiantWeight

theorem OAI.Ostmann.movingArithmeticPrimePageFactor_product line 36

theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_prime_page_average line 77

Source documentation

The literal two-prime giant average, with both exceptional-character multipliers, factors over the same concrete arithmetic blocks.

theorem movingSeparatedPairResidueCoefficient_prime_page_average (x y : ℝ) :
    correctedPrimePairAverage input Q (∏ b, movingArithmeticModuli r q P S b)
      (movingSeparatedPairResidueCoefficient q value outside F E g D S T nodes R) x y =
    ∏ b, (Fintype.card ((ZMod (movingArithmeticModuli r q P S b))ˣ ×
      (ZMod (movingArithmeticModuli r q P S b))ˣ) : ℂ)⁻¹ *
      ∑ z, movingArithmeticPrimePageFactor r q P S input Q x y
        (movingArithmeticLocalFactor q value outside F E g D T nodes R r P S) b z := by
…

Mentions: OAI.Ostmann.correctedPrimePairAverage, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingSeparatedPairResidueCoefficient, OAI.Ostmann.movingArithmeticPrimePageFactor, OAI.Ostmann.movingArithmeticLocalFactor