OriginalBulkExpectation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The iterated logarithmic integrals are the original product-prior means

def OAI.Ostmann.primeArrayLogs line 12
theorem OAI.Ostmann.primeArrayLogs_update line 15
theorem OAI.Ostmann.BulkIntegrand.averages_originalPrimePriors line 22

theorem OAI.Ostmann.BulkIntegrand.averages_all_originalPrimePriors line 40

Source documentation

With every original bulk coordinate present, the log integral is exactly the finite product expectation used by the scheduled amplitude.

theorem BulkIntegrand.averages_all_originalPrimePriors {σ : Type*} [Fintype σ]
    (f : BulkIntegrand σ) (P : Finset ℕ) (Q : σ → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
    (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
    (l : List σ) (hl : ∀ i, i ∈ l) (x : σ → P) :
    f.averages (fun i => primeSubsetLogMeasure (Q i) (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹)
      l (primeArrayLogs x) =
      ∑ y : σ → P, ((∏ i, primeSubsetPrior P (Q i) (y i) : ℝ) : ℂ) * f (primeArrayLogs y) := by
…

Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeSubsetLogMeasure, OAI.Ostmann.primeArrayLogs, OAI.Ostmann.primeSubsetPrior