OAI/NumberTheory/Ostmann/Arithmetic/MovingLogPrimeAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFrequencyPairFactor_bulk_log line 18
2. theorem OAI.Ostmann.movingFrequencyPrimeAverage_bulk_log line 34

   Source documentation

   Both Page corrections are unchanged. The original logarithmic weights are constants only with respect to the two giant residue variables.

   theorem movingFrequencyPrimeAverage_bulk_log (r : ℕ) [NeZero r]
       (P : PublishedProgressionInput) (Q : ℕ) (x y : ℝ) :
       movingFrequencyPrimeAverage value outside
         (fun b {_} T s => (movingBulkLeafLogWeight value tier k outside cb cd T : ℂ) * F b T s)
         E T nodes R r P Q x y =
       ((movingBulkTreeLogWeight value tier k outside cb cd (T false) : ℂ) *
         star (movingBulkTreeLogWeight value tier k outside cb cd (T true) : ℂ)) *
         movingFrequencyPrimeAverage value outside F E T nodes R r P Q x y := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.movingFrequencyPrimeAverage, OAI.Ostmann.movingBulkLeafLogWeight, OAI.Ostmann.movingBulkTreeLogWeight