OAI/NumberTheory/Ostmann/Construction/PrimeExternalLogCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeExternalAverage_congr_primes line 11
2. theorem OAI.Ostmann.primeExternalAverage_log_cutoff line 37
3. theorem OAI.Ostmann.smoothGiantExternalAverage_log_cutoff line 55

   Source documentation

   This is the normalized original giant law written with the same positive-log outer factors as the moving statistic.

   theorem smoothGiantExternalAverage_log_cutoff {B A : Type*} [Fintype B] [Fintype A]
       (ν : B → A → ℝ) (N : ℕ) (φ : ℝ → ℝ) (G H : ℝ)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0)
       (F : ℤ → (B → A) → ℝ → ℝ → ℂ) :
       smoothGiantExternalAverage ν N φ G H
         (fun s y p q => F s y (Real.log p) (Real.log q)) =
         (Real.exp (smoothGiantLogNormalizer (smoothGiantPrimeRange G) φ G +
           smoothGiantLogNormalizer (smoothGiantPrimeRange H) φ H) : ℂ) *
         primeExternalAverage ν N (G - 1) (G + 1) (H - 1) (H + 1) (fun s y x z =>
           (positiveLogCutoff φ G ⌊Real.exp x⌋₊ : ℂ) *
             (positiveLogCutoff φ H ⌊Real.exp z⌋₊ : ℂ) *
               F s y (Real.log ⌊Real.exp x⌋₊) (Real.log ⌊Real.exp z⌋₊)) := by
   …

   Mentions: OAI.Ostmann.smoothGiantExternalAverage, OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.primeExternalAverage, OAI.Ostmann.positiveLogCutoff