OAI/NumberTheory/Ostmann/Construction/PrimeSubsetCellMixture.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.primeSubsetLogMeasure_cells line 12
2. theorem OAI.Ostmann.BulkIntegrand.average_originalPrimeCells line 25

   Source documentation

   The original normalized subset prior equals the mixture of its complete log/residue cells, with the same single normalization constant.

   theorem BulkIntegrand.average_originalPrimeCells {σ C : Type*} [Fintype σ] [Fintype C]
       (f : BulkIntegrand σ) (P : Finset ℕ) (q : ℕ) (a : C → ℕ) (u v : C → ℝ)
       (hSP : primeCellSupport q a u v ⊆ P)
       (hsep : ∀ c d, c ≠ d → ¬Nat.ModEq q (a c) (a d) ∨ v c ≤ u d ∨ v d ≤ u c)
       (i : σ) (x : σ → ℝ) :
       let S := primeCellSupport q a u v
   …

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