OAI/NumberTheory/Ostmann/Arithmetic/BulkPrimeAtoms.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeCellAtomWeight line 12
2. theorem OAI.Ostmann.primeCellAtomWeight_nonneg line 15
3. theorem OAI.Ostmann.primeLogCellMeasure_ambient line 20
4. theorem OAI.Ostmann.BulkIntegrand.integral_prime_cell_product line 38

   Source documentation

   This equality retains each original atom and all residue restrictions; there is no replacement by an independent uniform prime sample.

   theorem BulkIntegrand.integral_prime_cell_product {J : Type*} [Fintype J]
       (f : BulkIntegrand J) (P : Finset ℕ) (q a : J → ℕ) (u v : J → ℝ)
       (hP : ∀ j, primeLogCellSet (q j) (a j) (u j) (v j) ⊆ P) :
       (∫ y, f y ∂Measure.pi (fun j => primeLogCellMeasure (q j) (a j) (u j) (v j))) =
         ∑ x : J → P, ((∏ j, primeCellAtomWeight (q j) (a j) (u j) (v j) (x j) : ℝ) : ℂ) *
           f (fun j => Real.log (x j : ℕ)) := by
   …

   Mentions: OAI.Ostmann.BulkIntegrand, OAI.Ostmann.primeLogCellSet, OAI.Ostmann.primeLogCellMeasure, OAI.Ostmann.primeCellAtomWeight