OAI/NumberTheory/Ostmann/Construction/PrimeExternalAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeExternalAverage line 11
2. def OAI.Ostmann.leftPrimeDensity line 18
3. theorem OAI.Ostmann.leftPrimeDensity_nonneg line 22
4. theorem OAI.Ostmann.leftPrimeDensity_le_one line 26
5. theorem OAI.Ostmann.leftPrimeDensity_norm_le_one line 32
6. theorem OAI.Ostmann.complexPrimeInterval_as_integer line 36
7. theorem OAI.Ostmann.primeExternalAverage_as_mixed line 62
8. theorem OAI.Ostmann.primeExternalAverage_bounded_statistic_cauchy line 84

   Source documentation

   The same bulk symmetrization applies to two genuine prime giants. Only one explicit scalar is lost when passing to the integer comparison law.

   theorem primeExternalAverage_bounded_statistic_cauchy {B A : Type*} [Fintype B] [Fintype A]
       (n m : ℕ) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (ν : B → A → ℝ) (hν : ∀ b a, 0 ≤ ν b a)
       (hidentical : ∀ j k, ν (slot j) = ν (slot k))
       (N : ℕ) (u v r w center : ℝ)
       (F H P : ℤ → (B → A) → ℝ → ℝ → ℂ)
       (hH : ∀ e s y x z, H s (selectedBulkSample slot e y) x z = H s y x z)
       (hP : ∀ e s y x z, P s (selectedBulkSample slot e y) x z = P s y x z)
       (hPnorm : ∀ s y x z, ‖P s y x z‖ ≤ 1)
       (W : ℝ → ℝ → ℝ) (hW : ∀ x z, 0 ≤ W x z) :
       ‖primeExternalAverage ν N u v r w
         (fun s y x z => ((P s y x z * H s y x z) * F s y x z) * W x z)‖ ^ 2 ≤
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.selectedBulkSample, OAI.Ostmann.primeExternalAverage