OAI/NumberTheory/Ostmann/Construction/PrimeExternalPartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.complexPrimeInterval_function_add line 10
2. theorem OAI.Ostmann.primeExternalAverage_left_add line 19
3. theorem OAI.Ostmann.primeExternalAverage_right_add line 37
4. theorem OAI.Ostmann.primeExternalAverage_four_cells line 51
5. theorem OAI.Ostmann.four_complex_terms_square_le line 66
6. theorem OAI.Ostmann.primeExternalAverage_full_cell_bound line 80

   Source documentation

   The complete pair of width-two cells loses only the fixed factor sixteen in the squared bound. No boundary primes are removed.

   theorem primeExternalAverage_full_cell_bound {B A : Type*} [Fintype B] [Fintype A]
       (ν : B → A → ℝ) (N : ℕ) (G H E : ℝ)
       (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) F‖ ^ 2 ≤ E) :
       ‖primeExternalAverage ν N (G - 1) (G + 1) (H - 1) (H + 1) F‖ ^ 2 ≤ 16 * E := by
   …

   Mentions: OAI.Ostmann.primeExternalAverage