OAI/NumberTheory/Ostmann/Arithmetic/MovingSeparatedAverages.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingFrequencyPageAverage line 12
2. def OAI.Ostmann.movingSpectatorHaarAverage line 23
3. theorem OAI.Ostmann.movingArithmeticPageFactor_averages line 29
4. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_page_factorization line 76
5. theorem OAI.Ostmann.movingSeparatedPairResidueCoefficient_square_error line 89

   Source documentation

   Remove all prime-square exclusions from the literal corrected average. The frequency/Page factor and each spectator factor are retained exactly.

   theorem movingSeparatedPairResidueCoefficient_square_error
       (tier : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (hlevels : ∀ side, (T side).Levels tier)
       (hfmod : ∀ p : P, ∀ side, (T side).Frequencies (fun s => (s : ZMod p.val) ≠ 0))
       (y B : ℝ)
       (hweight : ‖movingFrequencyPageAverage value outside F E T nodes R r input Q y *
           (∏ i : S, movingSpectatorHaarAverage value (q i.val) (g i.val)
             (fun side => D side i.val) T)‖ *
         (∏ p : P, movingInternalLineProbability value T p.val) ≤ B) :
       ‖correctedMixedPairAverage input Q (∏ b, movingArithmeticModuli r q P S b)
           (movingSeparatedPairResidueCoefficient q value outside F E g D S T nodes R) y -
   …

   Mentions: OAI.Ostmann.movingFrequencyPageAverage, OAI.Ostmann.movingSpectatorHaarAverage, OAI.Ostmann.movingInternalLineProbability, OAI.Ostmann.correctedMixedPairAverage, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingSeparatedPairResidueCoefficient