OAI/NumberTheory/Ostmann/Construction/SmoothGiantExternalAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.smoothGiantPrior_pair_interval line 10
2. def OAI.Ostmann.smoothGiantExternalAverage line 41
3. theorem OAI.Ostmann.smoothGiantExternalAverage_eq line 49
4. theorem OAI.Ostmann.smoothGiantExternalAverage_full_cell_bound line 69

   Source documentation

   The unit-rectangle bounds apply to the original normalized giant law with the exact two normalizers and the fixed four-rectangle cost.

   theorem smoothGiantExternalAverage_full_cell_bound {B A : Type*} [Fintype B] [Fintype A]
       (ν : B → A → ℝ) (N : ℕ) (φ : ℝ → ℝ) (G H E : ℝ)
       (hout : ∀ x, 1 ≤ |x| → φ x = 0) (F : ℤ → (B → A) → ℕ → ℕ → ℂ)
       (h : ∀ i j : Bool, ‖primeExternalAverage ν N
         (if i then G else G - 1) ((if i then G else G - 1) + 1)
         (if j then H else H - 1) ((if j then H else H - 1) + 1)
         (fun s y x z => (φ (x - G) : ℂ) * (φ (z - H) : ℂ) *
           F s y ⌊Real.exp x⌋₊ ⌊Real.exp z⌋₊)‖ ^ 2 ≤ E) :
       ‖smoothGiantExternalAverage ν N φ G H F‖ ^ 2 ≤
         16 * Real.exp (2 * (smoothGiantLogNormalizer (smoothGiantPrimeRange G) φ G +
           smoothGiantLogNormalizer (smoothGiantPrimeRange H) φ H)) * E := by
   …

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