OAI/NumberTheory/Ostmann/Arithmetic/BulkProductMixtures.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulk_product_mixtures line 14

   Source documentation

   Expanding all cell mixtures counts each joint box once and keeps the original product of harmonic normalization constants.

   theorem bulk_product_mixtures {J C : Type*} [Fintype J] [Fintype C]
       (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
       (μ : J → C → Measure ℝ) [∀ j c, IsFiniteMeasure (μ j c)] :
       Measure.pi (fun j => bulkCellMixture (Z j) (μ j)) =
         ENNReal.ofReal (∏ j, Z j) • ∑ c : J → C, Measure.pi (fun j => μ j (c j)) := by
   …

   Mentions: OAI.Ostmann.bulkCellMixture

2. theorem OAI.Ostmann.BulkIntegrand.integral_product_mixtures line 28

   Source documentation

   The exact joint integral corresponding to the original normalized cell mixture; cell counts enter through a sum of integrals, not as a main-term loss.

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

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