OAI/NumberTheory/Ostmann/Arithmetic/MovingSeparatedCRT.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_crt line 31

   Source documentation

   Pointwise CRT identification, using the actual frequency recursion and all actual internal occurrences, before any norm or average is taken.

   theorem movingSeparatedPairResidueCoefficient_crt
       (z : ZMod (∏ b, movingArithmeticModuli r q P S b) ×
         (ZMod (∏ b, movingArithmeticModuli r q P S b))ˣ) :
       movingSeparatedPairResidueCoefficient q value outside F E g D S T nodes R
         z.1.val (z.2 : ZMod (∏ b, movingArithmeticModuli r q P S b)).val =
       ∏ b, movingArithmeticLocalFactor q value outside F E g D T nodes R r P S b
         (crtExternalPairEquiv (movingArithmeticModuli r q P S) hc z b) := by
   …

   Mentions: OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingSeparatedPairResidueCoefficient, OAI.Ostmann.movingArithmeticLocalFactor, OAI.Ostmann.crtExternalPairEquiv

2. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_average line 87

   Source documentation

   The Haar average of the original coefficient equals the product of its frequency, internal-square and spectator averages.

   theorem movingSeparatedPairResidueCoefficient_average
       [∀ b, NeZero (movingArithmeticModuli r q P S b)] :
       (Fintype.card (ZMod (∏ b, movingArithmeticModuli r q P S b) ×
         (ZMod (∏ b, movingArithmeticModuli r q P S b))ˣ) : ℂ)⁻¹ *
         (∑ z : ZMod (∏ b, movingArithmeticModuli r q P S b) ×
           (ZMod (∏ b, movingArithmeticModuli r q P S b))ˣ, movingSeparatedPairResidueCoefficient q value outside F E g D S T nodes R
           z.1.val (z.2 : ZMod (∏ b, movingArithmeticModuli r q P S b)).val) =
       ∏ b, (Fintype.card (ZMod (movingArithmeticModuli r q P S b) ×
         (ZMod (movingArithmeticModuli r q P S b))ˣ) : ℂ)⁻¹ *
         ∑ z, movingArithmeticLocalFactor q value outside F E g D T nodes R r P S b z := by
   …

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