OAI/NumberTheory/Ostmann/Arithmetic/MovingSeparatedPageCRT.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Retaining the Page correction in the frequency block

  1. def OAI.Ostmann.movingArithmeticPageFactor line 11
  2. theorem OAI.Ostmann.movingArithmeticPageFactor_product line 22
  3. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_page_average line 61

    Source documentation

    The original Page-weighted mixed average factors exactly. Its Page term stays in the frequency factor, with no absolute value or mean replacement.

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

    Mentions: OAI.Ostmann.correctedMixedPairAverage, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingSeparatedPairResidueCoefficient, OAI.Ostmann.movingArithmeticPageFactor, OAI.Ostmann.movingArithmeticLocalFactor