OAI/NumberTheory/Ostmann/Construction/FrozenOriginalBulk.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkLogValues_base_update line 11
2. theorem OAI.Ostmann.bulkLogValues_prime_update line 20
3. theorem OAI.Ostmann.frozen_original_bulk_mean line 33

   Source documentation

   The full original mean is unchanged by bulk resampling even when the real kernel is built from the original nonbulk sample. This is the form needed for the sharp moving-history kernels.

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

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

4. theorem OAI.Ostmann.frozen_original_bulk_value line 47