OAI/NumberTheory/Ostmann/Arithmetic/BulkResidueMixtures.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_residue_mixture_integral line 14

   Source documentation

   Sum the residue classes before estimating. The common original normalization stays outside the sum, and the cell boxes are counted once.

   theorem bulk_residue_mixture_integral {J C R : Type*}
       [Fintype J] [Fintype C] [Fintype R]
       (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
       (μ : R → J → C → Measure ℝ) [∀ z j c, IsFiniteMeasure (μ z j c)]
       (f : R → BulkIntegrand J) :
       (∑ z, ∫ y, f z y ∂Measure.pi (fun j => bulkCellMixture (Z j) (μ z j))) =
         ((∏ j, Z j : ℝ) : ℂ) * ∑ c : J → C, ∑ z,
           ∫ y, f z y ∂Measure.pi (fun j => μ z j (c j)) := by
   …

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