OAI/NumberTheory/Ostmann/Construction/OriginalPrimeCellExpectation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.BulkIntegrand.averages_originalPrimeCells line 11
2. theorem OAI.Ostmann.BulkIntegrand.originalPrimeCells_mean line 37

   Source documentation

   Replacing any selected bulk coordinates by their original cell mixtures preserves the full original product expectation, including all other roles.

   theorem BulkIntegrand.originalPrimeCells_mean {σ C : Type*} [Fintype σ] [Fintype C]
       (f : BulkIntegrand σ) (P : Finset ℕ) (q : σ → ℕ) (a : σ → C → ℕ)
       (u v : σ → C → ℝ)
       (hSP : ∀ i, primeCellSupport (q i) (a i) (u i) (v i) ⊆ P)
       (hsep : ∀ i c d, c ≠ d →
         ¬Nat.ModEq (q i) (a i c) (a i d) ∨ v i c ≤ u i d ∨ v i d ≤ u i c)
       (hS : ∀ i, (∑ p ∈ primeCellSupport (q i) (a i) (u i) (v i), (p : ℝ)⁻¹) ≠ 0)
       (l : List σ) :
       let S := fun i => primeCellSupport (q i) (a i) (u i) (v i)
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeCellSupport

3. theorem OAI.Ostmann.originalPrimePrior_mean_comparison line 57

   Source documentation

   A pointwise joint replacement estimate survives the original normalized prime expectation with its error unchanged.

   theorem originalPrimePrior_mean_comparison {σ : Type*} [Fintype σ]
       (P : Finset ℕ) (Q : σ → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
       (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
       (F G : (σ → P) → ℂ) (ε : ℝ) (herr : ∀ x, ‖F x - G x‖ ≤ ε) :
       ‖(∑ x : σ → P, ((∏ i, primeSubsetPrior P (Q i) (x i) : ℝ) : ℂ) * F x) -
         ∑ x : σ → P, ((∏ i, primeSubsetPrior P (Q i) (x i) : ℝ) : ℂ) * G x‖ ≤ ε := by
   …

   Mentions: OAI.Ostmann.primeSubsetPrior

4. theorem OAI.Ostmann.BulkIntegrand.originalPrimeCells_mean_comparison line 82

   Source documentation

   The joint cell comparison can be integrated against the original product law without introducing another normalization or a count of prime samples.

   theorem BulkIntegrand.originalPrimeCells_mean_comparison {σ C : Type*}
       [Fintype σ] [Fintype C] (f : BulkIntegrand σ) (P : Finset ℕ)
       (q : σ → ℕ) (a : σ → C → ℕ) (u v : σ → C → ℝ)
       (hSP : ∀ i, primeCellSupport (q i) (a i) (u i) (v i) ⊆ P)
       (hsep : ∀ i c d, c ≠ d →
         ¬Nat.ModEq (q i) (a i c) (a i d) ∨ v i c ≤ u i d ∨ v i d ≤ u i c)
       (hS : ∀ i, (∑ p ∈ primeCellSupport (q i) (a i) (u i) (v i), (p : ℝ)⁻¹) ≠ 0)
       (l : List σ) (ν : σ → Measure ℝ) [∀ i, IsFiniteMeasure (ν i)] (ε : ℝ)
       (herr : ∀ x, ‖f.averages (fun i => bulkCellMixture
           (∑ p ∈ primeCellSupport (q i) (a i) (u i) (v i), (p : ℝ)⁻¹)⁻¹
           (fun c => primeLogCellMeasure (q i) (a i c) (u i c) (v i c))) l x -
         f.averages ν l x‖ ≤ ε) :
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeCellSupport, OAI.Ostmann.bulkCellMixture, OAI.Ostmann.primeLogCellMeasure